The introduction of symbolic model checking, coupled with BDDs as an underlying representation, has led to significant progress in the size and diversity of systems susceptible of being automatically verified. However crucial the role of BDDs has been in that achievement, they also have known drawbacks. Examples of such drawbacks include the need of manually fed variable ordering, or size explosion for well-known classes of problems.

In this work, we replace BDDs by a non-canonical data- structure, coupled with a SAT-procedure for efficient checking of satisfiability of propositional formulae. Based on this principle, we have implemented a tool: FixIt. This tool performs standard fixed-point reachability analysis.

We present the algorithm and the main implementation issues of FixIt. We also report on current work, and show some comparative results.

ASTEC seminar
March 7, 2000

Place: Information technology, Uppsala University
Room: 1549
Time: 13.15 - 14.00 (+ coffee and discussion)

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar nourished by cookies and coffee.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 1 hour.