CAV on Thursday, August 17th

FLoC Second Opening and Plenary Session (08:45‑10:00)
Chair: Moshe Vardi, Thomas Ball, Wolfram Schulte, Ken McMillan
Location: Metropolitan A/B

08:45‑09:00

Introduction and Welcome

09:00‑10:00

David Dill (Stanford University) I Think I Voted: E-voting vs. Democracy [ppt] Touch-screen voting machines store records of cast votes in internal memory, where the voter cannot check them. Because of our system of secret ballots, once the voter leaves the polls there is no way anyone can determine whether the vote captured was what the voter intended. Why should voters trust these machines? In January 2003, I drafted a "Resolution on Electronic Voting" stating that every voting system should have a "voter verifiable audit trail," which is a permanent record of the vote that can be checked for accuracy by the voter, and which is saved for a recount if it is required. I posted the page with endorsements from many prominent computer scientists. At that point, I became embroiled in a nationwide battle for voting transparency that has continued now for three years. In this talk, I'll explain the basic problems and solutions in electronic voting.

Break (10:00‑10:30)

Session 1: Automata (10:30‑12:00)
Chair: Amir Pnueli

10:30‑11:00	Martin De Wulf (ULB) Laurent Doyen (Université Libre de Bruxelles.) Tom Henzinger (EPFL) Jean-Francois Raskin (ULB) Antichains: A New Algorithm for Checking Universality of Finite Automata We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone operator in the lattice of antichains of location sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata.
11:00‑11:30	Orna Kupferman (Hebrew University) Moshe Y. Vardi (Rice University and Microsoft Research) Nir Piterman (EPFL) Safraless Compositional Synthesis In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. In spite of the rich theory developed for system synthesis, little of this theory has been reduced to practice. This is in contrast with of model-checking theory, which has led to industrial development and use of formal verification tools. We see two main reasons for the lack of practical impact of synthesis. The first is algorithmic: synthesis involves Safra's determinization of automata on infinite words, and a solution of parity games with highly complex state spaces; both problems have been notoriously resistant to efficient implementation. The second is methodological: current theory of synthesis assumes a single comprehensive specification. In practice, however, the specification is composed of a set of properties, which is typically evolving -- properties may be added, deleted, or modified. In this work we address both issues. We extend the Safraless synthesis algorithm of Kupferman and Vardi so that it handles LTL formulas by translating them to nondeterministic generalized Buchi automata. This leads to an exponential improvement in the complexity of the algorithm. Technically, our algorithm reduces the synthesis problem to the emptiness problem of a nondeterministic Buchi tree automaton A. The generation of A avoids determinization, avoids the parity acceptance condition, and is based on an analysis of runs of universal generalized co-Buchi tree automata. The clean and simple structure of A enables optimizations and a symbolic implementation. In addition, it makes it possible to use information gathered during the synthesis process of properties in the process of synthesizing their conjunction.
11:30‑12:00	Sudeep Juvekar (IIT Bombay) Nir Piterman (EPFL) Minimizing Generalized Buchi Automata We consider the problem of minimization of generalized Buchi automata. We extend fair-simulation minimization and delayed-simulation minimization to the case where the Buchi automaton has multiple acceptance conditions. For fair simulation, we show how to efficiently compute the fair-simulation relation while maintaining the structure of the automaton. We then use the fair-simulation relation to merge states and remove transitions. Our fair-simulation algorithm works in time O(mn3k2) where m is the number of transitions, n is the number of states, and k is the number of acceptance sets. For delayed simulation, we extend the existing definition to the case of multiple acceptance conditions. We show that our definition can indeed be used for minimization and give an algorithm that computes the delayed-simulation relation. Our delayed-simulation algorithm works in time O(mn3k). We implemented the two algorithms and report on experimental results.

Session 2: Tools Papers (12:00‑12:30)
Chair: Amir Pnuelo

12:00‑12:15

Luca de Alfaro (University of California, Santa Cruz) Marco Faella (University of Naples) B. Thomas Adler (UCSC) Leandro Dias Da Silva (U Campina Grande) Axel Legay (University of Liege) Vishwanath Raman (UCSC) Pritam Roy (University of California) Ticc: A Tool for Interface Compatibility and Composition We present the tool Ticc(Tool for Interface Compatibility and Composition). In Ticc, a component interface describes both the behavior of a component, and the component's assumptions on the environment's behavior. Ticc can check the compatibility of such interfaces, and analyze their emergent behavior, via a symbolic implementation of game-theoretic algorithms.

12:15‑12:30

Sébastien Bardin (ENS de Cachan) Jerome Leroux (CNRS) Gérald Point (CNRS) FAST Extended Release FAST is a tool designed for the analysis of counter systems, i.e. automata extended with unbounded integer variables. Despite the reachability set is not recursive in general, FAST implements several innovative techniques such as acceleration and circuit selection to solve this problem in practice. In its latest version, the tool is built upon an open architecture: the Presburger library is manipulated through a clear and convenient interface, thus any Presburger arithmetics package can be plugged to the tool. We provide three implementations of the interface using Lash, Mona and a new shared automata package with computation cache. Finally new features are available, like different acceleration algorithms.

Lunch break (12:30‑14:00)

Session 3: Arithmetic (14:00‑15:00)
Chair: Sanjit A. Seshia

14:00‑14:30

Jochen Eisinger (Albert-Ludwigs-Universität Freiburg) Felix Klaedtke (ETH Zurich) Don't Care Words with Application to the Automata-based Approach for Real Addition Automata are a useful tool in infinite-state model checking, since they can represent infinite sets of integers and reals. However, analogous to the use of BDDs to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation. In this paper, we generalize the notion of "don't cares" for BDDs to word languages as a means to reduce the automata sizes. We show that the minimal weak deterministic Büchi automaton (WDBA) with respect to a given don't care set, under certain restrictions, is uniquely determined and can be efficiently constructed. We apply don't cares to improve the efficiency of a decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on WDBAs.

14:30‑15:00

Bruno Dutertre (SRI international) Leonardo de Moura (SRI International) A Fast Linear-Arithmetic Solver for DPLL(T) We present a new Simplex-based linear arithmetic solver that can be integrated efficiently in the DPLL(T) framework. The new solver improves over existing approaches by enabling fast backtracking, supporting a priori simplification to reduce the problem size, and providing an efficient form of theory propagation. We also present a new and simple approach for solving strict inequalities. Experimental results show substantial performance improvements over existing tools that use other Simplex-based solvers in DPLL(T) decision procedures. The new solver is even competitive with state-of-the-art tools specialized for the difference logic fragment.

Session 4: SAT and Bounded Model Checking (15:00‑16:00)
Chair: Clark Barrett

15:00‑15:30

Keijo Heljanko (Laboratory for Theoretical Computer Science, Helsinki University of Technology) Tommi Junttila (Helsinki University of Technology) Misa Keinänen (Laboratory for Theoretical Computer Science, Helsinki University of Technology) Martin Lange (Institut fur Informatik Ludwig-Maximilians-Universitat Munchen) Timo Latvala (Department of Computer Science, University of Illinois at Urbana-Champaign) Bounded Model Checking for Weak Alternating Buchi Automata We present an incremental bounded model checking encoding into propositional satisfiability where the property specification is expressed as a weak alternating Buchi automaton (WABA). The encoding is linear in the specification, or, more exactly O(|I|+k·|T|+k·|d|), where |I| is the size of the initial state predicate, k is the bound, |T| is the size of the transition relation, and |d| is the size of the WABA transition relation. Minimal length counterexamples can also be provided by the approach by increasing the encoding size to be quadratic in the number of states in the largest component of the WABA. The proposed encoding can be used to implement more efficient bounded model checking algorithms for omega-regular industrial specification languages such as Accellera’s Property Specification Language (PSL). Encouraging experimental results on a prototype implementation are reported.

15:30‑16:00

Roman Gershman (Technion) Maya Koifman (Technion) Ofer Strichman (Technion, Haifa) Deriving small unsatisfiable cores with dominators The problem of finding a small unsatisfiable core of an unsatisfiable CNF formula is addressed. The proposed algorithm, Trimmer, iterates over each internal node d in the resolution graph that `consumes' a large number of clauses M (i.e. a large number of original clauses are present in the unsat core only for proving d) and attempts to prove them without the M clauses. If this is possible, it transforms the resolution graph into a new graph that does not have the M clauses at its core. Trimmer can be integrated into a fixpoint framework similarly to Malik and Zhang's fix-point algorithm run-till-fix. We call this option trim-till-fix. Experimental evaluation on a large number of industrial CNF unsatisfiable formulas shows that trim-till-fix doubles, on average, the number of reduced clauses in comparison to run-till-fix. It is also better when used as a component in a bigger system that enforces short timeouts.

Break (16:00‑16:30)

Invited Talk (16:30‑17:30)
Chair: Thomas Ball

16:30‑17:30

Manuvir Das (Microsoft) Formal Specifications on Industrial-Strength Code - From Myth to Reality [ppt] The research community has long understood the value of formal specifications in building robust software. However, the adoption of any specifications beyond run-time assertions in industrial software has been limited. All of this has changed at Microsoft in the last few years. Today, formal specifications are a mandated part of the software development process in the largest Microsoft product groups. Millions of specifications have been added, and tens of thousands of bugs have been exposed and fixed in future versions of products under development. In addition, Windows public interfaces are formally specified and the Visual Studio compiler understands and enforces these specifications, meaning that programmers anywhere can now use formal specifications to make their software more robust. How did this happen? The key ingredients of success were picking a critical programming error that costs software companies real money (buffer overruns), and building an incremental solution in which programmers obtain value proportional to their specification effort. The key technical aspects of this incremental approach include SAL, a lightweight specification language for describing memory access behaviour of C/C++ programs; espX, a heavyweight modular checker that enforces consistency between the code and the specification and validates memory accesses; and SALinfer, a lightweight global analysis that infers and inserts a large fraction of the memory specifications automatically. The goal of this talk is to share the technical story of the insights that enabled SAL, espX and SALinfer, as well as the social and practical story of how we were able to move organizations with thousands of programmers to an environment where the use of specifications is routine.