Patent Document ID: 8412668
Application ID: 12579141

Base Claim:
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.

---

Claim 6:
6. The method of claim 1 , wherein the trace is a test suite comprising a plurality of traces.