scholarly journals Reachability Modulo Theory Library

10.29007/f3rp ◽  
2018 ◽  
Author(s):  
Francesco Alberti ◽  
Roberto Bruttomesso ◽  
Silvio Ghilardi ◽  
Silvio Ranise ◽  
Natasha Sharygina
Keyword(s):  
Reachability Analysis ◽  
Safety Properties ◽  
Standard Language ◽  
Transition Systems ◽  
Smt Solvers ◽  
Verification Tools ◽  
Infinite State Systems ◽  
Infinite State

Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.

scholarly journals Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis

1999 ◽  
pp. 146-159 ◽  
Author(s):  
Parosh Aziz Abdulla ◽  
Aurore Annichini ◽  
Saddek Bensalem ◽  
Ahmed Bouajjani ◽  
Peter Habermehl ◽  
...  
Keyword(s):  
Reachability Analysis ◽  
Infinite State Systems ◽  
Infinite State

ON REACHABILITY AND SAFETY IN INFINITE-STATE SYSTEMS

2001 ◽  
Vol 12 (06) ◽  
pp. 821-836 ◽  
Author(s):  
OSCAR H. IBARRA ◽  
TEVFIK BULTAN ◽  
JIANWEN SU
Keyword(s):  
Data Structures ◽  
State Transition ◽  
Constant Independent ◽  
Transition Systems ◽  
Basic Model ◽  
Counter Machine ◽  
A Cell ◽  
Infinite State Systems ◽  
Infinite State ◽  
Nondeterministic Finite Automaton

We introduce some new models of infinite-state transition systems. The basic model, called a (reversal-bounded) counter machine (CM), is a nondeterministic finite automaton augmented with finitely many reversal-bounded counters (i.e. each counter can be incremented or decremented by 1 and tested for zero, but the number of times it can change mode from nondecreasing to nonincreasing and vice-versa is bounded by a constant, independent of the computation). We extend a CM by augmenting it with some familiar data structures: (i) A pushdown counter machine (PCM) is a CM augmented with an unrestricted pushdown stack. (ii) A tape counter machine (TCM) is a CM augmented with a two-way read/write worktape that is restricted in that the number of times the head crosses the boundary between any two adjacent cells of the worktape is bounded by a constant, independent of the computation (thus, the worktape is finite-crossing). There is no bound on how long the head can remain on a cell. (iii) A queue counter machine (QCM) is a CM augmented with a queue that is restricted in that the number of alternations between non-deletion phase and non-insertion phase on the queue is bounded by a constant. A non-deletion (non-insertion) phase is a period consisting of insertions (deletions) and no-changes, i.e., the queue is idle. We show that emptiness, (binary, forward, and backward) reachability, nonsafety, and invariance for these machines are solvable. We also look at extensions of the models that allow the use of linear-relation tests among the counters and parameterized constants as "primitive" predicates. We investigate the conditions under which these problems are still solvable.

scholarly journals Improving Reachability Analysis of Infinite State Systems by Specialization

2012 ◽  
Vol 119 (3-4) ◽  
pp. 281-300 ◽  
Author(s):  
Fabio Fioravanti ◽  
Alberto Pettorossi ◽  
Maurizio Proietti ◽  
Valerio Senni
Keyword(s):  
Reachability Analysis ◽  
Infinite State Systems ◽  
Infinite State

scholarly journals Improving Reachability Analysis of Infinite State Systems by Specialization

2011 ◽  
pp. 165-179 ◽  
Author(s):  
Fabio Fioravanti ◽  
Alberto Pettorossi ◽  
Maurizio Proietti ◽  
Valerio Senni
Keyword(s):  
Reachability Analysis ◽  
Infinite State Systems ◽  
Infinite State

scholarly journals Model Completeness, Uniform Interpolants and Superposition Calculus

2021 ◽  
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Automated Reasoning ◽  
Quantifier Elimination ◽  
Effective Solution ◽  
Model Completeness ◽  
Present Contribution ◽  
First Order ◽  
Reduction Strategies ◽  
Infinite State Systems ◽  
Infinite State ◽  
Superposition Calculus

AbstractUniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

Sign in / Sign up

Export Citation Format

Share Document