• Mohua Banerjee, IIT Kanpur
    Modal logic and algebra

  • Kamal Lodaya, The Institute of Mathematical Sciences
    Logic and definability on words and trees
    [Abstract +]

    In this course we discuss logic on models which are finite words (coloured linear orders), finite trees and generalizations. A set of models is called a “language”, and definability of languages by formulae will also be covered. First order logic, monadic second order logic and temporal logics can all be used to specify requirements that the models must satisfy. We discuss the motivation for using these different formalisms.

  • Alexander Rabinovich, Tel Aviv University
    Church synthesis problem and extensions
    Talk 1 | Talk 2 | Talk 3 | Talk 4

  • Natarajan Shankar, SRI International Computer Science Laboratory, Menlo Park USA
    Automated Formal Methods with PVS, SAL, and Yices
    [Abstract +] | Slides

    Formal verification employs logic to model the actual and intended behavior of computation systems, and uses logical inference to prove or refute the desired properties of these behaviors. Techniques for formal verification range from interactive proof checking to automated techniques based on theorem proving, satisfiability solving, and model checking. We review the basic foundations of logic and then examine the techology for interactive and automated verification as implemented in the PVS interactive theorem prover, the SAL model checker, and the Yices SMT solver. The use of these verification systems will be be illustrated through a range of examples.

    1. Logical foundations
    2. Basic interactive proofs with PVS
    3. Advanced features of PVS
    4. Model checking with SAL
    5. Satisfiability checking with Yices

  • Registration closed
  • Dates
  • Registration deadline:
    December 15, 2011
  • Conference dates:
    January 9–20, 2012
  • Contact
  • ali at