Name
Abstract | ||
|---|---|---|
Bounded Model Checking (BMC) is a successful method for refuting properties of erroneous systems. Initially applied to discrete sys- tems only, BMC could be extended to more complex domains like linear hybrid automata. The increasing complexity coming along with these com- plex models, but also recent optimizations of SAT-based BMC, like exces- sive conflict learning, reveal a memory explosion problem especially for deep counterexamples. In this paper we introduce parametric data types for the internal solver structure that, taking advantage of the symmetry of BMC problems, remarkably reduce the memory requirements of the solver. |
Year | Venue | Field |
|---|---|---|
2006 | MBMV | Model checking,Computer science,Theoretical computer science,Hybrid system,Bounded function |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
7 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erika Ábrahám | 1 | 830 | 63.17 |
| Marc Herbstritt | 2 | 136 | 11.01 |
| Bernd Becker | 3 | 345 | 31.68 |
| Martin Steffen | 4 | 122 | 10.32 |