Model Checking @CMU
[Home]

[People]

[Software]

[Publications]

[Support]

 [Links]

[Internal]

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
July 31 2007 VCEGAR v1.3  binary release
July 15 2006 VCEGAR v1.0  binary release
May 20 2006 SatMate  binary release
Mar 24 2005 VCEGAR v0.9  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