Formal modeling and verification technology has made significant advances in the last two decades. Techniques like model checking and theorem proving are now used in both the hardware and software industries. Formal techniques are also increasingly being used in scientific modeling, as for example in systems biology and in the engineering of complex cyber-physical systems. The biggest challenge facing this technology is the lack of trained users and developers of this technology. To address this gap, we started the Summer School in Formal Techniques. Two such schools have been organized, during the summers of 2011 and 2012, at Menlo College in Atherton, California. These schools attracted around 80 participants with a diverse range of interests and backgrounds. The lectures were supported by hands-on laboratories. Both schools have been received enthusiastically by the participants. The 2013 Summer School on Formal Techniques continues the work of developing a well-knit community of researchers who are interested in learning cutting-edge techniques in formal modeling and verification. Attendees at the school have the opportunity to present their own research ideas and to interact closely with both the lecturers and other students.

Project Report

Formal modeling and verification technology has made significant advances in the last two decades. Techniques like model checking and theorem proving are now used in both the hardware and software industries. Formal techniques are also increasingly being used in scientific modeling, as for example in systems biology and in the engineering of complex cyber-physical systems. The biggest challenge facing this technology is the lack of trained users and developers of this technology. To address this gap, we started the Summer School in Formal Techniques. The first such school was held in the Summer of 2011 at Menlo College in Atherton, California, with support from the National Science Foundation and SRI International. The school attracted 80 participants with a diverse range of interests and backgrounds. The lectures were rigorous and covered the spectrum of formal techniques including static analysis, model checking, theorem proving, invariant generation, compositional verification, and systems biology. The lectures were supported by hands-on laboratories. Building on the model of the first school, the Second Summer School on Formal Techniques was held in May/June 2012, and also drew around 80 participants. The third Summer School held in May 2013 drew around 60 participants. Like the preceding schools, the third edition of the school was received enthusiastically by the participants. The lecturers included Dr. Cesar Munoz (NASA Langley), Professor Daniel Kroening (Oxford), Dr. Aarti Gupta (NEC Labs), Dr. Leonardo de Moura (Microsoft Research), and Dr. Natarajan Shankar (SRI). We also had invited talks from Dr. Richard Waldinger (SRI) and Dr. Arnaud Venet (NASA Ames). In addition to participating in the lectures and laboratory sessions, the students gave informal presentations of their own ongoing research activities.

Project Start
Project End
Budget Start
2013-04-01
Budget End
2014-03-31
Support Year
Fiscal Year
2013
Total Cost
$90,037
Indirect Cost
Name
Sri International
Department
Type
DUNS #
City
Menlo Park
State
CA
Country
United States
Zip Code
94025