A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic
Alessandro Armando (Università degli Studi di Genova, Italia)
Silvio Ranise (DIST - Università degli Studi di Genova, Genova, Italia and LORIA - Université Henri Poincaré, France)
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, decision procedures, formal verification, lemma speculation, universal Presburger Arithmetic over integers, universal arithmetic over integers
Categories: F.3.1, I.1.1, I.1.2, I.2.3