PDPAR on Monday, August 21st

Session 1 (09:30‑10:30)

09:30‑10:30

Peter O'Hearn (Queen Mary, University of London) Proof Procedures for Separated Heap Abstractions Separation logic is a program logic geared towards reasoning about programs that mutate heap-allocated data structures. This talk describes ideas arising from joint work with Josh Berdine and Cristiano Calcagno on proof procedure for a sublogic of separation logic that is oriented to lightweight program verification and analysis. The proof theory uses ideas from substructural logic together with induction-free reasoning about inductive definitions of heap structures. Substructural reasoning is used to to infer frame axioms, which describe the portion of a heap that is not altered by a procedure, as well as to discharge verification conditions; more precisely, the leaves of failed proofs can give us candidate frame axioms. Full automation is achieved through the use of special axioms that capture properties that would normally be proven using by induction. I will illustrate the proof method through its use in the Smallfoot static assertion checker, where it is used to prove verification conditions and infer frame axioms, as well as in the Space Invader program analysis, where it is used to accelerate the convergence of fixed-point calculations.

Break (10:30‑11:00)

Session 2 (11:00‑12:30)

11:00‑11:30	Sava Krstic (Intel Corporation) Robert Jones (Intel) John O'Leary (Intel) Mothers of Pipelines We present a novel method for pipeline verification using SMT solvers. It is based on a non-deterministic ``mother pipeline'' machine (MOP) that abstracts the instruction set architecture (ISA). The MOP vs. ISA correctness theorem splits naturally into a large number of simple subgoals. This theorem reduces proving the correctness of a given pipelined implementation of the ISA to verifying that each of its transitions can be modeled as a sequence of MOP state transitions.
11:30‑12:00	Swen Jacobs (Max Planck Institute for Computer Science, Saarbruecken) Viorica Sofronie-Stokkermans (Max Planck Institute for Computer Science) Applications of hierarchical reasoning in the verification of complex systems In this paper we show how hierarchical reasoning can be used to verify properties of complex systems. Chains of local theory extensions are used to model a case study taken from the European Train Control System (ETCS) standard, but considerably simplified. We show how testing invariants and bounded model checking can automatically be reduced to checking satisfiability of ground formulae over a base theory.
12:00‑12:15	Ofer Strichman (Technion, Haifa) Daniel Kroening (ETH Zurich) A Framework for Decision Procedures in Program Verification Program analysis tools for modern programming languages require a very rich logic to reason about constructs such as bit-vector operators or dynamic data structures. We propose a generic framework for reducing decidable decision problems to propositional logic that starts with an axiomatization of the logics. Instantiating the framework for a specific logic requires a deductive decision procedure that fulfills several conditions. Linear arithmetic, the theory of arrays and other logics useful for verification, have such a decision procedure, as we show. Further, the framework allows to reduce combined theories to a unified propositional formula, which enables learning across theories. We conclude by presenting several challenges that need to be met for making the framework more general and useful for program verification.
12:15‑12:30	Geoffrey Brown (Indiana University CS) Lee Pike (Galois Connections) Easy Parameterized Verificaton of Biphase Mark and 8N1 Protocols The Biphase Mark Protocol (BMP) and 8N1 Protocol are physical layer protocols for data transmission. We present a generic model in which timing and error values are parameterized by linear constraints, and then we use this model to verify these protocols. The verifications are carried out using SRI's SAL model checker that combines a satisfiability modulo theories decision procedure with a bounded model checker for highly-automated induction proofs of safety properties over infinite-state systems. Previously, parameterized formal verification of real-time systems required mechanical theorem-proving or specialized real-time model checkers; we describe a compelling case-study demonstrating a simpler and more general approach. The verification reveals a significant error in the parameter ranges for 8N1 given in a published application note.

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:30)

14:00‑15:00	Koen Claessen (Chalmers University of Technology and Jasper Design Automation) The Power of Finite Model Finding [ppt] Paradox is a tool that automatically finds finite models for first-order logic formulas, using incremental SAT. In this talk, I will present a new look on the problem of finding finite models for first-order logic formulas. In particular, I will present a novel application of finite model finding to the verification of finite and infinite state systems; here, a finite model finder can be used to automatically find abstractions of systems for use in safety property verification. In this verification process, it turns out to be vital to use typed (or sorted) first-order formulas. Finding models for typed formulas brings the freedom to use different domain sizes for each type. How to choose these different domain sizes is still very much an unexplored problem. We show how a simple extension to a SAT-solver can be used to guide the search for typed models with several domains of different sizes.
15:00‑15:15	Chao Wang (NEC Laboratories America) Aarti Gupta (NEC Laboratories USA) Malay Ganai (NEC Laboratories USA) Predicate Learning and Selective Theory Deduction for Solving Difference Logic Design and verification of systems at the Register-Transfer (RT) or behavioral level require the ability to reason at higher levels of abstraction. Difference logic consists of an arbitrary Boolean combination of propositional variables and difference predicates and therefore provides an appropriate abstraction. In this paper, we present several new optimization techniques for efficiently deciding difference logic formulas. We use the lazy approach by combining a DPLL Boolean SAT procedure with a dedicated graph-based theory solver, which adds transitivity constraints among difference predicates on a ``need-to'' basis. Our new optimization techniques include flexible theory constraint propagation, selective theory deduction, and dynamic predicate learning. We have implemented these techniques in our lazy solver. We demonstrate the effectiveness of the proposed techniques on public benchmarks through a set of controlled experiments.
15:15‑15:30	Silvio Ghilardi (Dipartimento di Informatica, Università degli Studi di Milano (Italia)) Enrica Nicolini (Università degli Studi di Milano) Silvio Ranise (LORIA-INRIA Lorraine and Universita degli Studi di Milano) Daniele Zucchelli (Università degli Studi di Milano) Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.

Break (15:30‑16:00)

Session 4 (16:00‑17:45)

16:00‑16:30	Behzad Akbarpour (University of Cambridge) Lawrence Paulson (University of Cambridge) Towards Automatic Proofs of Inequalities Involving Elementary Functions Inequalities involving functions such as sines, exponentials and logarithms lie outside the scope of decision procedures, and can only be solved using heuristic methods. Preliminary investigations suggest that many such problems can be solved by reduction to algebraic inequalities, which can then be decided by a decision procedure for the theory of real closed fields (RCF). The reduction involves replacing each occurrence of a function by a lower or upper bound (as appropriate) typically derived from a power series expansion. Typically this requires splitting the domain of the function being replaced, since most bounds are only valid for specific intervals.
16:30‑17:00	Maria Paola Bonacina (Universita` degli Studi di Verona) Mnacho Echenim (Università degli Studi di Verona) Rewrite-Based Satisfiability Procedures for Recursive Data Structures The superposition calculus SP is an inference system for first-order logic with equality that has been used to devise decision procedures for several theories of data structures. These decision procedures are obtained by proving that any fair strategy based on SP terminates on any input that includes the axioms of the theory and the ground literals to be tested. In this paper, we consider the class of theories defining recursive data structures, that might appear out of reach for this approach, because they are defined by an infinite set of axioms. We overcome this obstacle by designing a problem reduction that allows us to prove a general termination result for all these theories.
17:00‑17:30	Clark Barrett (New York University) Igor Shikanian (New York University) Cesare Tinelli (University of Iowa) An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types The theory of recursive data types is a valuable modeling tool for software verification. In the past, decision procedures have been proposed for both the full theory and its universal fragment. However, previous work has been limited in various ways. In this paper, we present a general algorithm for the universal fragment. The algorithm is presented declaratively as a set of abstract rules which are terminating, sound, and complete. We show how other algorithms can be realized as strategies within our general framework. Finally, we propose a new strategy and give experimental results showing that it is significantly faster than other strategies.
17:30‑17:45	Silvio Ranise (LORIA-INRIA & U. Milano) Christophe Ringeissen (LORIA-INRIA) Duc-Khanh Tran (LORIA-INRIA) Producing Conflict Sets for Combinations of Theories Recently, it has become evident that the capability of computing conflict sets is of paramount importance for the efficiency of systems for Satisfiability Modulo Theories (SMT). In this paper, we consider the problem of modularly constructing conflict sets for a combined theory, when this is obtained as the disjoint union of many component theories for which satisfiability procedures capable of computing conflict sets are assumed available. The key idea of our solution to this problem is the concept of explanation graph, which is a labelled, acyclic and undirected graph capable of recording the entailment of some elementary equalities. Explanation graphs allow us to record the explanations computed by, for instance, a proof-producing congruence closure and to extend the well-known Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We study how the computed conflict sets relate to an appropriate notion of minimality.

Discussion (17:45‑18:30)

17:45‑18:30

Discussion