As tliis volume is going to print, model checking is attracting worldwide media attention, and we are celebrating the ACM Turing Award 2007 for the paradigm-shifting work initiated a quarter century ago. Today, model checking technology evidently ranges among the foremost applications of logic to computer science and computer engineering. The model checking community has achieved multiple breakthroughs, bridging the gap between theoretical computer science, hardware and software engineering, and is reaching out to new challenging areas such as systems biology and hybrid systems. 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 and electrical engineering curricula at universities worldwide, and has become a universal tool for the analysis of systems.This volume presents a collection of invited papers based on talks at the symposium u25 Years of Model Checking (25MC).'' In addition, we have included facsimile reprints of the two visionary papers on model checking by Edmund Clarke, Allen Emerson, Jean-Pierre Queille, and .Joseph Sifakis. The 25MC syni|>osium was part of the 18th International Conference on Computer Aided Verification (CAV), which in turn was part of the Federated Logic Conference (FLOC) 200G in Seattle. The program was complemented by a panel on ''Verification in the Next 25 Years'' organized by Limor Fix.