The enormous number of states reachable during explicit model checking is the main bottleneck for scalability. This paper presents approaches of using decision diagrams to represent very large state space compactly and efficiently. This is possible …
Efficacy of partial order reduction in reducing state space relies on adequate extraction of the independence relation among possible behaviors. However, traditional approaches by statically analyzing system model structures are often not able to …
Embedded systems are composed of a heterogeneous collection of digital, analog, and mixed-signal hardware components. This paper presents a method for the verification of systems composed of such a variety of components. This method utilizes a new …
This paper presents a new algorithm for timed state-space exploration, POSET timing, POSET timing improves upon geometric methods by utilizing concurrency and causality information to dramatically reduce the number of geometric regions needed to …