scholarly journals Synthesis of infinite-state systems with random behavior

2020 ◽  
Author(s):  
Andreas Katis ◽  
Grigory Fedyukovich ◽  
Jeffrey Chen ◽  
David Greve ◽  
Sanjai Rayadurgam ◽  
...  
Keyword(s):  
Random Behavior ◽  
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.

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

Efficient Symbolic Representations for Arithmetic Constraints in Verification

2003 ◽  
Vol 14 (04) ◽  
pp. 605-624 ◽  
Author(s):  
Constantinos Bartzis ◽  
Tevfik Bultan
Keyword(s):  
Finite Automata ◽  
Transition Function ◽  
Linear Constraints ◽  
Symbolic Representations ◽  
Integer Variables ◽  
Efficient Storage ◽  
Verification Algorithms ◽  
Infinite State Systems ◽  
Construction Algorithms ◽  
Infinite State

In this paper we discuss efficient symbolic representations for infinite-state systems specified using linear arithmetic constraints. We give algorithms for constructing finite automata which represent integer sets that satisfy linear constraints. These automata can represent either signed or unsigned integers and have a lower number of states compared to other similar approaches. We present efficient storage techniques for the transition function of the automata and extend the construction algorithms to formulas on both boolean and integer variables. We also derive conditions which guarantee that the pre-condition computations used in symbolic verification algorithms do not cause an exponential increase in the automata size. We experimentally compare different symbolic representations by using them to verify non-trivial concurrent systems. Experimental results show that the symbolic representations based on our construction algorithms outperform the polyhedral representation used in Omega Library, and the automata representation used in LASH.

scholarly journals Abstraction refinement and antichains for trace inclusion of infinite state systems

2020 ◽  
Vol 55 (3) ◽  
pp. 137-170
Author(s):  
Lukáš Holík ◽  
Radu Iosif ◽  
Adam Rogalewicz ◽  
Tomáš Vojnar
Keyword(s):  
Abstraction Refinement ◽  
Infinite State Systems ◽  
Infinite State

SMT-based verification of data-aware processes: a model-theoretic approach

2020 ◽  
Vol 30 (3) ◽  
pp. 271-313
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Model Theory ◽  
Satisfiability Modulo Theories ◽  
Theoretic Approach ◽  
Model Checker ◽  
Present Contribution ◽  
Relational Systems ◽  
Infinite State Systems ◽  
Algorithmic Techniques ◽  
The One ◽  
Infinite State

AbstractIn recent times, satisfiability modulo theories (SMT) techniques gained increasing attention and obtained remarkable success in model-checking infinite-state systems. Still, we believe that whenever more expressivity is needed in order to specify the systems to be verified, more and more support is needed from mathematical logic and model theory. This is the case of the applications considered in this paper: we study verification over a general model of relational, data-aware processes, to assess (parameterized) safety properties irrespectively of the initial database (DB) instance. Toward this goal, we take inspiration from array-based systems and tackle safety algorithmically via backward reachability. To enable the adoption of this technique in our rich setting, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems and represents the main original contribution of this paper. In this way, we pursue a twofold purpose. On the one hand, we isolate three notable classes for which backward reachability terminates, in turn witnessing decidability. Two of such classes relate our approach to conditions singled out in the literature, whereas the third one is genuinely novel. On the other hand, we are able to exploit SMT technology in implementations, building on the well-known MCMT (Model Checker Modulo Theories) model checker for array-based systems and extending it to make all our foundational results fully operational. All in all, the present contribution is deeply rooted in the long-standing tradition of the application of model theory in computer science. In particular, this paper applies these ideas in an original mathematical context and shows how these techniques can be used for the first time to empower algorithmic techniques for the verification of infinite-state systems based on arrays, so as to make such techniques applicable to the timely, challenging settings of data-aware processes.

Theorem-proving anonymity of infinite-state systems

2007 ◽  
Vol 101 (1) ◽  
pp. 46-51 ◽  
Author(s):  
Yoshinobu Kawabe ◽  
Ken Mano ◽  
Hideki Sakurada ◽  
Yasuyuki Tsukada
Keyword(s):  
Theorem Proving ◽  
Infinite State Systems ◽  
Infinite State
Sign in / Sign up

Export Citation Format

Share Document