Abstract
Computer programs are formal texts that are composed by programmers and executed by machines. Formal methods are used to predict the execution-time behavior of a program text through formal, symbolic calculation. Automation in the form of computer programs can be used to execute formal calculations so that they are reproducible and checkable. Deduction and exploration are two basic frameworks for the formal calculation of program properties. Both deduction and exploration have their limitations. We argue that these limitations can be overcome through a methodology for automated verification that uses property-preserving abstractions to bridge the gap between deduction and exploration. We introduce models, logics, and verification methods for transition systems, and outline a methodology based on the combined use of deduction, exploration, and abstraction.
This research was supported by NSF Grant CCR-0082560, DARPA/AFRL Contract F33615-00-C-3043, and NASA Contract NAS 1-00079.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104 (1): 2–34, May 1993.
R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems I,Lecture Notes in Computer Science 736, pages 209–229. Springer-Verlag, 1993. 16. Automated verification using deduction, exploration, and abstraction 349
R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science,126(2):183–235, 25 April 1994. Fundamental Study.
R. Alur and T. A. Henzinger. Logics and models of real time: A survey. In J. W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 74–106. Springer-Verlag, 1991.
Rajeev Alur and Thomas A. Henzinger, editors. Computer-Aided Verification, CAV ‘86, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996. Springer-Verlag.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98 (2): 142–170, June 1992.
Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, César Munoz, Sam Owre, Harald Rueß, John Rushby, Vlad Rusu, Hassen Saldi, N. Shankar, Eli Singerman, and Ashish Tiwari. An overview of SAL. In C. Michael Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop,pages 187–196, Hampton, VA, June 2000. NASA Langley Research Center. Proceedings available at http:// shemesh. larc.nasa.gov/fm/ Lfm2000/Proc/.
Tevfik Bultan, Richard Gerber, and William Pugh. Symbolic model checking of infinite state systems using Presburger arithmetic. In Grumberg [Gru97], pages 400–411.
R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: a system for verification and synthesis. In Alur and Henzinger [AH96], pages 428–432.
Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Hu and Vardi [HV98], pages 319–331.
K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient implementation of a BDD package. In Proc. of the 27th ACM/IEEE Design Automation Conference, pages 40–45, 1990.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis. In 4th ACM Symposium on Principles of Programming Languages. ACM, January 1977.
James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering,pages 439–448, Limerick, Ireland, June 2000. IEEE Computer Society.
E.M. Clark, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16 (5): 1512–1542, September 1994.
E. M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999. 350 Shankar
K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988.
M. A. Colón and T. E. Uribe. Generating finite-state abstractions of reactive systems using decidion procedures. In Hu and Vardi [HV98], pages 293–304.
Satyaki Das, David L. Dill, and Seungjoon Park. Experience with predicate abstraction. In Halbwachs and Peled [HP99], pages 160–171.
David L. Dill. The Mur0 verification system. In Alur and Henzinger [AH96], pages 390–393.
Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli, editors. Compositionality: The Significant Difference (Revised lectures from International Symposium COMPOS’97), volume 1536 of Lecture Notes in Computer Science, Bad Malente, Germany, September 1997. Springer-Verlag.
E. Allen Emerson and Joseph Y. Halpern. “sometimes” and “not never” revisited: On branching versus linear time. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 127–140, Austin, Texas, January 1983.
E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 16, pages 995–1072. Elsevier and MIT press, Amsterdam, The Netherlands, and Cambridge, MA, 1990.
Formal Systems (Europe) Ltd, Oxford, UK. Failures Divergence Refinement: User Manual and Tutorial, 1.20 edition, October 1992.
Orna Grumberg, editor. Computer-Aided Verification, CAV ‘87, volume 1254 of Lecture Notes in Computer Science, Haifa, Israel, June 1997. Springer-Verlag.
C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(101: 576–583, 1969.
C. A. R. Hoare. Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, 1985.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.
Nicolas Halbwachs and Doron Peled, editors. Computer-Aided Verification, CAV ‘89, volume 1633 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag.
Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV ‘88, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag.
R.P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1993.
Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16 (3): 872–923, May 1994.
N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Annual Symposium on Principles of Distributed Computing,pages 137–151, New York, 1987. ACM Press. 16. Automated verification using deduction, exploration, and abstraction 351
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993.
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Volume I: Specification. Springer-Verlag, New York, NY, 1992.
K. McMillan, S. Qadeer, and J. Saxe. Induction in compositional model checking. In E. A. Emerson and A. P. Sistla, editors, Computer-Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 312–327, Chicago, IL, July 2000. Springer-Verlag. [ORSvH95] S. Owre, J. Rushby, N. Shankar, and E. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
David Park. Finiteness is mu-ineffable. Theoretical Computer Science, 3: 173–181, 1976.
S. Rajan, N. Shankar, and M. Srivas. An integration of theorem proving and automated proof checking. In Computer-Aided Verification, number 939 in Lecture Notes in Computer Science, pages 84–97. Springer-Verlag, 1995.
D. Scott and J. W. de Bakker. A theory of programs, unpublished notes. IBM Seminar, Vienna, 1969.
SG97] Hassen Saldi and Susanne Graf. Construction of abstract state graphs with PVS. In Grumberg [Gru97], pages 72–83.
N. Shankar. Machine-assisted verification using theorem proving and model checking. In M. Broy and Birgit Schieder, editors, Mathematical Methods in Program Development, volume 158 of NATO ASI Series F: Computer and Systems Science, pages 499–528. Springer, 1997.
Hassen Saldi and N. Shankar. Abstract and model check while you prove. In Halbwachs and Peled [HP99], pages 443–454.
A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. of Math., 5: 285–309, 1955.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer Science+Business Media New York
About this chapter
Cite this chapter
Shankar, N. (2003). Automated verification using deduction, exploration, and abstraction. In: McIver, A., Morgan, C. (eds) Programming Methodology. Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-0-387-21798-7_16
Download citation
DOI: https://doi.org/10.1007/978-0-387-21798-7_16
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4419-2964-8
Online ISBN: 978-0-387-21798-7
eBook Packages: Springer Book Archive