JUCS - Journal of Universal Computer Science 7(2): 124-140, doi: 10.3217/jucs-007-02-0124
A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic
expand article infoAlessandro Armando‡, Silvio Ranise§
‡ Università degli Studi di Genova, Genova, Italy§ DIST - Università degli Studi di Genova, Genova, Italia and LORIA - Université Henri Poincaré, Nancy, France

Corresponding author: Alessandro Armando ( armando@dist.unige.it )

© Alessandro Armando, Silvio Ranise.
This article is freely available under the J.UCS Open Content License.
Citation: Armando A, Ranise S (2001) A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. JUCS - Journal of Universal Computer Science 7(2): 124-140. https://doi.org/10.3217/jucs-007-02-0124
Open Access
Abstract
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.
Keywords
affnization, augmentation, formal verification, decision procedures, lemma speculation, universal arithmetic over integers, universal Presburger Arithmetic over integers