First Summer School on Formal Techniques

Formal verification techniques such as model checking, satisfiability, and static analysis have matured rapidly in recent years. These techniques are widely applicable in computing as well as in engineering, biology, and mathematics. This school will focus on the principles and practice of formal verification, with a strong emphasis on the hands-on use of verification technology. It primarily targets graduate students who are interested in using or developing verification technology in their own research.

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.

The lecturers at the school include

• Leonardo de Moura and Bruno Dutertre: Satisfiability Modulo Theories
• Jason Baumgartner: Hardware Verification: Model Checking and Equivalence Checking
• David Monniaux: Static Analysis
• Ken McMillan: Abstraction, Interpolation, and Composition
• Neha Rungta and Peter Mehlitz: Software Verification with Java Pathfinder
• Natarajan Shankar: Interactive Theorem Proving

Students are invited to apply for admission to the school by filling in the form below with name, email, affiliation, education status, graduate advisor, research interests, and the names and emails of two references. We especially welcome applications from women and under-represented minorities.^† Applications must be received by Mar 31, 2011.

Questions on any aspect of the school can be posted here.

^†NOTE: Underrepresented minority refers to blacks, Hispanics, American Indians/Alaska Natives, and Native Hawaiians/Other Pacific Islanders.