Research Laboratory - Laboratory for Logic
Practical applications of mathematical logic to computer science have burgeoned over the last decade, particularly in the domain of verification of software and hardware, artificial intelligence, and logic-based programming languages. Some of these have attained sufficient maturity to have been packaged in commercial products, most notably the "model checking" technique for verification of protocols and circuits. The potential future impact of formal methods based on logic is enormous.
Automated theorem proving and verification have been topics of research since the earliest days of computers. Attempting to prove correctness of programs, and similarly verification of circuits, faces many difficulties. The general problem is unsolvable, many restrictions that are solvable are intractable, and those that are fast enough require human intervention.
A recent strategy for dealing with these issues is finite model checking, which is a very important method for verifying sequential designs (in those cases where there are only finitely many possibilities). In bounded model checking, one tries larger and larger paths through the design in a search for a satisfying assignment, which serves as counterexample to the correctness of the design (that is, a "bug"). A major problem with model checking, however, is the explosion of states in the temporal model generated, hence, of the number of possibilities that need to be checked. This project touches on many different areas of computer science, either to describe the problem or help analyze and attack it, for example, automated deduction, concurrent programming, temporal logic, complexity theory, computer algebra, computational group theory. One specific aspect we intend to address is that of solving satisfiability and validity problems for symbolic model checking faster.