Abstract
We describe a computer-aided verification system which combines deductive with algorithmic (model-checking) verification methods. The system, called tlv (for temporal verification system), is constructed as an additional layer superimposed on top of the cmu smv system, and can verify finite-state systems relative to linear temporal logic (ltl) as well as ctl specifications. The systems to be verified can be either hardware circuits written in the smv design language or finite-state reactive programs written in a simple programming language (spl).
The paper presents a common computational model which can support these two types of applications and a high-level interactive language tlv-Basic, in which temporal verification rules, proofs, and complex assertions can be written. We illustrate the efficiency and generality gained by combining deductive with algorithmic techniques on several examples, culminating in verification of fragments of the Futurebus+ system. In the analysis of the Futurebus+ system, we even managed to detect a bug that was not discovered in a previous model-checking analysis of this system.
This research was supported in part by a basic research grant from the Israeli Academy of Sciences, and by the. European Community ESPRIT Basic Research Action Project 6021 (REACT).
Chapter PDF
Similar content being viewed by others
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
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
E.M Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness. Verification of the Futurebus+ cache coherence protocol. In L. Claesen, editor, Proc. of the 11th Int. Symp. on Computer Hardware Description Languages and their Applications. North-Holland, April 1993.
M. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In Formal Aspects of VLSI Design, pages 153–177. Elsevier Science Publishers (North Holland), 1986.
J.J Joyce and C.-J.H. Seger. Linking BDD-based symbolic evaluation to interactive theorem proving. In Proc. of the 30th Design Automation Conf., ACM, 1993.
R. Kurshan and L. Lamport. Verification of a multiplier: 64 bits and beyond. In C. Courcoubetis, editor, Proc. of 5th CAV, volume 697 of Lect. Notes in Comp. Sci., pages 166–179. Springer-Verlag, 1993.
Z. Manna, A. Annchitanukul, N. Bjørner, A. Browne, E. Chang, M. Colón, L. De Alfaro. H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994.
Z. Manna. Beyond model checking. In D. L. Dill, editor, Proc. of 6th CAV, volume 818 of Lect. Notes in Comp. Sci., pages 220–221. Springer-Verlag, 1994. Invited talk.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
S. Owre, J.M. Rushby, N. Shankar, and M.K. Srivas. A tutorial on using PVS for hardware verification. In R. Kumar and T. Kropf, editors, Proc. of the 2nd Conf. on Theorem Provers in Circuit Design, pages 167–188. FZI Publication, Universität Karlsruhe, 1994. Preiminary Version.
A. Pnueli and E. Shahar. The TLV system and its applications. Technical report, The Weizmann Institute, 1996.
S. Rajan, N. Shankar, and M.K. Srivas. An integration of model checking with automated proof checking. In P. Wolper, editor, Proc. of 7th CAV, volume 939 of LNCS, pages 84–97. Springer-Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pnueli, A., Shahar, E. (1996). A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_68
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_68
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive