According to a study in 2002 commisioned by a US Department, software bugs annually costs the US economy an estimated $59 billion. A more recent study in 2013 by Cambridge University estimated that the global cost has risen to $312 billion globally.

There exists various ways to prevent, isolate and fix software bugs, ranging from lightweight methods that are (semi)-automatic, to heavyweight methods that require significant user interaction. Our own method described in this tutorial is based on automated run-time checking of a combination of protocol- and data-oriented properties of object-oriented programs.


Regular Expression Sequence Diagram Parse Tree Java Modeling Language Attribute Grammar 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.): Communicating Sequential Processes. LNCS, vol. 3525. Springer, Heidelberg (2005)Google Scholar
  2. 2.
    Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA, pp. 345–364 (2005)Google Scholar
  3. 3.
    Artho, C., Drusinksy, D., Goldberg, A., Havelund, K., Lowry, M., Păsăreanu, C.S., Roşu, G., Visser, W.: Experiments with test case generation and runtime analysis. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 87–107. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Backus, J.W.: The syntax and semantics of the proposed international algebraic language of the Zurich ACM-GAMM conference. In: IFIP Congress, pp. 125–131 (1959)Google Scholar
  5. 5.
    Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes, 1st edn. Cambridge University Press, New York (2009)CrossRefzbMATHGoogle Scholar
  6. 6.
    Bartetzko, D., Fischer, C., Möller, M., Wehrheim, H.: Jass - Java with assertions. Electr. Notes Theor. Comput. Sci. 55(2) (2001)Google Scholar
  7. 7.
    Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)Google Scholar
  9. 9.
    Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal — a tool suite for automatic verification of real–time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  10. 10.
    Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Berdine, J., Cook, B., Ishtiaq, S.: sLAyer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  12. 12.
    Bergstra, J.A., Klop, J.W.: Acttau: A universal axiom system for process specification. In: Algebraic Methods, pp. 447–463 (1987)Google Scholar
  13. 13.
    Bertot, Y., Castéran, P., Huet, G., Paulin-Mohring, C.: Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin (2004)Google Scholar
  14. 14.
    Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)CrossRefGoogle Scholar
  15. 15.
    Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  16. 16.
    Chalin, P., James, P.R., Karabotsos, G.: JML4: Towards an industrial grade IVE for java and next generation research platform for JML. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 70–83. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Chen, F., Rosu, G.: MOP: an efficient and generic runtime verification framework. In: OOPSLA, pp. 569–588 (2007)Google Scholar
  18. 18.
    Cheon, Y., Perumandla, A.: Specifying and checking method call sequences of Java programs. Software Quality Journal 15(1), 7–25 (2007)CrossRefGoogle Scholar
  19. 19.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  20. 20.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)CrossRefGoogle Scholar
  21. 21.
    Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)Google Scholar
  22. 22.
    Colombo, C., Pace, G.J., Schneider, G.: LARVA — safer monitoring of real-time java programs (tool paper). In: SEFM, pp. 33–37 (2009)Google Scholar
  23. 23.
    Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001)CrossRefzbMATHGoogle Scholar
  24. 24.
    de Boer, F.S., Bonsangue, M.M., Steffen, M., Ábrahám, E.: A fully abstract semantics for UML components. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 49–69. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  25. 25.
    de Gouw, S., de Boer, F.S., Johnsen, E.B., Wong, P.Y.H.: Run-time checking of data- and protocol-oriented properties of Java programs: an industrial case study. In: SAC, pp. 1573–1578 (2013)Google Scholar
  26. 26.
    Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA, pp. 213–226 (2008)Google Scholar
  27. 27.
    Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  28. 28.
    Fischer, C., Wehrheim, H.: Behavioural subtyping relations for Object-Oriented formalisms. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 469–483. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  29. 29.
    Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, Providence, Rhode Island. Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society (1967)Google Scholar
  30. 30.
    Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-Dimensional Modal Logics: Theory and Applications. Elsevier (2003)Google Scholar
  31. 31.
    Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Elements of Reusable Object-Oriented Software. Addison-Wesley (1995)Google Scholar
  32. 32.
    Grune, D., Jacobs, C.J.: Parsing Techniques - A Practical Guide, 2nd edn. Springer (2008)Google Scholar
  33. 33.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)Google Scholar
  34. 34.
    Hedin, G.: Incremental attribute evaluation with side-effects. In: Hammer, D. (ed.) CCHSC 1988. LNCS, vol. 371, pp. 175–189. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  35. 35.
    Heisel, M., Reif, W., Stephan, W.: Implementing verification strategies in the KIV-system. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 131–140. Springer, Heidelberg (1988)CrossRefGoogle Scholar
  36. 36.
    Hennessy, M.: Algebraic theory of processes. MIT Press series in the foundations of computing. MIT Press (1988)Google Scholar
  37. 37.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  38. 38.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefzbMATHGoogle Scholar
  39. 39.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)Google Scholar
  40. 40.
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)CrossRefGoogle Scholar
  41. 41.
    International Telecommunication Union. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). Technical report, ITU, Geneva (2001)Google Scholar
  42. 42.
    Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  43. 43.
    Jeffrey, A., Rathke, J.: ava Jr: Fully abstract trace semantics for a core Java language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423–438. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  44. 44.
    Kleene, S.C.: Representation of events in nerve nets and finite automata. Automata Studies (1956)Google Scholar
  45. 45.
    Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Prog. Lang. Syst. 28(4), 619–695 (2006)CrossRefGoogle Scholar
  46. 46.
    Klint, P., van der Storm, T., Vinju, J.J.: Rascal: a domain specific language for source code analysis and manipulation. In: Walenstein, A., Schupp, S. (eds.) Proceedings of the IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2009), pp. 168–177 (2009)Google Scholar
  47. 47.
    Knuth, D.E.: Semantics of context-free languages. Mathematical Systems Theory 2(2), 127–145 (1968)MathSciNetCrossRefzbMATHGoogle Scholar
  48. 48.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)Google Scholar
  49. 49.
    Lee, L.: Fast context-free grammar parsing requires fast boolean matrix multiplication. J. ACM 49(1), 1–15 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  50. 50.
    Li, X., Liu, Z., He, J.: A formal semantics of UML sequence diagram. In: Australian Software Engineering Conference, pp. 168–177 (2004)Google Scholar
  51. 51.
    Martin, J.C.: Introduction to Languages and The Theory of Computation. McGraw-Hil (2010)Google Scholar
  52. 52.
    Martin, M., Livshits, B., Lam, M.S.: Finding application errors and security flaws using PQL: a Program Query Language. In: OOPLSLA (2005)Google Scholar
  53. 53.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall (1997)Google Scholar
  54. 54.
    Mikhajlov, L., Sekerinski, E.: A study of the fragile base class problem. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 355–382. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  55. 55.
    Milner, R.: Fully abstract models of typed λ-calculi. Theoretical Comput. Sci. 4, 1–22 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  56. 56.
    Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)CrossRefzbMATHGoogle Scholar
  57. 57.
    Milner, R.: Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, New York (1999)zbMATHGoogle Scholar
  58. 58.
    Nobakht, B., Bonsangue, M.M., de Boer, F.S., de Gouw, S.: Monitoring method call sequences using annotations. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 53–70. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  59. 59.
    Parr, T.J., Quong, R.W.: Adding semantic and syntactic predicates to LL(k): pred-LL(k). In: Fritzson, P.A. (ed.) CC 1994. LNCS, vol. 786, pp. 263–277. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  60. 60.
    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57 (1977)Google Scholar
  61. 61.
    Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  62. 62.
    Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: FOCS, pp. 109–121 (1976)Google Scholar
  63. 63.
    Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)Google Scholar
  64. 64.
    Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes. Cambridge University Press (2001)Google Scholar
  65. 65.
    Sipser, M.: Introduction to the theory of computation. PWS Publishing Company (1997)Google Scholar
  66. 66.
    Stolz, V., Huch, F.: Runtime verification of concurrent Haskell programs. Electr. Notes Theor. Comput. Sci. 113, 201–216 (2005)CrossRefGoogle Scholar
  67. 67.
    Valiant, L.G.: General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10(2), 308–315 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  68. 68.
    van den Berg, J., Jacobs, B.: The LOOP Compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  69. 69.
    van Eijk, P.H.J., Vissers, C., Diaz, M. (eds.): Formal Description Technique Lotos: Results of the Esprit Sedos Project. Elsevier Science Inc., New York (1989)Google Scholar
  70. 70.
    Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Frank S. de Boer
    • 1
    • 2
  • Stijn de Gouw
    • 1
    • 2
  1. 1.CWIAmsterdamThe Netherlands
  2. 2.Leiden UniversityThe Netherlands

Personalised recommendations