[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Second Summer School on Formal Techniques, May 27-June 1, 2012

Second Summer School on Formal Techniques
May 27- June 1, 2012
Menlo College, Atherton, CA

Formal verification techniques such as model checking, satisfiability, and
static analysis have matured rapidly in recent years. This school, the
second in the series, will focus on the principles and practice of formal
verification, with a strong emphasis on the hands-on use and development of
this technology. It primarily targets graduate students and young
researchers who are interested in using verification technology in their own
research in computing as well as engineering, biology, and
mathematics. Students at the school will have the opportunity to experiment
with the tools and techniques presented in the lectures.

The first Summer Formal school (SSFT11; http://fm.csl.sri.com/SSFT11) was
held in May 2011. This year, the school starts on Sun May 27 with a
background course on Logic in Computer Science taught by Natarajan Shankar
(SRI). The course is optional but highly recommended - it covers the
prerequisites for the main lectures.

We have NSF support for the travel and accommodation for students from US
universities, but welcome applications from graduate students at non-US
universities as well. Non-US students will have to cover their travel and
lodging expenses (around $500). The deadline for applications is April
30. Non-US students requiring US visas are requested to apply early (by
April 15).  Interested students can submit their application at

The lecturers at the school include

    Leonardo de Moura (MSR Redmond) and Bruno Dutertre (SRI):
            Satisfiability Modulo Theories
    Sumit Gulwani (MSR):
            Dimensions in Program Synthesis
    Daniel Kroening (Oxford):
            Verifying Concurrent Programs
    Ken McMillan:
            Abstraction, Decomposition, and Relevance
    Corina Pasareanu, Dimitra Giannakopoulou, Neha Rungta, Peter Mehlitz, and Oksana Tkachuk:
            Verifying Components in the Right Context

The school will also include invited talks by distinguished researchers.
The SSFT Steering Committee consists of Tom Ball (MSR Redmond), Lenore Zuck
(UIC), and Natarajan Shankar (SRI).