Abstract (click to open/close)

Up to now SMT-solvers addressing floating-point arithmetic were based on bit-blasting. Quite recently, methods based on interval constraint propagation (ICP) for accurate reasoning over floating-point arithmetic were proposed. One prominent use-case for such methods is automatic dead-code detection in floating-point dominated embedded C programs. However, C programs usually contain a mix of floating-point arithmetic, integer arithmetic and bitwise integer operations. Thus, adding ICP-based support for floating-point arithmetic is not enough -- bitwise integer operations have to be supported as well. Therefore, this report gives a detailed overview how these operations can be handled with ICP.

Subproject(s): T1

Abstract (click to open/close)

In this technical report, we present an application of the iSAT constraint solver to instances of traffic flow networks.We give an account of the underlying model and provide details of different instances of the model and a variety of verification and falsification tasks handled by our solver.

Subproject(s): H1/2

Abstract (click to open/close)

The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them bounded model checking (BMC) of symbolically represented Markov decision processes. This paper identifies a notion of Craig interpolant for the SSAT framework and develops an algorithm for computing such interpolants based on SSAT resolution. As a potential application, we address the use of interpolation in SSAT-based BMC, turning the falsification procedure into a verification approach for probabilistic safety properties.

Subproject(s): H1/2,H4

Abstract (click to open/close)

In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initial-value problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic constraint solving. Interval-based safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: post-images of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, pre-images are narrowed based on partial knowledge about post-sets. In contrast to the related CLP(F) approach of Hickey and Wittenberg, we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating interval-based overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhacements of recent SAT solving technology.

Subproject(s): H1/2

Abstract (click to open/close)

In recent years, the use of constraint solvers for analysis and verification of industrial systems has become increasingly popular. The correctness and reliability of the results returned by the employed solvers are a vital requirement, in particular for safety-critical systems. If a solver proves the satisfiability of a constraint system and returns a solution then the answer of the solver can be validated by means of the solution. However, in case the solver claims that the constraint system is unsatisfiable without any certificate then the validation of this answer is not that simple. In this paper, we establish the theoretical basis of generating proofs of unsatisfiability in the mixed Boolean and non-linear arithmetic constraint framework over the reals and integers. To do so, we propose a simple rule-based calculus for unsatisfiable mixed Boolean-arithmetic constraints to produce and check unsatisfiability proofs. Furthermore, we enhance the iSAT constraint solver to generate unsatisfiability proofs, we implement a tool validating such proofs, and give some experimental results.

Subproject(s): H1/2

Abstract (click to open/close)

The recently presented constraint solver HySAT tackles the in general undecidable problem of solving mixed Boolean and non-linear arithmetic constraint formulae over the reals involving transcendental functions. The algorithmic core of HySAT is the iSAT algorithm, a tight integration of the Davis-Putnam-Logemann-Loveland algorithm with interval constraint propagation enriched by enhancements like conflict-driven clause learning and non-chronological backtracking. However, it was an open question whether HySAT's conflict analysis scheme, an adapted first unique implication point technique as applied in most modern SAT solvers, performs favorably compared to other schemes. In this paper, we compare several conflict analysis heuristics to answer this question. Furthermore, we consider the integration of restarts into the iSAT algorithm and investigate their impact. For our empirical results we use benchmarks from the hybrid systems domain.

Subproject(s): H1/2

Abstract (click to open/close)

Given the structural diversity of modeling paradigms for hybridsystems that are in widespread use, which ranges from asignal-transducer-based view like in Simulink/Stateflow to anautomaton-based view in various hybrid automata frameworks, there isneed for an intermediate-level language that can accommodate thesestructures in a concise way, thereby isolating verification backendsfrom the particular modeling frontend used.This technical report provides a description of the intermediate-levelmodeling language for hybrid systems used in project area H of AVACS asa gateway to verification backends.

Subproject(s): H1/2,H3