We describe a method for computing an exact minimal automaton to act as an intermediate assertion in assume-guarantee reasoning, using a sampling approach and a Boolean satisfiability solver. For a set of synthetic benchmarks intended to mimic common situations in hardware verification, this is shown to be significantly more effective than earlier approximate methods based on Angluin's L* algorithm. For many of these benchmarks, this method also outperforms BDD-based model checking and interpolation-based model checking. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Gupta, A., McMillan, K. L., & Fu, Z. (2007). Automated assumption generation for compositional verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4590 LNCS, pp. 420–432). Springer Verlag. https://doi.org/10.1007/978-3-540-73368-3_45
Mendeley helps you to discover research relevant for your work.