Model checking is
a method for formally verifying finite-state concurrent systems. Specifications
about the system are expressed as temporal logic formulas, and efficient
symbolic algorithms are used to traverse the model defined by the system and
check if the specification holds or not. Extremely large state-spaces can often
be traversed in minutes. The technique has been applied to several complex
industrial systems such as the Futurebus+ and the PCI local bus protocols. Here
is an overview.
The Model
Checking Group is part of the Specification
and Verification Center at CMU.
news/events
May
23 2009
NFLSAT
binary release
Feb
15 2005
CMU-WISC
MURI Review Meeting, Arlington VA
Aug
16 2004
CMU-WISC
MURI Review Meeting, Annapolis MD
Nov
12-13 2003
CMU-WISC
MURI Review Meeting,
Details
Aug
03 2003
CBMC
binary release
Jul
29 2003
MAGIC
0.1 source release
Jul
22-23 2003
CMU-WISC
MURI Review Meeting,
Details
May
1-2 2003
Workshop
on High Confidence Embedded Systems, Details
Jan
9-10 2003
CMU-UPenn
Workshop on Hybrid and Embedded Systems,
Details,
Allenberry Resort
Dec
7 2002
Joint
CMU-WISC ONR Workshop Details
Nov
5 2002
Li
Tan,
Evidence Based Verification,
Abstract
3:30 p.m.- 4:30 p.m. 7220 Wean Hall
Oct
8 2002
Gianfranco
Ciardo, Professor of Computer
Science, College of William and Mary
Exploiting Structural Information for Efficient Symbolic State-Space
Generation,
Abstract
3:30 p.m.- 5:00 p.m. , 7220 Wean Hall
Oct
4 2002
J.
Strother Moore, Professor and
Chair, Department of Computer Sciences, University of Texas at Austin
Proving Theorems about Java and the JVM, Abstract
10:00 a.m.- 11:30 a.m. 4623 Wean Hall