Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Madhusudan, P., Nam, W.: Parametric temporal logic for model measuring. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548–562. Springer, Heidelberg (2005)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75, 87–106 (1987)
Cobleigh, J., Giannakopoulou, D., Pasareanu, C.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, Springer, Heidelberg (2003)
Gold, E.M.: Complexity of automaton identification from given data. Information and Computation 37, 302–320 (1978)
Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.L.: Synthesis of FSMs: Functional Optimization. Kluwer Academic Publishers, Boston (1997)
McMillan, K.L.: Cadence SMV. Cadence Berkeley Labs, CA
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)
Mitchell, T.M.: Machine Learning. WCB/McGraw-Hill (1997)
Oliveira, A.L., Marques Silva, J.P.: Efficient search techniques for the inference of minimum size finite automata. In: Proceedings of the Symposium on String Processing and Information Retrieval (SPIRE), pp. 81–89 (1998)
Pfleeger, C.F.: State reduction in incompletely specified finite state machines. IEEE Transactions on Computers C-22, 1099–1102 (1973)
Pena, J.M., Oliveira, A.L.: A new algorithm for the reduction of incompletely specified finite state machines. In: Jorge, M. (ed.) Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pp. 482–489. ACM Press, New York, NY, USA (1998)
Quinlan, J.R.: Induction of decision trees. Machine Learning (1986)
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. In: Proceedings of the ACM Symposium on Theory of Computing (STOC), pp. 411–420. ACM Press, New York, NY, USA (1989)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gupta, A., McMillan, K.L., Fu, Z. (2007). Automated Assumption Generation for Compositional Verification. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_45
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_45
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)