Seminars & Colloquia
Computer Science, CMU
"Model Checking: From Hardware To Software And Back Again"
Monday January 29, 2007 04:00 PM
Location: 331, Daniels -- NOTE THE CHANGE ==>> NCSU Historical Campus
(Visitor parking instructions)
This talk is part of the Triangle Computer Science Distinguished Lecturer Series
Abstract: The first major successes of model checking were in hardware verification. Symbolic model checking with BDDs and later SAT-based bounded model checking made it possible to handle hardware designs of realistic complexity. Combining counterexample-guided abstraction refinement and predicate abstraction with these symbolic techniques, led to a new generation of powerful software model checkers (SLAM, BLAST, MAGIC, CBMC, etc). Recently, we have used software model checking techniques to verify programs in hardware description languages like Verilog. Most model checkers for hardware verification currently compile the design into a gate-level description or netlist before verification. As a result, much of the structure of the design is lost and the state explosion problem is exacerbated. By analyzing the hardware description language using software model checking techniques, we are able to avoid the translation into netlist form and handle even larger designs.
Short Bio: See http://www.cs.cmu.edu/~emc/
Host: Sanjoy Baruah, Computer Science, UNC