Symbolic model checking is a powerful formal verification technique that, contrarily to theorem proving, requires no user assistance. It is able to verify that an implementation, modelled as a labelled finite-state transition graph, satisfies its ...
Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of ...
This paper describes a SAT-based unbounded symbolic model checking algorithm. BDDs have been widely used for symbolic model checking, but the approach suffers from memory overflow. The SAT procedure was exploited to overcome the problem, but it verified ...
IEEE Computer Society
United States
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in