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

available in:   PDF (298 kB) PS (96 kB)
 
get:  
Similar Docs BibTeX   Write a comment
  
get:  
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