<< PUBLICATIONS (in reverse chronological order) Click here to hide/show abstracts
. . {Abstract} We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., ``x^n in Q'' and ``x^n in Z.'' Our decision procedure combines computation over real algebraic cells with the rational root theorem and witness construction via algebraic number density arguments.
. . {Abstract} We present a complete, certificate-based decision procedure for first order univariate polynomial problems in Isabelle. This decision procedure is built around an executable function to decide the sign of a univariate polynomial at a real algebraic point. The procedure relies on no trusted code except for Isabelle's kernel and code generation. This work is the first step towards integrating MetiTarski into Isabelle.
. . {Abstract} We describe work in progress on constructing a complete implementation of Weispfenning's virtual term substitution method for real closed field formulas of unbounded degree. We build upon a recent high-performance library for computing over non-Archimedean real closed fields using Thom's Lemma.
. .
{Abstract} Hybrid systems with both discrete and continuous dynamics are an important model for real-world physical systems. The key challenge is how to ensure their correct functioning with respect to safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner, and formal verification to prove their correctness. Their combination forms the vision of verification-driven engineering. Despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires nontrivial human guidance, since hybrid systems verification tools solve undecidable problems. It is thus not uncommon for verification teams to consist of many players with diverse expertise. This paper introduces a verification-driven engineering toolset that extends our previous work on hybrid and arithmetic verification with tools for (i) graphical (UML) and textual modeling of hybrid systems, (ii) exchanging and comparing models and proofs, and (iii) managing verification tasks. This toolset makes it easier to tackle large-scale verification efforts.
. .
{Abstract} Recent applications of decision procedures for nonlinear real arithmetic (the theory of real closed fields, or RCF) have presented a need for reasoning not only with polynomials but also with transcendental constants and infinitesimals. In full generality, the algebraic setting for this reasoning consists of real closed transcendental and infinitesimal extensions of the rational numbers. We present a library for computing over these extensions. This library contains many contributions, including a novel combination of Thom's Lemma and interval arithmetic for representing roots, and provides all core machinery required for building RCF decision procedures. We describe the abstract algebraic setting for computing with such field extensions, present our concrete algorithms and optimizations, and illustrate the library on a collection of examples.
. .
{Abstract} Nonlinear real arithmetic (the theory of real closed fields, or RCF) is crucial to the formal verification of cyber-physical systems (CPS). Though RCF is decidable, it is fundamentally infeasible (hyperexponential in the number of variables). This infeasibility is a serious practical concern, as modern CPS verification tools such as KeYmaera and MetiTarski make heavy use of nonlinear real arithmetic decision procedures, generating hundreds or thousands of many-variable RCF subproblems during their proof search. As these verification tools progress upon a proof, they accumulate a large database of RCF facts which pertain to the system being analyzed. As subsequent RCF subproblems are generated, they are tested for validity modulo this database of background facts. In this work, we exploit the fact that, in practice, often only a small subset of the background RCF facts are needed to decide the generated subproblems. The difficulty is in how the most relevant facts should be selected. We present an RCF decision method which combines sampling techniques and cell decomposition methods adapted from cylindrical algebraic decomposition to use geometric information to select relevant background facts. We illustrate its performance upon real-world benchmark problems drawn from KeYmaera and MetiTarski verification efforts.
. .
{Abstract} Hybrid systems with both discrete and continuous dynamics are an important model for real-world physical systems. The key challenge is how to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner and formal verification to prove their correctness, forming the vision of verification-driven engineering. Despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires significant human guidance, since hybrid systems verification tools work over an undecidable theory. It is thus not uncommon for verification teams to consist of many players with diverse expertise. This paper introduces a verification-driven engineering toolset that extends our previous work on hybrid and arithmetic verification with tools for (i) modeling hybrid systems, (ii) exchanging and comparing models and proofs, and (iii) managing verification tasks. This toolset makes it easier to tackle large-scale verification tasks.
. .
{Abstract} High-performance SMT solvers contain many tightly integrated, hand-crafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems (e.g., SMT-LIB benchmarks), they may easily perform very badly on new classes of problems not anticipated by solver developers. This issue is becoming increasingly pressing as SMT solvers begin to gain the attention of practitioners in diverse areas of science and engineering. In many cases, changes to the prover heuristics can make a tremendous difference in the success of SMT solving within new problem domains. Classically, however, much of the control of these heuristics has been outside the reach of solver end-users. We present a challenge to the SMT community: to develop methods through which users can exert strategic control over core heuristic aspects of SMT solvers. We present evidence, through research undertaken with the tools RAHD and Z3, that the adaptation of ideas of strategy prevalent within both Argonne-style theorem provers and the LCF-influenced interactive theorem proving community can go a long way towards realizing this goal. In the process, we solidify some foundations for strategy in the context of SMT and pose a number of challenge problems.
. .
{Abstract} MetiTarski is an automatic theorem prover that can prove inequalities involving sin, cos, exp, ln, etc. During its proof search, it generates a series of subproblems in nonlinear polynomial real arithmetic which are reduced to true or false using a decision procedure for the theory of real closed fields (RCF). These calls are often a bottleneck: RCF is fundamentally infeasible. However, by studying these subproblems, we can design specialised variants of RCF decision procedures that run faster and improve MetiTarski's performance.
. .
{Abstract} Though decidable, the theory of real closed fields (RCF) is fundamentally infeasible. This is unfortunate, as automatic proof methods for nonlinear real arithmetic are crucially needed in both formalised mathematics and the verification of real-world cyber-physical systems. Consequently, many researchers have proposed fast, sound but incomplete RCF proof procedures which are useful in various practical applications. We show how such practically useful, sound but incomplete RCF proof methods may be systematically utilised in the context of a complete RCF proof method without sacrificing its completeness. In particular, we present an extension of the RCF quantifier elimination method Partial CAD (P-CAD) which uses incomplete $\exists$ RCF proof procedures to ``short-circuit'' expensive computations during the lifting phase of P-CAD. We present the theoretical framework and preliminary experiments arising from an implementation in our RCF proof tool RAHD.
. . {Abstract} John organized a state lottery, and his wife won the main prize. You may feel that the event of her winning wasn't particularly random, but how would you argue that in a fair court of law? Traditional probability theory does not even have the notion of random events. Information complexity theory does, but it is not applicable to real-world scenarios like the lottery one. We attempt to rectify that.
. .
{Abstract}
We describe contributions to algorithmic proof techniques for deciding the satisfiability of boolean combinations of many-variable nonlinear polynomial equations and inequalities over the real and complex numbers. In the first half, we present an abstract theory of Groebner basis construction algorithms for algebraically closed fields of characteristic zero and use it to introduce and prove correct Groebner basis methods specialised to the needs of modern satisfiability modulo theories (SMT) solvers. In the process, we use the technique of proof orders to derive a generalisation of S-polynomial superfluousness in terms of transfinite induction along an ordinal parameterised by a monomial order. We use this generalisation to prove the abstract (``strategy-independent'') admissibility of a number of superfluous S-polynomial criteria important for efficient basis construction. Finally, we consider local notions of proof minimality for weak Nullstellensatz proofs and give ideal-theoretic methods for computing complex ``unsatisfiable cores'' which contribute to efficient SMT solving in the context of nonlinear complex arithmetic. In the second half, we consider the problem of effectively combining a heterogeneous collection of decision techniques for fragments of the existential theory of real closed fields. We propose and investigate a number of novel combined decision methods and implement them in our proof tool RAHD (Real Algebra in High Dimensions). We build a hierarchy of increasingly powerful combined decision methods, culminating in a generalisation of partial cylindrical algebraic decomposition (CAD) which we call Abstract Partial CAD. This generalisation incorporates the use of arbitrary sound but incomplete (semi-)decision procedures for the existential theory of real closed fields as functional parameters for ``short-circuiting'' the lifting phase of CAD. Identifying the decision procedure parameters used during lifting formally with RAHD proof strategies, we implement the method in RAHD for the case of full-dimensional cell decompositions and investigate its efficacy with respect to a collection of proof strategy parameters and the Brown-McCallum projection operator. We end with some wishes for the future.
. . {Abstract} We present novel Groebner basis algorithms based on saturation loops used by modern superposition theorem provers. We illustrate the practical value of the algorithms through an experimental implementation within the Z3 SMT solver.
. . {Abstract} RAHD is a tool that takes advantage of a heterogeneous collection of proof procedures to decide the satisfiability of formulas in the existential fragment of the theory of real closed fields. But system analysts can rarely restrict themselves only to arithmetic-based problems: they might want to use RAHD as part of a more diverse formal toolbox. In this paper, we present ongoing work on an architecture that enables the skeptical integration of RAHD into general-purpose proof assistants. We will present a system-level view of how this integration can be performed, and examine efficiency concerns for this implementation.
. . {Abstract} Using the machinery of proof orders originally introduced by Bachmair and Dershowitz in the context of canonical equational proofs, we give an abstract, strategy-independent presentation of Groebner basis procedures and prove the correctness of two classical criteria for recognising superfluous S-polynomials, Buchberger's criteria 1 and 2, w.r.t. arbitrary fair and correct basis construction strategies. To do so, we develop a general method for proving the strategy-independent correctness of superfluous S-polynomial criteria which seems to be quite powerful. We also derive a new superfluous S-polynomial criterion which is a generalisation of Buchberger-1 and is proved to be correct strategy-independently.
. . {Abstract} Hilbert's weak Nullstellensatz guarantees the existence of algebraic proof objects certifying the unsatisfiability of systems of polynomial equations not satisfiable over any algebraically closed field. Such proof objects take the form of ideal membership identities and can be found algorithmically using Groebner bases and cofactor-based linear algebra techniques. However, these proof objects may contain redundant information: a proper subset of the equational assumptions used in these proofs may be sufficient to derive the unsatisfiability of the original polynomial system. For using Nullstellensatz techniques in SMT-based decision methods, a minimal proof object is often desired. With this in mind, we introduce a notion of locally minimal Nullstellensatz proofs and give ideal-theoretic algorithms for their construction.
. . {Abstract} We observe that the decision problem for the existential theory of real closed fields (RCF) is simply reducible to the decision problem for RCF over a connective-free universal language in which the only relation symbol is a strict inequality. In particular, every existential RCF sentence phi can be settled by deciding a proposition of the form ``polynomial p (which is a sum of squares) takes on strictly positive values over the reals,'' with p simply derived from phi. Motivated by this observation, we pose the goal of isolating a syntactic criterion characterising the positive definite (i.e., strictly positive) real polynomials. Such a criterion would be a strictly positive analogue to the fact that every positive semidefinite (i.e., non-negative) real polynomial is a sum of squares of rational functions, as established by Artin's positive solution to Hilbert's 17th Problem. We then prove that every positive definite real polynomial is a ratio of a Real Nullstellensatz witness and a positive definite real polynomial. Finally, we conjecture that every positive definite real polynomial is a product of ratios of Real Nullstellensatz witnesses and examine an interesting ramification of this conjecture.
. . Note: This paper contains an obselete description of the RAHD system. {Abstract} Methods for deciding quantifier-free non-linear arithmetical conjectures over \mathbb{R} are crucial in the formal verification of many real-world systems and in formalised mathematics. While non-linear (rational function) arithmetic over \mathbb{R} is decidable, it is fundamentally infeasible: any general decision method for this problem is worst-case exponential in the dimension (number of variables) of the formula being analysed. This is unfortunate, as many practical applications of real algebraic decision methods require reasoning about high-dimensional conjectures. Despite their inherent infeasibility, a number of different decision methods have been developed, most of which have ``sweet spots'' -- e.g., types of problems for which they perform much better than they do in general. Such ``sweet spots'' can in many cases be heuristically combined to solve problems that are out of reach of the individual decision methods when used in isolation. RAHD (``Real Algebra in High Dimensions'') is a theorem prover that works to combine a collection of real algebraic decision methods in ways that exploit their respective ``sweet-spots.'' We discuss high-level mathematical and design aspects of RAHD and illustrate its use on a number of examples.
. . {Abstract} We have constructed a tool for using SMT (SAT Modulo Theories) solvers to discharge verification conditions (VCs) from programs written in the SPARK language. The tool can drive any solver supporting the SMT-LIB standard input language and has API interfaces for some solvers. SPARK is a subset of Ada used primarily in high-integrity systems in the aerospace, defence, rail and security industries. Formal verification of SPARK programs is supported by tools produced by the UK company Praxis High Integrity Systems. We report in this paper on our experience in proving SPARK VCs using the popular SMT solvers CVC3, Yices, Z3 and Simplify. We find that the SMT solvers can prove virtually all the VCs that are discharged by Praxis's prover, and sometimes more. Average run-times of the fastest SMT solvers are observed to be roughly 1-2x that of the Praxis prover. Significant work is sometimes needed in translating VCs into a form suitable for input to the SMT solvers. A major part of the paper is devoted to a detailed presentation of the translations we implement.
. . {Abstract} In this paper we study the structure of the set SAT of all satisfiable propositional logical formulas. In particular we raise the question whether the distribution of SAT within the set A of all propositional formulas exhibits fractal behavior. This answer is of course relative to a metric on A. We show that for one such metric there is strong evidence that the distribution does indeed behave wildly. Next we look at an alternative metric.
. . {Abstract} We shall examine the genesis and proof of the Davis-Putnam-Robinson-Matiyasevich negative solution to Hilbert's Tenth Problem, and then proceed to prove a handful of elementary new results on definability and decidability in <\mathbb{N}, *>. |