Reducing the verification of a property in a system to a decision problem in some logic is a common practice in formal verification. Decision procedures can then be used to automate the solution of the verification task at hand. In this talk, Tacchella describe efficient decision procedures, their implementation and use in formal verification. His main focus is on decision procedures for propositional logic. He outlines a "modern" implementation of the Davis-Logemann-Loveland (DLL) algorithm for propositional satisfiability (SAT). The effectiveness of the approach was tested by developing SIMO, a C++ prototype SAT solver based on DLL, which showed a great potential for bug-finding in hardware designs at an industrial setting. The production version, SIM, is comparable to current state of the art SAT solvers and we plan to use it for increasing the capacity of existing hardware verification techniques.

His review will also include the extensions of the DLL algorithm to deal with the decision problem in logics that are more expressive (and more complex to decide) than propositional logics. These extensions will include our current research in decision procedures for modal (temporal and description) logics and quantified propositional logic.

Tuesday, February 6 at 4pm in DH 1064

A reception will follow in DH 3092.