Overview

Model checking technology arguably ranges among the foremost applications of logic to computer science and computer engineering. In the twenty-five years since its invention, model checking has achieved multiple breakthroughs, bridging the gap between theoretical computer science, hardware and software engineering. Today, model checking is extensively used in the hardware industry, and has become feasible for verifying many types of software as well. Model checking has been introduced into computer science curricula at universities worldwide, and virtually has become a universal tool for the analysis of systems. As the number of research groups and conferences in model checking is steadily increasing, the symposium will focus on the state of the art and the future challenges in model checking, seen through the eyes of the leading researchers which have shaped the field during the last decades. The symposium will consist of invited lectures delivered by leading researchers in the field of model checking. The invited speakers are encouraged to reflect the state of the art in their respective field of expertise, and to focus on the most important and exciting future research directions.

Program

• 25MC program
• 25MC pre-proceedings

ACM Sponsored Lunch/Panel

The distinguished Kanellakis award was given twice to model checking pioneers: The 1988 ACM Kanellakis award winners were Randy Bryant, Ed Clarke, Allen Emerson, and Ken McMillan. The 2006 ACM Kanellakis award winners are Gerard Holzmann, Robert Kurshan, Moshe Vardi, and Pierre Wolper. The panel chair is Orna Grumberg.

The panel is sponsored by ACM Distinguished Lectureship Program - a program that encourages technical education and dissemination of technical information.

Organizers / Editors

• Orna Grumberg, Technion Haifa, Israel
• Helmut Veith, Technische Universität München, Germany

Sponsor