ABSTRACT. Despite decades of research, reasoning efficiently about formulas containing both quantifiers and built-in symbols for a given background theory remains a challenge in automated deduction. Nevertheless, several exciting advances have been made in the last few years, mainly in two directions: (i) integrating theory reasoning in saturation-based calculi for first-order logic and (ii) integrating quantified reasoning into frameworks for ground Satisfiability Modulo Theories (SMT). Focusing on the latter, this talk provides an overview of a general, refutation-based approach for reasoning about quantified formulas in SMT. The approach maintains a set S of ground formulas that is incrementally expanded with selected instances of quantified input formulas, with the selection based on counter-models of S. In addition to being quite effective in practice, for several logical theories that admit quantifier elimination and have a decidable universal fragment this approach also leads to practically efficient decision procedures for the full theory. While the approach applies to traditional theories with quantifier elimination such as linear real and integer arithmetic, this talk will present new promising developments for the theory of fixed-sized bit vectors and the theory of floating point arithmetic whose full-fragments are notoriously difficult to reason about.

ABSTRACT. Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmetic or pseudo-Boolean terms. However, many SMT and OMT applications, mostly from SW and HW verification, require handling bit-precise representations of numbers, which in SMT are handled by means of the theory of Bit-Vectors (BV) for the integers and that of Floating-Point Numbers (FP) for the reals respectively. Whereas an approach for OMT with (unsigned) BV has been proposed by Nadel & Ryvchin, unfortunately we are not aware of any existing approach for OMT with FP.

In this paper we fill this gap. We present a novel OMT approach, based on the novel concept of attractor and dynamic attractor, which extends the work of Nadel & Ryvchin to signed BV and, most importantly, to FP. We have implemented some OMT(BV) and OMT(FP) procedures on top of OptiMathSAT and tested the latter ones on modified problems from the SMT-LIB repository. The empirical results support the validity and feasibility of the novel approach.

ABSTRACT. Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The underlying synthesis problem, however, is challenging and existing methods have limitations on the form of formulae to be interpolated. We leverage classification techniques with space transformations and kernel tricks as established in the realm of machine learning, and present a counterexample-guided method named NIL for synthesizing polynomial interpolants, thereby yielding a unified framework tackling the interpolation problem for the general quantifier-free theory of nonlinear arithmetic, possibly involving transcendental functions. We prove the soundness of NIL and propose sufficient conditions under which NIL is guaranteed to converge, i.e., the derived sequence of classifiers (candidate interpolants) converges to an actual interpolant, and to be complete, namely the algorithm terminates by producing an interpolant if there exists one. The applicability and effectiveness of our technique are demonstrated experimentally on a collection of representative benchmarks from the literature, where in particular, our method suffices to address more interpolation tasks, including those with perturbations in parameters, and in many cases synthesize simpler interpolants comparing to existing approaches.

ABSTRACT. In this paper we study possibilities for automated invariant generation in parametric systems. For this, we refine results on symbol elimination we previously established in order to make them more efficient. We use these results for devising a method for iteratively strengthening certain classes of safety properties to obtain invariants of the system. We identify conditions under which the method is correct and complete, and situations in which the method is guaranteed to terminate. We illustrate the method on several examples.

ABSTRACT. We introduce the class of constant probability (CP) programs and show that classical results from probability theory directly yield a simple decision procedure for (positive) almost sure termination of programs in this class. Moreover, asymptotically tight bounds on their expected runtime can always be computed easily. Based on this, we present an algorithm to infer the exact expected runtime of any CP program.

ABSTRACT. In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and exploited it to attack infinite-state model checking problems. Motivated by applications to the verification of data-aware processes, we show how covers are strictly related to model completions, a well-known topic in classical model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus, equipped with appropriate settings and reduction strategies.

ABSTRACT. Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical admissibility checks does this paper introduce a uniform substitution mechanism that proceeds in a linear pass homomorphically along the formula. Soundness is recovered using a simple variable condition at the replacements performed by the substitution. The setting in this paper is that of differential hybrid games, in which discrete, continuous, and adversarial dynamics interact in differential game logic dGL. This paper proves soundness and completeness of one-pass uniform substitutions for dGL.

ABSTRACT. We enable the theory of differential dynamic logic (dL) for hybrid systems to play catchup with its practice in the theorem prover KeYmaera X by augmenting dL with terms for definite descriptions that describe definable partial functions. At least in the form of divisions, nth roots, or absolute values do such extended terms arise frequently in applications. Besides the woes of partiality do they come with subtleties in differential equations, because definable functions may ruin local Lipschitz continuity and, thereby, uniqueness and longevity of solutions.

Our extension of dL to definite descriptions (dLi) is a free logic; we investigate the interaction of free logic and the differential equations (ODEs) of dL, showing that this combination is sound. We show how dLi can be used not only to recover practical features used today in KeYmaera X, but also many desirable features not yet available in implementation, proving it to be a useful foundation. We give examples showing how new systems can be defined and verified using these extensions.

ABSTRACT. Some hybrid systems models are unsafe for mathematically correct but physically unrealistic reasons. For example, mathematical models can classify a system as being unsafe on a set that is too small to have physical importance. In particular, differences in measure-zero sets in models of cyber-physical systems (CPS) have significant mathematical impact on the mathematical safety of these models even though differences on measure-zero sets have no tangible physical effect in a real system. We develop the concept of ``physical hybrid systems'' to help reunite mathematical models with physical reality. We modify a hybrid systems logic (differential temporal dynamic logic) by adding a first-class operator to elide distinctions on measure-zero sets of time within CPS models. This approach facilitates modeling since it admits the verification of a wider class of models, including some physically realistic models that would otherwise be classified as mathematically unsafe. We also develop a proof calculus to help with the verification of physical hybrid systems.

ABSTRACT. Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, however, cannot be used directly to reason about bit-vectors of symbolic bit-width. To address this shortcoming, we propose a translation from bit-vector formulas of non-fixed bit-width to formulas in a logic supported by SMT solvers that includes non-linear integer arithmetic, uninterpreted functions, and universal quantification. While this logic is undecidable, this approach can still solve many formulas by capitalizing on advancements in SMT solving for non-linear arithmetic and universally quantified formulas. We provide several case studies in which we have applied this approach with promising results, including the bit-width independent verification of invertibility conditions, compiler optimizations, and bit-vector rewrites.

ABSTRACT. SPASS-SATT is a CDCL(LA) solver for linear rational and linear mixed/integer arithmetic. This system description explains its specific features: fast cube tests for integer solvability, bounding transformations for unbounded problems, close interaction between the SAT solver and the theory solver, efficient data structures, and small-clause-normal-form generation. SPASS-SATT is currently one of the strongest systems on the respective SMT-LIB benchmarks.