4. The method of claim 1 , further including generating an association list that identifies the relationship between the atomic assertions and the propositional symbols.
1. A method for verifying an executable system against an assertion in a specification, the method comprising the steps of: generating a propositional formula representing an assertion in the specification using Boolean propositional symbols, each Boolean propositional symbol being associated with an atomic assertion in the assertion; generating a set of traces representing a sequence of configurations of the system with respect to the assertion, wherein the traces include trace configuration data representing a configuration of the system in response to a particular trace; converting the trace configuration data into truth assignments for a set of propositional symbols; generating a trace of the system using the truth assignments for the propositional symbols; and verifying the assertion using the trace of truth assignments for the propositional symbols and the propositional formula.