Invited Speakers

  • Invited talks
    • David Harel (Weizmann Institute)
      A Grand Challenge: Towards Full Reactive Modeling of a Multi-Cellular Animal
    • Sriram K. Rajamani (Microsoft Research)
      Zing: Exploiting Program Structure for Model Checking Concurrent Software
      Authors: Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof and Yichen Xie

      Abstract: Model checking is a technique for finding bugs in systems by systematically exploring their state spaces. We wish to extract sound models from concurrent programs automatically and check the behaviors of these models systematically. The ZING project is an effort to build a flexible infrastructure to represent and model check abstractions of large concurrent software. To support automatic extraction of models from programs written in common programming languages, ZING's modeling language supports three facilities present in modern programming languages: (1) procedure calls with a call-stack, (2) objects with dynamic allocation, and (3) processes with dynamic creation, using both shared memory and message passing for communication. We believe that these three facilities capture the essence of model checking modern concurrent software. Building a scalable model-checker for such an expressive modeling language is a huge challenge. ZING's modular architecture provides a clear separation between the expressive semantics of the modeling language, and a simple view of ZING programs as labeled transition systems. This separation has allowed us to decouple the design of efficient model checking algorithms from the complexity of supporting rich constructs in the modeling language. ZING's model checking algorithms have been designed to exploit existing structural abstractions in concurrent programs such as processes and procedure calls. We present two such novel techniques in the paper: (1) compositional checking of ZING models for message-passing programs using a conformance theory inspired by work in the process algebra community, and (2) a new summarization algorithm, which enables ZING to reuse work at procedure boundaries by extending interprocedural data-flow analysis algorithms from the compiler community to analyze concurrent programs.

  • Tutorials
    • Steve Brookes (Carnegie-Mellon) and Peter O'Hearn (Queen Mary University of London)
      Resources, Concurrency and Local Reasoning

      Abstract: Resource has always been a central concern in concurrent programming. Often, a number of processes share access to system resources such as memory, processor time, or network bandwidth, and correct resource usage is essential for the overall working of a system. In the 1960s and 1970s Dijkstra, Hoare and Brinch Hansen attacked the problem of resource control in their basic works on concurrent programming. In addition to the use of synchronization mechanisms to provide protection from inconsistent use, they stressed the importance of resource separation as a means of controlling the complexity of process interactions and reducing the possibility of time-dependent errors.

      The intervening years have seen the development of resource-oriented logics such as linear logic and BI. This work uses one such logic, separation logic (a species of BI), to revisit the problem of reasoning about resources in imperative concurrent programs. We use the separating conjunction connective to partition the portions of state used by different processes. The resulting proof method is modular, in the sense that assertions make local remarks about the resources used by program components, instead of global remarks about the entire system state. The first part of the tutorial, by O'Hearn, describes the basic ideas, and illustrates it with programs that transfer ownership of portions of state between processes. Examples include resource pools, efficient message passing, and semaphores programs (where a semaphore is dynamically ``attached'' to a portion of state that it owns). The second part of the tutorial, by Brookes, provides a foundation for the method using a denotational model. In addition to soundness, the model shows that any program that gets past the proof rules does not have a race condition, where different processes attempt to access the same portion of state without explicit synchronization.

    • Bengt Jonsson (Uppsala)
      Regular Model Checking

      Abstract: Regular model checking is being developed for algorithmic verification of several classes of infinite-state systems whose configurations can be modeled as words over a finite alphabet. Examples include parameterized systems consisting of an arbitrary number of homogeneous finite-state processes connected in a linear or ring-formed topology, and systems that operate on queues, stacks, integers, and other linear data structures. The main idea is to use regular languages as the representation of sets of configurations, and finite-state transducers to describe transition relations. In general, the verification problems considered are all undecidable, so the work has consisted in developing semi-algorithms, and decidability results for restricted cases. This tutorial explains some of the work that has been performed so far, some of its applications, and gives comparisons with other frameworks for analyzing parameterized structures, such as shape analysis and rewriting.