αSPIN: A tool for abstract model checking

2004 ◽  
Vol 5 (2-3) ◽  
pp. 165-184 ◽  
Author(s):  
María del Mar Gallardo ◽  
Jesús Martínez ◽  
Pedro Merino ◽  
Ernesto Pimentel
Keyword(s):  
Model Checking ◽  
Abstract Model ◽  
Abstract Model Checking

AUTOMATED TERMINATION IN MODEL-CHECKING MODULO THEORIES

2013 ◽  
Vol 24 (02) ◽  
pp. 211-232 ◽  
Author(s):  
ALESSANDRO CARIONI ◽  
SILVIO GHILARDI ◽  
SILVIO RANISE
Keyword(s):  
Model Checking ◽  
Sufficient Conditions ◽  
Order Logic ◽  
Satisfiability Modulo Theories ◽  
First Order Logic ◽  
Reachability Problem ◽  
First Order ◽  
Recent Advances ◽  
Infinite State Systems ◽  
Infinite State

We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic.

scholarly journals Automatic verification of timed concurrent constraint programs

2006 ◽  
Vol 6 (3) ◽  
pp. 265-300 ◽  
Author(s):  
MORENO FALASCHI ◽  
ALICIA VILLANUEVA
Keyword(s):  
Model Checking ◽  
Infinite Number ◽  
Reactive Systems ◽  
Finite Model ◽  
Computation Model ◽  
Huge Number ◽  
Finite State ◽  
Infinite State Systems ◽  
Infinite State ◽  
Concurrent Constraint Programming

The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. Constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp.

Sign in / Sign up

Export Citation Format

Share Document