2009 CAV award announcement

The 2009 CAV (Computer-Aided Verification) award was presented to seven individuals who made major advances in creating high-performance Boolean satisfiability solvers. This annual award recognizes a specific fundamental contribution or series of outstanding contributions to the CAV field.     

2010 CAV award announcement

The 2010 CAV (Computer-Aided Verification) award was awarded to Kenneth L. McMillan of Cadence Research Laboratories for a series of fundamental contributions resulting in significant advances in scalability of model checking tools. The annual award recognizes a specific fundamental contribution or a series of outstanding contributions to the CAV field.     

Introductory paper

This special section is devoted to a selection of contributions originally presented at the 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002), which took place in Brno, Czech Republic in September 2002 as a satellite event of the 13th conference on concurrency theory (CONCUR 2002). The growing importance of automated formal verification in industry is driving a growing interest in those aspects that have a direct impact on its applicability to real-world problems. One of the main technical challenges is in devising tools that allow one to handle large state spaces. In the last several years numerous approaches to solving this problem have been developed. Recently there has been increasing interest in parallelizing and distributing verification techniques. Papers that appear in this special section provide an interesting sampling of typical approaches in this direction.     

A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits

This paper presents a scalable method for parallelizing symbolic reachability analysis on a distributed-memory environment of workstations. We have developed an adaptive partitioning algorithm that significantly reduces space requirements. The memory balance is maintained by dynamically repartitioning the state space throughout the computation. A compact BDD representation allows coordination by shipping BDDs from one machine to another. This representation allows for different variable orders in the sending and receiving processes. The algorithm uses a distributed termination protocol, with none of the memory modules preserving a complete image of the set of reachable states. No external storage is used on the disk. Rather, we make use of the network, which is much faster.We implemented our method on a standard, loosely-connected environment of workstations, using a high-performance model checker. Initial performance evaluation of several large circuits shows that our method can handle models too large to fit in the memory of a single node. The partitioning algorithm achieves reduction in space, which is linear in the number of workstations employed. A corresponding decrease in space requirements is measured throughout the reachability analysis. Our results show that the relatively slow network does not become a bottleneck, and that computation time is kept reasonably small.     

Test sequence generation and model checking using dynamic transition relations

The task of finding a set of test sequences that provides good coverage of industrial circuits is infeasible because of the size of the circuits. For small critical subcircuits of the design, however, designers can create a set of test sequences that achieve good coverage. These sequences cannot be used on the full design because the inputs to the subcircuit may not be accessible. In this work we present an efficient test generation algorithm that receives a test sequence created for the subcircuit and finds a test sequence for the full design that reproduces the given sequence on the subcircuit. The algorithm uses a new technique called dynamic transition relations to increase its efficiency .The most common and most expensive step in our algorithm is the computation of the set of predecessors of a set of states. To make this computation more efficient we exploit a partitioning of the transition relation into a set of simpler relations. At every step we use only those that are necessary, resulting in a smaller relation than the original one. A different relation is used for each step, hence the name dynamic transition relations. The same idea can be used to improve symbolic model checking for the temporal logic CTL.We have implemented the new method in SMV and run it on several large circuits. Our experiments indicate that the new method can provide gains of up to two orders of magnitude in time and space during verification. These results show that dynamic transition relations can make it possible to verify circuits that were previously unmanageable due to their size and complexity .     

Preface: Volume 23, Issue 2

This volume contains the proceedings of the First International Workshop on Symbolic Model Checking (SMC'99), held in Trento, Italy, on July 6, 1999, as part of the Second Federated Logic Conference (FLoC'99).Symbolic model checking is a formal technique for the verification of finite-state concurrent systems. Symbolic model checkers (e.g. SMV, VIS) have been used to verify industrial systems, ranging from hardware to communication protocols to safety critical plants and procedures. Symbolic model checking is the core technique for several industrial verification tools, and is applied in technology transfer projects. The aim of the SMC'99 workshop is to bring together active developers and users of symbolic model checkers, compare state of the art model checking techniques (e.g. compositional reasoning, abstraction, partitioning), discuss experimental results and experience reports, and promising directions for future research.Nine contributions (out of twenty-two submissions) were selected for presentation by the program committee. The workshop program is completed by two keynote invited lectures, given by Ken McMillan (Cadence Labs, USA) on Compositional Reasoning and Abstraction, and Fabio Somenzi (University of Colorado, USA) on Symbolic State ExplorationThanks are due to a number of people who helped to organize and plan the workshop. Among this group are the Program Committee members:

Adnan Aziz	(University of Texas at Austin, USA)
Armin Biere	(Verysys)
Sergio Campos	(Federal University of Minas Gerais, Brazil)
Alessandro Cimatti	(IRST, Italy)
Edmund Clarke	(Carnegie Mellon University, USA)
Danny Geist	(IBM Haifa, Israel)
Fausto Giunchiglia	(IRST, Italy)
Orna Grumberg	(Technion, Israel)
Markus Kaltenbach	(Siemens, Germany)
Carl Pixley	(Motorola, USA)

Full-size table

The following people helped in the evaluation of the submissions: Yael Abarbanel-Vinov, Neta Aizenbud-Reshef, Shoham Ben-David, Doron Bustan, Jorge Cuellar, David Deharbe, Cindy Eisner, Ranan Fraer, Edelweis Garcez, Leonid Gluhovsky, Marcelo Glusman, Jae-Young Jang, Shmuel Katz, Sharon Keidar, Monika Maidl, Robi Malik, Anamaria Martins Moreira, Shiri Moran, Peter Päppinghaus, Marco Roveri, Peter Warkentin, Karen Yorav, Jun Yuan, Yunshan Zhu.We would like to thank IBM Haifa Research Laboratory for the financial support to SMC'99. Carola Dori, Morena Carli, Marco Roveri and Adolfo Villafiorita helped in several matters related to the local organization. Finally, we are grateful to Michael Mislove for his constat support during the preparation of this electronic volume.Alessandro Cimatti and Orna Grumberg, Guest Editors     

Distributed Symbolic Model Checking for μ-Calculus

In this paper we propose a distributed symbolic algorithm for model checking of propositional μ-calculus formulas. μ-calculus is a powerful formalism and μ-calculus model checking can solve many problems, including, for example, verification of (fair) CTL and LTL properties. Previous works on distributed symbolic model checking were restricted to reachability analysis and safety properties. This work thus significantly extends the scope of properties that can be verified distributively, enabling us to use them for very large designs.The algorithm distributively evaluates subformulas. It results in sets of states which are evenly distributed among the processes. We show that this algorithm is scalable and therefore can be implemented on huge distributed clusters of computing nodes. The memory modules of the computing nodes collaborate to create a very large memory space, thus enabling the checking of much larger designs. We formally prove the correctness of the parallel algorithm. We complement the distribution of the state sets by showing how to distribute the transition relation.This research was supported by The Israel Science Foundation (grant number 111/01-2) and by a grant from Intel Academic Relations.     

SaBRe: load-time selective binary rewriting

Binary rewriting consists in disassembling a program to modify its instructions. However, existing solutions suffer from shortcomings in terms of soundness and performance. We present SaBRe, a load-time system for selective binary rewriting. SaBRe rewrites specific constructs—particularly system calls and functions—when the program is loaded into memory, and intercepts them using plugins through a simple API. We also discuss the theoretical underpinnings of disassembling and rewriting. We developed two backends—for x86_64 and RISC-V—which were used to implement three plugins: a fast system call tracer, a multi-version executor, and a fault injector. Our evaluation shows that SaBRe imposes little overhead, typically below 3%.

     

Assume,guarantee or repair: a regular framework for non regular properties

We present Assume-Guarantee-Repair (AGR)—a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs—these are simple C-like programs, extended with synchronous actions over communication channels. Our method, which consists of a learning-based approach to assume–guarantee reasoning, performs verification and repair simultaneously: in every iteration, AGR either makes another step towards proving that the (current) system satisfies the required properties, or alters the system in a way that brings it closer to satisfying the properties. To handle infinite-state systems we build finite abstractions, for which we check the satisfaction of complex properties that contain first-order constraints, using both syntactic and semantic-aware methods. We implemented AGR and evaluated it on various communication protocols. Our experiments present compact proofs of correctness and quick repairs.