Abstract
We propose an iterative approach to formal verification by language containment. We start with some initial abstraction and then iteratively refine it, guided by the failure report from the verification tool. We show that the procedure will terminate, propose a series of heuristic aimed at reducing the size of BDD’s used in the computation, and formulate several open problems that could improve efficiency of the procedure. Finally, we present and discuss some initial experimental results.
Cite
CITATION STYLE
Balarin, F., & Sangiovanni-Vincentelli, A. L. (1993). An iterative approach to language containment. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 697 LNCS, pp. 29–40). Springer Verlag. https://doi.org/10.1007/3-540-56922-7_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
