| Symbolic Model Checking is a technique for checking certain properties of a finite state model of a computer system. The most widely used symbolic representation is based on Ordered Binary Decision Diagrams. In [4], G. Avrunin showed how computational geometry and Gröbner basis techniques may be used for symbolic model checking. The present work investigates the details of this approach, and its practicality, using theoretical means and experiments based on a prototype implementation. |
