scholarly journals Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic

2014 ◽  
pp. 85-97 ◽  
Author(s):  
Stéphane Demri ◽  
Amit Kumar Dhar ◽  
Arnaud Sangnier
Keyword(s):  
Model Checking ◽  
Presburger Arithmetic

Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic

2003 ◽  
pp. 687-698 ◽  
Author(s):  
Véronique Bruyère ◽  
Emmanuel Dall’Olio ◽  
Jean-FranÇois Raskin
Keyword(s):  
Model Checking ◽  
Timed Automata ◽  
Parametric Model ◽  
Presburger Arithmetic

A practical approach to model checking Duration Calculus using Presburger Arithmetic

2013 ◽  
Vol 71 (1-3) ◽  
pp. 251-278 ◽  
Author(s):  
Michael R. Hansen ◽  
Anh-Dung Phan ◽  
Aske W. Brekling
Keyword(s):  
Model Checking ◽  
Practical Approach ◽  
Duration Calculus ◽  
Presburger Arithmetic

scholarly journals Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays

10.29007/zfkw ◽  
2018 ◽  
Author(s):  
Angelo Brillout ◽  
Daniel Kroening ◽  
Philipp Rümmer ◽  
Thomas Wahl
Keyword(s):  
Model Checking ◽  
Program Verification ◽  
Model Checker ◽  
Craig Interpolation ◽  
Presburger Arithmetic ◽  
C Programs ◽  
Full Theory ◽  
Software Model ◽  
Interpolation Procedure ◽  
Versatile Tool

Craig interpolation has become a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. In this paper, we present a novel interpolation procedure for the theory of arrays, extending an interpolating calculus for the full theory of quantifier-free Presburger arithmetic, which will be presented at IJCAR this year. We investigate the use of this procedure in a software model checker for C programs. A distinguishing feature of the model checker is its ability to faithfully model machine arithmetic with an encoding into Presburger arithmetic with uninterpreted predicates. The interpolation procedure allows the synthesis of quantified invariants about arrays. This paper presents work in progress; we include initial experiments to demonstrate the potential of our method.

scholarly journals Equivalence between model-checking flat counter systems and Presburger arithmetic

2018 ◽  
Vol 735 ◽  
pp. 2-23
Author(s):  
Stéphane Demri ◽  
Amit Kumar Dhar ◽  
Arnaud Sangnier
Keyword(s):  
Model Checking ◽  
Presburger Arithmetic

COMPOSITIONALITY AND REACHABILITY WITH CONDITIONS ON PATH LENGTHS

2009 ◽  
Vol 20 (05) ◽  
pp. 851-868 ◽  
Author(s):  
INGO FELSCHER ◽  
WOLFGANG THOMAS
Keyword(s):  
Model Checking ◽  
Finite Number ◽  
Order Logic ◽  
First Order Logic ◽  
Presburger Arithmetic ◽  
First Order ◽  
Path Lengths ◽  
Composition Theorem ◽  
Compositional Method

In model-checking the systems under investigation often arise in the form of products. The compositional method, developed by Feferman and Vaught in 1959, fits to this situation and can be used to deduce the truth of a formula in the product from information in the factors. Building on earlier work of Wöhrle and Thomas (2004), we study first-order logic with reachability predicates over finitely synchronized products (i.e. synchronized products with a finite number of synchronization transitions). We extend the reachability predicates by conditions on the length of the corresponding paths, formulated in Presburger arithmetic. For finitely synchronized products with these enhanced reachability predicates we prove a composition theorem and then show that severe limitations exist for generalisations of this result.

Sign in / Sign up

Export Citation Format

Share Document