Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 7 / Issue 2

available in:   PDF (298 kB) PS (96 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-007-02-0124


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