Abstract
A program verifier determines whether a program satisfies a specification. Ideally verification is achieved by static analysis without executing the code. However, program verification is unsolvable in general. The interactive approach, for example with a human guiding a theorem prover, does not in practice scale to large software systems. Some restricted kinds of specifications can, however, be checked automatically, for example type definitions. Also static analysis of properties such as un-initialized variables, null-pointer de-referencing, and arraybound violations scales to production programs on the order of hundreds of thousands of lines of code. Even concurrency-related problems such as data races and deadlocks can to some extent be checked statically, although often resulting in false positives. However, going beyond these simple properties to arbitrarily complex behavior specification and scaling to ever-growing production program size is undoubtedly a challenge, and in our opinion we cannot expect regular economic use of program verification of arbitrary properties to be fully achieved within the 15 year time horizon of the challenge.
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.
Download to read the full chapter text
Chapter PDF
References
1st – 5th Workshops on Runtime Verification (RV 2001 - RV 2005). ENTCS, vol. 55(2), 70(4), 89(2), 113. Elsevier Science Direct. Amsterdam (to be published, 2001–2005), http://www.runtime-verification.org
Allan, C., Avgustinov, P., Kuzins, S., de Moor, O., Sereni, D., Sittamplan, G., Tibble, J., Christensen, A.S., Hendren, L., Lhoták, O.: Adding Trace Matching with Free Variables to AspectJ. In: OOPSLA 2005 (2005)
Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M., Pasareanu, C., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining Test-Case Generation and Runtime Verification. Theoretical Computer Science 336(2–3), 209–234 (2005), Extended version of [4]
Artho, C., Drusinsky, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., 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)
Artho, C., Havelund, K., Biere, A.: High-Level Data Races. Software Testing, Verification and Reliability 13(4) (2004)
Artho, C., Havelund, K., Biere, A.: Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. In: 2nd International Symposium on Automated Technology for Verification and Analysis, Taiwan, October–November (2004)
AspectJ. http://eclipse.org/aspectj
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, Springer, Heidelberg (2005)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program Monitoring with LTL in Eagle. In: Parallel and Distributed Systems: Testing and Debugging (PADTAD 2004), Santa Fee, New Mexico, USA, April (2004)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, Springer, Heidelberg (2004)
Bensalem, S., Bozga, M., Krichen, M., Tripakis, S.: Testing Conformance of Real-Time Applications by Automatic Generation of Observers. In: Proceedings of the 4th International Workshop on Runtime Verification (RV 2004) [1], pp. 19–38 (2004)
Bensalem, S., Fernandez, J.-C., Havelund, K., Mounier, L.: Confirmation of Deadlock Potentials Detected by Runtime Analysis. In: Parallel and Distributed Systems: Testing and Debugging (PADTAD 2006), Portland, Maine, USA (July 2006)
Bensalem, S., Havelund, K.: Scalable Dynamic Deadlock Analysis of Multi-Threaded Programs. In: Parallel and Distributed Systems: Testing and Debugging (PADTAD - 3), IBM Verification Conference, Haifa, Israel, November 2005. LNCS (2005)
Chen, F., D’Amorim, M., Roşu, G.: Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP. In: Proceedings of the 5th International Workshop on Runtime Verification (RV 2005) [1] (2005)
Clavel, M., Durán, F.J., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: The Maude System. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 240–243. Springer, Heidelberg (1999)
Daikon. http://pag.csail.mit.edu/daikon
D’Amorim, M., Havelund, K.: Runtime Verification for Java. In: Workshop on Dynamic Program Analysis (WODA 2005) (March 2005)
D’Amorim, M., Rosu, G.: Efficient Monitoring of Omega-Languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, Springer, Heidelberg (2005)
D’Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: Runtime Monitoring of Synchronous Systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166–174 (2005)
Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000)
Drusinsky, D.: Monitoring Temporal Rules Combined with Time Series. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 114–118. Springer, Heidelberg (2003)
Drusinsky, D.: Semantics and Runtime Monitoring of TLCharts: Statechart Automata with Temporal Logic Conditioned Transitions. In: Proceedings of the 4th International Workshop on Runtime Verification (RV 2004) [1], pp. 2–18 (2004)
Eiffel. http://www.eiffel.com
Eytani, Y., Havelund, K., Stoller, S., Ur, S.: Toward a Framework and Benchmark for Testing Tools for Multi-Threaded Programs. In: Concurrency and Computation: Practice and Experience (to appear, 2005)
Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting Statistics over Runtime Executions. In: Proceedings of the 2nd International Workshop on Runtime Verification (RV 2002) [1], pp. 36–55 (2002)
Finkbeiner, B., Sipma, H.: Checking Finite Traces using Alternating Automata. In: Proceedings of the 1st International Workshop on Runtime Verification (RV 2001)[1], pp. 44–60 (2001)
Flanagan, C., Freund, S.: Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs. SIGPLAN Not. 39(1), 256–267 (2004)
Giannakopoulou, D., Havelund, K.: Automata-Based Verification of Temporal Properties on Running Programs. In: Proceedings, International Conference on Automated Software Engineering (ASE 2001), Coronado Island, California. ENTCS, pp. 412–416 (2001)
Goldberg, A., Havelund, K.: Instrumentation of Java Bytecode for Runtime Analysis. In: Fifth ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP 2003), Darmstadt, Germany (July 2003)
Harel, D.: Statecharts: A Visual Formalism For Complex Systems. Science of Computer Programming 8, 231–274 (1987)
Harrow, J.: Runtime Checking of Multithreaded Applications with Visual Threads. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 331–342. Springer, Heidelberg (2000)
Havelund, K.: Using Runtime Analysis to Guide Model Checking of Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 245–264. Springer, Heidelberg (2000)
Havelund, K., Roşu, G.: Monitoring Java Programs with Java PathExplorer. In: Proceedings of the 1st International Workshop on Runtime Verification (RV 2001)[1], pp. 97–114 (2001)
Havelund, K., Roşu, G.: Monitoring Programs using Rewriting. In: Proceedings, International Conference on Automated Software Engineering (ASE 2001), Coronado Island, California. Institute of Electrical and Electronics Engineers, pp. 135–143 (2001)
Havelund, K., Roşu, G.: An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design 24(2) (March 2004)
Havelund, K., Roşu, G.: Efficient Monitoring of Safety Properties. Software Tools for Technology Transfer 6(2), 158–173 (2004)
Havelund, K., Roşu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002), Best paper award
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An Overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–353. Springer, Heidelberg (2001)
Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a Run-time Assurance Tool for Java. In: Proceedings of the 1st International Workshop on Runtime Verification (RV 2001)[1] (2001)
Patterns. http://patterns.projects.cis.ksu.edu
PSL/Sugar. http://www.pslsugar.org
Roşu, G., Havelund, K.: A Rewriting-based Approach to Trace Analysis. Automated Software Engineering 12(2), 151–197 (2005)
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Transactions on Computer Systems 15(4), 391–411 (1997)
Sen, K., Roşu, G.: Generating Optimal Monitors for Extended Regular Expressions. In: Proceedings of the 3rd International Workshop on Runtime Verification (RV 2003)[1], pp. 162–181 (2003)
Sen, K., Roşu, G., Agha, G.: Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, Springer, Heidelberg (2005)
Specware. http://www.specware.org
SPIN. http://spinroot.com
Stolz, V., Bodden, E.: Temporal Assertions using AspectJ. In: Fifth Workshop on Runtime Verification (RV 2005). Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers, Amsterdam (2005)
T-UPPAAL. http://www.cs.aau.dk/~marius/tuppaal
Thati, P., Rosu, G.: Monitoring Algorithms for Metric Temporal Logic Specifications. In: Proceedings of the 4th International Workshop on Runtime Verification (RV 2004)[1], pp. 131–147 (2004)
Valgrind. http://valgrind.org
Vanderperren, W., Suvé, D., Augustina Cibrán, M., De Fraine, B.: Stateful Aspects in JAsCo. In: Workshop on Software Composition, ETAPS 2005 (2005)
Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Proceedings of ASE 2000: The 15th IEEE International Conference on Automated Software Engineering, September 2000, IEEE CS Press, Los Alamitos (2000)
Walker, R.J., Viggers, K.: Implementing Protocols via Declarative Event Patterns. In: Taylor, R.N., Dwyer, M.B. (eds.) 12th International Symposium on the Foundations of Software Engineering, ACM, New York (2004)
Wang, L., Stoller, S.: Run-Time Analysis for Atomicity. In: Proceedings of the 3rd International Workshop on Runtime Verification (RV 2003) [1] (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Havelund, K., Goldberg, A. (2008). Verify Your Runs. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_40
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)