Pre-FSTTCS 2003 Tutorial Workshop

Advances in Model Checking

Tata Institute of Fundamental Research,
Mumbai 400 005.
14, December 2003

  • Motivation and Goals
  • Workshop Speakers
  • Affiliations
  • Venue
  • Arriving at TIFR
  • Coordinators
  • Lecture Schedule
  • Workshop Program
  • Registration and Arrangements
  • Directions and travel information
  • Course Material


  • Motivation and Goals

    This workshop will consist of  tutorial presentations on the theme Advances in Model Checking presented by leading scientists at the forefront of the emerging technology of model checking.
    The talks will focus on current research topics such as SAT solving, Bounded model checking,
    Verification of Infinite State and Timed systems, Abstraction and  Software model checking.

    "Program verification aims at proving that programs meet their specifications, i.e., that the actual program behaviour coincides with the desired one. Model checking refers to algorithmic techniques for program verification. Model checking has been applied  to the verification of temporal properties of reactive and concurrent systems, which has proven successful in the area of  Harware, Protocols and Embedded Systems Controllers verification."

    While explicit state space exploration is used for  model checking systems with small state spaces,
    symbolic model checking based on the Binary Decision Diagrams introduced by Bryant has proved effective in model checking many moderately sized finite state systems. This has found considerable use in Hardware Verification.

    "Since its introduction in 1999 by Biere, Cimatti, Clarke and Zhu, Bounded Model Checking has been adopted as a complementary technique to the more traditional BDD based unbounded symbolic model checking. Largely due to the advances in SAT technology in the last few years, Bounded Model Checking became a leading tool in detection of relatively shallow logical errors, outperforming BDD based tools in most of these cases. The large interest in this technology has created a constant stream of new ideas and improvements that make this technique more and more useful."

    "The growing importance of model checking in hardware verification and the difficulty of producing correct software are driving a growing interest in the application of model checking to software. This leads to many challenges of scientific and practical interest, both in core model checking technology and in supporting techniques, such as program analyses and transformations that help automate abstraction of the data state and reduction of the control state."

    (Excerpts from Recently Held Related Workshops)

    Workshop Speakers

  • Randy Bryant (Carnegie Mellon University)

  •  
  • Alessandro Cimatti (IRST, Trento, Italy)

  •  
  • Sriram Rajamani (Microsoft Research)

  •  

    Workshop Affiliations

    The workshop will be hosted by the Tata Institute of Fundamental Research, Mumbai.
    The workshop is affiliated with  the  FSTTCS 2003 Conference (15-17 December, IIT, Mumbai). It is co-located with the ICLP'03 and ASIAN'03 conferences, (TIFR, Mumbai).

    Venue

    Tata Institute of Fundamental Research
    Homi Bhabha Road, Colaba
    Mumbai 400 005
    India

    Date: 14 December 2003

    Workshop Email:  amcworkshop@tifr.res.in

    How to reach TIFR:  See http://theory.tifr.res.in/misc/reaching_tifr.html

    Arriving at TIFR

    Workshop Coordinators

    Paritosh K. Pandya (Coordinator)
    School of Technology and Computer Science, TIFR
    Homi Bhabha Road, Colaba
    Mumbai 400 005
    India

    Phone: ++91 22 22804545 Ext. 2551
    Email:  pandya@tifr.res.in

    Supratik Chakraborty (Co-cordinator)
    Dept. of Computer Science and Engg.
    IIT Bombay
    Powai, Mumbai 400 076
    Email: Supratik@cse.iitb.ac.in

    Workshop Program

  • Speaker: Randy Bryant  (Carnegie Mellon University)

  • Title:  SAT-Based Decision Procedures for Subsets of First-Order Logic

    Abstract:  Formal verification tools that operate on finite-state system models, such as symbolic model checkers, have gained widespread acceptance in industry due to their ability to handle large scale designs and to require minimal human guidance.  More abstract systems, such as synchronization protocols that work for arbitrary numbers of processes and software programs that  work for arbitrary word and memory sizes, call for tools that can verify  infinite state systems.  Historically, the only way to mechanically verify  such systems was to use a general-purpose, automated theorem prover. This requires considerable effort and expertise on the part of the user.

    A more recent trend has been to create automatic verification tools for infinite-state systems that use specialized decision procedures for subsets  of first-order logic. This talk presents one approach to creating such  decision procedures, in which the first-order formula is translated into a  satisfiability preserving propositional formula.  We then use an existing Boolean satisfiability (SAT) solver to decide the original formula.  This approach exploits the tremendous improvements recent SAT solvers have made  in both efficiency and capacity.

    We describe a very limited class of logic, allowing only uninterpreted  functions with equality.  We then extend this to include "separation  constraints" of the form x <= y + c, where c is an integer constant.  We  describe different techniques for encoding integer constraints into  propositional logic and ways to exploit the structure of the formulas to  greatly improve the efficiency of the decision procedure.
     
     

  • Speaker: Alessandro Cimatti  (IRST, Trento, Italy)

  • Title: Symbolic Model Checking: a SAT-based perspective

    Abstract: The introduction of symbolic techniques has been the enabling factor
    for model checking large sized designs. Traditionally, symbolic model
    checking has been based on Binary Decision Diagrams; more recently,
    Bounded Model Checking has highlighted the potential for symbolic
    techniques based on propositional satisfiability (SAT).

    In the first part of the talk, I will overview the field of symbolic
    model checking, with particular emphasis on SAT-based methods. In the
    second, I will present the MathSAT paradigm, and its applications to
    symbolic model checking. MathSAT extends propositional satisfiability
    to deal with constraints over numerical variables, and provides a
    uniform and efficient way for advanced forms of model checking, such
    as word-level reasoning, and reasoning about Timed and Hybrid systems.
     
     

  • Speaker: Sriram Rajamani  (Microsoft Research)

  • Title: Software Model Checking with SLAM

    Abstract: Model checking is a technique to find bugs in systems be systematically exploring their state spaces. Due to state space explosion, model checkers typically operate on a manually constructed finite-state abstraction of the system. The goal of the SLAM project is to model check software written in common programming languages directly. SLAM has been successfully used to find and fix errors in Windows device drivers written in the C language.

    SLAM operates by automatically constructing and refining model-checkable abstractions (called Boolean Programs) of a C program. The first part of this tutorial will describe how the SLAM project has combined and extended results from the areas of program analysis, model checking and theorem proving to analyze critical properties of systems software written in the C language. The second half of the tutorial will present some of the engineering "secrets" we applied to the basic SLAM process to improve its performance on Windows device drivers.

    SLAM is joint work with Tom Ball, Byron Cook, Vladimir Levin and Jakob Lichtenberg.
     

    Lecture Schedule

    Time  Speaker
    09:15 -- 09:30  Inauguration
    09:30 -- 10:30  Alessandro Cimatti 
    10:30 -- 11:00  Coffee/Tea
    11:00 -- 12:00  Alessandro Cimatti 
    12:00 -- 13:00  Sriram Rajamani
    13:00 -- 14:00  Lunch
    14:00 -- 15:00  Sriram Rajamani
    15:00 -- 16:00  Randy Bryant
    16:00 -- 16:30  Coffee/Tea
    16:30 -- 17:30  Randy Bryant
    17:30 -- 17:45  Concluding Remarks

    Lecture Material

              Please see the web  pages of the speakers for reference material related to their talks.
     

    Registration and Arrangements

          The participants of the FSTTCS 2003 can directly register for the workshop through the FSTTCS 2003 web page. There is no separate fee for participating in the workshop for the FSTTCS participants. A consolidated  request for accomodation at IIT Mumbai should be made for the FSTTCS workshops and the conference with the FSTTCS registration.  We regret that we cannot provide accomodation at TIFR for the workshop.

            A bus will be arranged to bring and take back the workshop participants from IIT Mumbai and the Rodas Hotel (near IIT)  to TIFR on 14th December.  (Timings of this bus and boarding locations will be notified later on this web page.)

            Participants of ICLP/ASIAN conferences and any other participants wishing to attend the workshop must directly communicate with the workshop coordinator by email after 2nd November 2003 but before 9 December 2003.  The email for this should be sent to amcworkshop@tifr.res.in with Subject: Workshop Registration. Approved requests will be acknowldeged. Please do not participate without obtaining such acknowledgement.