Verification of Data Paths Using Unbounded Integers: Automata Strike Back

In: E. Bin and A. Ziv and S. Ur ed., Haifa Verification Conference (HVC), Haifa, Israel. LNCS, Volume 4383, Springer, P. 65-80, 2007

Authors

• Tobias Schüle
• Klaus Schneider

Abstract

We present a decision procedure for quantifier-free Presburger arithmetic that is based on a polynomial time translation of Presburger formulas to alternating finite automata (AFAs). Moreover, our approach leverages the advances in SAT solving by reducing the emptiness problem of AFAs to satisfiability problems of propositional logic. In order to obtain a complete decision procedure, we use an inductive style of reasoning as originally proposed for proving safety properties in bounded model checking. Besides linear arithmetic constraints, our decision procedure can deal with bitvector operations that frequently occur in hardware design. Thus, it is well-suited for the verification of data paths at a high level of abstraction.

Full Text

• Publication: ScSc07.pdf

BibTeX

 
@InProceedings{ ScSc07, 
   title = { Verification of Data Paths Using Unbounded Integers: Automata Strike Back }, 
   author = { Tobias Schüle and Klaus Schneider },  
   editor = { E. Bin and A. Ziv and S. Ur }, 
   booktitle = { Haifa Verification Conference (HVC), Haifa, Israel },  
   series = { LNCS }, 
   volume = { 4383 },     
   publisher = { Springer },   
   pages = { 65-80 },   
   year = 2007, 
} 

---

This publication belongs to the project EVAS.