Search

In recent years, the inductive, incremental verification algorithm IC3 had a major impact on hardware model checking. Also for software model checking, a number of adaptations of Boolean IC3 and combinations with CEGAR and ART-based techniques have been developed. However, most of them exploit the peculiarities of software programs, such as the explicit representation of control flow, only to a limited extent. In this paper, we present an approach that supports this explicit representation in the form of control-flow automata, and integrates it with symbolic reasoning about the data state space of the program. By maintaining reachability information specifically for each control location, we arrive at a “two-dimensional” extension of IC3, which provides a true lifting from hardware to software model checking. Moreover, we address the problem of generalization in this setting, an essential feature to ensure the scalability of IC3. We introduce several improvements that range from efficient caching of generalizations over variable reductions to syntax-oriented generalization by means of weakest preconditions. Using a prototypical implementation, we evaluate our approach on a number of case studies, including a significant subset of the SV-COMP 2018 benchmarks, and compare the outcomes with results obtained from other IC3 software model checkers.

Generalization is a key feature to support state-space abstraction in IC3-based algorithms for software model checking, such as Tree-IC3 or IC3CFA. This paper introduces several improvements that range from efficient caching of generalizations over variable reductions to syntax-oriented generalization. Our techniques are generic in that they are independent of the underlying theory, and some of them are even applicable to IC3 in general. Their evaluation on multiple benchmarks, including a significant subset of the SV-COMP 2017 benchmarks, yields promising results.

Schedulers in randomly timed games can be classified as to whether they use timing information or not. We consider continuous-time Markov decision processes (CTMDPs) and define a hierarchy of positional (P) and history-dependent (H) schedulers which induce strictly tighter bounds on quantitative properties on CTMDPs. This classification into time abstract (TA), total time (TT) and fully time-dependent (T) schedulers is mainly based on the kind of timing details that the schedulers may exploit. We investigate when the resolution of nondeterminism may be deferred. In particular, we show that TTP and TAP schedulers allow for delaying nondeterminism for all measures, whereas this does neither hold for TP nor for any TAH scheduler. The core of our study is a transformation on CTMDPs which unifies the speed of outgoing transitions per state.

This paper provides a contribution to the formal verification of programs written in the concurrent functional programming language Erlang, which is designed for telecommunication applications. We present a formalization of this language in the Rewriting Logic framework, employing equations for defining abstraction mappings on the state space of the system. Moreover we give a sketch of an implementation in the Maude system, and demonstrate the use of its model checker to verify simple system properties.

This paper presents a novel refinement strategy in the setting of counterexample-guided abstraction refinement (CEGAR)-based model checking. More specifically, the approach shown builds on lazy abstraction in the context of predicate abstraction. While the concept of interpolants is typically used for refinement, this paper employs unsatisfiability cores together with weakest preconditions. The new refinement technique is especially applicable in the setting where interpolants are hard to compute, such as for McCarthy’s theory of arrays or for the theory of fixed-width bit vectors. It is implemented within a model-checking tool developed for the verification of industrial-critical systems and outperforms current refinement strategies on several examples.

Programmable logic controllers (PLC) are widely used in industries ranging from assembly lines, power plants, chemical processes to mining and rail automation. Such systems usually exhibit high safety requirements, and downtimes due to software errors entail intolerably high economic costs. Hence, their control programs are particularly suited for applying formal methods; in particular, bounded model checking (BMC) techniques based on satisfiability modulo theories promise to be highly beneficial in this domain.

We propose to exploit three-valued abstraction to stochastic systems in a compositional way. This combines the strengths of an aggressive state-based abstraction technique with compositional modeling. Applying this principle to interactive Markov chains yields abstract models that combine interval Markov chains and modal transition systems in a natural and orthogonal way. We prove the correctness of our technique for parallel and symmetric composition and show that it yields lower bounds for minimal and upper bounds for maximal timed reachability probabilities.

This paper introduces strong bisimulation for continuous-time Markov decision processes (CTMDPs), a stochastic model which allows for a nondeterministic choice between exponential distributions, and shows that bisimulation preserves the validity of CSL. To that end, we interpret the semantics of CSL - a stochastic variant of CTL for continuous-time Markov chains - on CTMDPs and show its measure theoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory.