NFM
2011
13 years 7 months ago
2011
Symbolic execution is a powerful automated technique for generating test cases. Its goal is to achieve high coverage of software. One major obstacle in adopting the technique in pr...
NFM
2011
13 years 7 months ago
2011
Abstract. We present a general scheme for automated instantiation-based invariant discovery. Given a transition system, the scheme produces k-inductive invariants from templates re...
NFM
2011
13 years 7 months ago
2011
Abstract. We present a new open source model checker, opaal, for automatic verification of models using lattice automata. Lattice automata allow the users to incorporate abstracti...
NFM
2011
13 years 7 months ago
2011
A main idea underlying bounded model checking is to limit the length of the potential counter-examples, and then prove properties for the bounded version of the problem. In softwar...
NFM
2011
13 years 7 months ago
2011
A safety claim for a system is a statement that the system, which is subject to hazardous conditions, satisfies a given set of properties. Following work by John Rushby and Bev Li...
NFM
2011
13 years 7 months ago
2011
Program verifiers based on first-order theorem provers model the program heap as a collection of mutable maps. In such verifiers, preserving unmodified facts about the heap acr...
NFM
2011
13 years 7 months ago
2011
NFM
2011
13 years 7 months ago
2011
Abstract. Tabular expressions have been successfully used in developing safety critical systems, however insufficient tool support has hampered their wider adoption. To address thi...
NFM
2011
13 years 7 months ago
2011
Abstract. In parametric Markov Decision Processes (PMDPs), transition probabilities are not fixed, but are given as functions over a set of parameters. A PMDP denotes a family of ...
NFM
2011
13 years 7 months ago
2011
Abstract. Event-B is a formal method for modeling and verifying consistency of systems. In formal methods such as Event-B, refinement is the process of enriching or modifying an a...