Q. Tran and M.Y. Vardi (USA)
Groebner basis, Boolean ring, model checking, automated formal verification.
Model checking is an algorithmic approach for automatically verifying whether a hardware or software system functions cor rectly. Typically, computation is carried over Boolean algebras using binary decision diagrams (BDDs) or satisfiability (SAT) solvers. In this paper we show that computation for model checking can also be carried over the dual Boolean rings of the Boolean algebras by means of efficient polynomial and Groebner basis (GB) computation. We also show how all operations required for model checking can be implemented by means of Groebner bases.
Important Links:
Go Back
