Abstract
A time-consuming and error-prone activity in symbolic model-checking is the construction of environments. We present a technique for modeling environmental constraints that avoids the need for explicit construction of environments. Moreover, our approach supports an assume/guarantee style of reasoning that also supports simulation monitors. We give examples of the use of constraints in PowerPCTMverification.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
E.M. Clarke and E.A. Emerson, Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic, Proceedings of the Workshop on Logics of Programs, York town Heights, NY, Springer-Verlag LNCS no. 131, pp. 52–71, May 1981.
D.E. Long, “Model Checking, Abstraction, and Compositional Verification,” School of Computer Science, Carnegie Mellon University publication CMU-CS-93-178, July 1993.
K. L. McMillan, “A Compositional Rule for Hardware Design Refinement,” Orna Grunberg (Ed.) Computer Aided Verification, Proceedings of the 9th International Conference, Haifa, Israel, Springer-Verlag LNCS no. 1254, pp. 24–35, June 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kaufman, M., Martin, A., Pixley, C. (1998). Design constraints in symbolic model checking. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028768
Download citation
DOI: https://doi.org/10.1007/BFb0028768
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive