IJCAR on Sunday, July 18th

09:00‑10:00 Induction
Location: AT LT5
09:00 Markus Aderhold
Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion

In order to support the verification of programs, verification tools such as ACL2 or Isabelle try to extract suitable induction axioms from the definition of terminating, recursively defined procedures. However, these extraction techniques have difficulties with procedures that are defined by second-order recursion: There a first-order procedure 'f' passes itself as an argument to a second-order procedure like 'map', 'every', 'foldl', 'foldr', etc., which leads to indirect recursive calls. For instance, second-order recursion is commonly used in implementations of algorithms on data structures such as terms (variadic trees). We present a method to automatically extract induction axioms from such procedures. Furthermore, we describe how the induction axioms can be optimized (i.e., generalized and simplified). An implementation of these methods demonstrates that our approach facilitates straightforward inductive proofs in a verification tool.

09:30 David Baelde, Dale Miller and Zachary Snow
Focused Inductive Theorem Proving

Focused proof systems provide means for reducing and structuring the non-determinism involved in searching for sequent calculus proofs. We present a focused proof system for a first-order logic with inductive and co-inductive definitions in which the introduction rules are partitioned into an asynchronous phase and a synchronous phase. These focused proofs allows us to naturally see proof search as being organized around interleaving intervals of computation and more general deduction. For example, entire Prolog-like computations can be captured using a single synchronous phase and many model-checking queries can be captured using an asynchronous phase followed by a synchronous phase. Leveraging these ideas, we have developed an interactive proof assistant, called Tac, for this logic. We describe its high-level design and illustrate how it is capable of automatically proving many theorems using induction and coinduction. Since the automatic proof procedure is structured using focused proofs, its behavior is often rather easy to anticipate and modify. We illustrate the strength of Tac with several examples of proof developments, some achieved entirely automatically and others achieved with user guidance.

10:30‑12:30 Decision Procedures
Location: AT LT5
10:30 Vincent Aravantinos, Ricardo Caferra and Nicolas Peltier
A Decidable Class of Nested Iterated Schemata

Many problems can be specified by patterns of propositional formulae depending on a parameter, e.g. the specification of a circuit usually depends on the number of bits of its input. We define a logic whose formulae, called \emph{iterated schemata}, allow to express such patterns. Schemata extend propositional logic with indexed propositions, e.g. $P_i$, $P_{i+1}$, $P_1$ or $P_n$, and with generalized connectives, e.g. $\bigwedge_{i=1}^n$ or $\bigvee_{i=1}^n$ where $n$ is an (unbound) integer variable called a \emph{parameter}. The expressive power of iterated schemata is strictly greater than propositional logic: it is even out of the scope of first-order logic. We define a proof procedure, called DPLL*, in the spirit of the DPLL procedure, able to prove that a schema is satisfiable for at least one value of its parameter. But proving that a schema is unsatisfiable \emph{for every value of the parameter}, has been shown to be undecidable so DPLL* does not terminate in general. Still, DPLL* terminates for schemata of a syntactic subclass called \emph{regularly nested}.

11:00 Vincent Aravantinos, Ricardo Caferra and Nicolas Peltier
RegSTAB: a SAT-Solver for Propositional Schemata

We describe the system REGSTAB (for REGular Schemata TABleau) that solves the satisfiability problem for a class of propositional schemata. Our formalism extends propositional logic by considering \emph{indexed propositions} (such as $P_1,P_i,P_{j+1},\ldots$) and \emph{iterated connectives} (e.g. $\bigvee_{i=1}^n \phi$). The indices and bounds are linear arithmetic expressions (possibly containing variables, interpreted as integers). Our system allows one to check the satisfiability of sequences of formulae such as $(\bigvee_{i=1}^n P_i) \wedge (\bigwedge_{i=1}^n \neg P_i)$.

11:15 Nikolaj Bjørner
Linear Quantifier Elimination as an Abstract Decision Procedure

This paper develops abstract quantifier elimination procedures for linear arithmetic over the reals and integers. They are formulated as theory solvers in the context of an abstract DPLL-based search. The resulting procedures allow the solvers to maintain integral control of the search process. We also offer evidence that our procedure for Presburger arithmetic offers compelling advantages.

11:45 Oliver Friedmann, Markus Latte and Martin Lange
A Decision Procedure for CTL* Based on Tableaux and Automata

We present a decision procedure for the full branching-time logic CTL* which is based on tableaux with global conditions on infinite branches. These conditions can be checked using automata-theoretic machinery. The decision procedure then consists of a doubly exponential reduction to the problem of solving a parity game. This has advantages over existing decision procedures for CTL*, in particular the automata-theoretic ones: the underlying tableaux only work on subformulas of the input formula. The relationship between the structure of such tableaux and the input formula is given by very intuitive tableau rules. Furthermore, runtime experiments with an implementation of this procedure in the MLSolver tool show the practicality of this approach within the limits of the problem's computational complexity of being 2EXPTIME-complete.

12:15 Filip Maric and Predrag Janicic
URBiVA: Uniform Reduction to Bit-Vector Arithmetic

We describe a system URBIiVA for specifying and solving a range of problems by uniformly reducing them to bit-vector arithmetic (BVA). A problem description is given in a C-like specification language and this high-level specification is transformed to a BVA formula by symbolic execution. The formula is passed to a BVA solver and if it is satisfiable, its models give solutions of the problem. The system can be used for efficient modeling (specifying and solving) of a wide class of problems. Several state-of-the-art solvers for BVA are currently used (Boolector, MathSAT, Yices) and additional solvers can be easily included. Hence, the system can be used not only a specification and solving tool, but also as a platform for evaluation and comparison between BVA solvers.

14:00‑15:00 FLoC Keynote Talk: Deepak Kapur
Location: George Square Lecture Theatre
14:00 Deepak Kapur (University of New Mexico)
Induction, Invariants, and Abstraction

Invariants play a key role in verifying properties of imperative programs. Inductive reasoning is essential to verifying properties of recursive programs. Relationship between derivation of loop invariants and speculation of lemmas in inductive reasoning is explored. Abstraction is an effective heuristic for approximating program behavior in order to derive invariants. Interaction among developing abstractions, inductive reasoning, and generating invariants is investigated.

15:30‑17:00 Arithmetic
Location: AT LT5
15:30 Jonathan Abourbih, Luke Blaney, Alan Bundy and Fiona McNeill
A Single-Significant-Digit Calculus for Semi-Automated Guesstimation

We describe a single-significant-digit calculus for estimating approximate solutions to guesstimation problems. The calculus is formalised as a collection of proof methods, which are combined into proof plans. These proof methods have been implemented and successfully evaluated in a system, GORT, which forms a customised proof plan for each problem and then executes the plan to obtain a solution.

16:00 Hicham Bensaid, Ricardo Caferra and Nicolas Peltier
Perfect discrimination graphs: indexing terms with integer exponents

Perfect discrimination trees are used by many efficient resolution and superposition-based theorem provers (e.g. E-prover, Waldmeister, Logic Reasoner, ...) in order to efficiently implement rewriting and unit subsumption. In this paper, we extend this indexing technique to handle a class of terms with integer exponents (or I-terms), a schematisation language that has been proposed to capture sequences of iterated patterns. We provide an algorithm to construct the so called perfect discrimination graphs from I-terms and to retrieve indexed I-terms from their instances. Our research is essentially motivated by some approaches to inductive proofs, for which termination of the proof procedure is capital.

16:30 Angelo Brillout, Daniel Kroening, Philipp Rümmer and Thomas Wahl
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic

Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis. Interpolants are typically determined by annotating the steps of an unsatisfiability proof with partial interpolants. In this paper, we consider Craig interpolation for full quantifier-free Presburger arithmetic (QFPA), for which currently no efficient interpolation procedures are known. Closing this gap, we introduce an interpolating sequent calculus for QFPA and prove it to be sound and complete. We then add uninterpreted predicates to the calculus, thus extending it to important theories such as arrays and uninterpreted functions. We demonstrate the efficiency of our interpolation procedure on a large range of publicly available benchmarks.

17:10‑17:50 Business Meeting
Location: AT LT5
17:10 IJCAR Business Meeting