Sciweavers

Share
FORTE
2008

An SMT Approach to Bounded Reachability Analysis of Model Programs

8 years 5 months ago
An SMT Approach to Bounded Reachability Analysis of Model Programs
Model programs represent transition systems that are used fy expected behavior of systems at a high level of abstraction. The main application area is application-level network protocols or protocolects of software systems. Model programs typically use abstract data types such as sets and maps, and comprehensions to express complex state updates. Such models are mainly used in model-based testing as inputs for test case generation and as oracles during conformance testing. Correctness assumptions about the model itself are usually expressed through state invariants. An important problem is to validate the model prior to its use in the above-mentioned contexts. We introduce a technique of using Satisfiability Modulo Theories or SMT to perform bounded reachability analysis of a fragment of model programs. We use the Z3 solver for our implementation and benchmarks, and we use AsmL as the modeling language. The translation from a model program into a verification condition of Z3 is increme...
Margus Veanes, Nikolaj Bjørner, Alexander R
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2008
Where FORTE
Authors Margus Veanes, Nikolaj Bjørner, Alexander Raschke
Comments (0)
books