2014 SAT/SMT Summer School

New York University, New York NY

Investigators

Abstract

Formal methods have made significant advances during the last decade, and now form the backbone of formal assurance across hardware and software industries. Underlying many of these techniques is the capability to effectively reason about system properties, often by describing the properties as constraint satisfaction problems and delegating the reasoning to a constraint solver. The most common constraint reasoning engines in use today are satisfiability (modulo theories) solvers (SAT and SMT). As a rapidly developing field, there is a lack of highly trained users and researchers that will sustain and further advance the field. The SAT/SMT summer school addresses this issue by familiarizing young researchers with cutting-edge solver technologies and their applications. The SAT/SMT summer school addresses this issue by familiarizing young researchers with cutting-edge solver technologies and their applications. The lecturers at the school are world-renown experts, and the three day gathering gives the students the opportunity to discuss the lecture topics, their own research, and the challenges and future directions with these experts. The material is covered rigorously, with depth and breadth, but at a pace appropriate for a student audience, making the school a unique place for disseminating new research to the future users and researchers.