Abstract
Program verification is concerned with proving that a program is correct and adheres to a given specification. Testing a program, in contrast, means to search for a witness that the program is incorrect. In the present paper, we use a program logic forJava to prove the incorrectness of programs. We show that this approach, carried out in a sequent calculus for dynamic logic, creates a connection between calculi and proof procedures for program verification and test data generation procedures. Starting with a program logic enables to find more general and more complicated counterexamples for the correctness of programs.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C.: JML Reference Manual (August 2002)
Rümmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 422–436. Springer, Heidelberg (2006)
King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Notices 35(9), 268–279 (2000)
Edvardsson, J.: A survey on automatic test data generation. In: ECSEL. Proceedings of the Second Conference on Computer Science and Engineering in Linkping, pp. 21–28 (October 1999)
Hähnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 101–178. Elsevier Science BV, Amsterdam (2001)
Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1996)
Giese, M.: Incremental closure of free variable tableaux. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 545–560. Springer, Heidelberg (2001)
Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Supercomputing 1991. Proceedings of the 1991 ACM/IEEE conference on Supercomputing, pp. 4–13. ACM Press, New York, USA (1991)
Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common lisp. IEEE Trans. Softw. Eng. 23(4), 203–213 (1997)
Gupta, N., Mathur, A.P., Soffa, M.L.: Automated test data generation using an iterative relaxation method. In: SIGSOFT 1998/FSE-6. Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 231–244. ACM Press, New York (1998)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer 2(4), 410–425 (2000)
Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering 10(2), 203–232 (2003)
Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings PLDI, pp. 203–213 (2001)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proceedings PLDI, pp. 234–245 (2002)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Reif, W., Schellhorn, G., Thums, A.: Flaw detection in formal specifications. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 642–657. Springer, Heidelberg (2001)
Shah, M.A.: Generating counterexamples for Java dynamic logic. Master’s thesis (November 2005)
Parasoft: JTest (2006), http://www.parasoft.com/jsp/products/home.jsp?product=Jtest
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rümmer, P., Shah, M.A. (2007). Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic. In: Gurevich, Y., Meyer, B. (eds) Tests and Proofs. TAP 2007. Lecture Notes in Computer Science, vol 4454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73770-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-73770-4_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73769-8
Online ISBN: 978-3-540-73770-4
eBook Packages: Computer ScienceComputer Science (R0)