An SMT approach to bounded reachability analysis of model programs

Abstract. Model programs represent transition systems that are used to specify expected behavior of systems at a high level of abstraction. The main application area is application-level network protocols or protocol-data types such as sets and maps, and comprehensions to express com-plex 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 ex-pressed through state invariants. An important problem is to validate the model prior to its use in the above-mentioned contexts. We intro-duce a technique of using Satisfiability Modulo Theories or SMT to per-form 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 incremental and involves selective quantifier instantiation of quantifiers that result from the comprehension expressions.