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 second edition of the school builds on the success of the first one to develop a well-knit community of young researchers with a deep interest in formal methods.
that was held from May 27 to June 1, 2012, at Menlo College California. The school covers a wide range of topics in the construction and use of formal tools and techniques. Lectures are extremely rigorous and laboratories train students in the hands-on use of formal techniques. The topics covered at a typical summer school include formal logic, theory of computation, specification languages, static and dynamic analysis, invariant generation, satisfiability solvers, automated and interactive proof, hardware and software model checking, compositional verification, cyber-physical systems modeling, and symbolic systems biology.The school was attended by nearly 80 students, mostly from the United States. The lecturers at the school included 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 Natarajan Shankar: Speaking Logic The invited speakers at the school included: Aaron Bradley: IC3 and Beyond: Incremental, Inductive Verification Alex Aiken: New Applications of Underapproximations in Static Analysis Dawn Song: BitBlaze-WebBlaze-DroidBlaze: Automatic Security Analysis in Binary, Web and Android The students participated enthusiastically in the lectures, discussions, and laboratory work. Feedback, mostly positive, from the students was useful in planning the 2013 Summer School on Formal Techniques.
