A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic
Дата
Авторы
Armando,Alessandro
Ranise,Silvio
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
In this paper, we propose a generic mechanism for extending decision procedures by means of a lemma speculation mechanism. This problem is important in order to widen the scope of decision procedures incorporated in state-of-the-art verification systems. Soundness and termination of the extension schema are formally stated and proved. As a case study, we consider extensions of a decision procedure for the quantifier-free fragment of Presburger Arithmetic to significant fragments of non-linear arithmetic.
Ключевые слова
affnization , augmentation , formal verification , decision procedures , lemma speculation , universal arithmetic over integers , universal Presburger Arithmetic over integers