Efficient monitoring of safety properties

Artho C, Drusinsky D, Goldberg A, Havelund K, Lowry M, Pasareanu C, Roşu G, Visser W (2003) Experiments with test case generation and runtime analysis. In: Börger E, Gargantini A, Riccobene E (eds) Proceedings of Abstract State Machines 2003, Taormina, Italy, March 2003. Lecture notes in computer science, vol 2589. Springer, Berlin Heidelberg New York, pp 87–107

Artho C, Havelund K, Biere A (2003) High-level data races. In: Proceedings of the 1st international workshop on verification and validation of enterprise information systems (VVEIS’03), Angers, France, April 2003

Ball T, Podelski A, Rajamani S (2001) Boolean and Cartesian abstractions for model checking C programs. In: Proceedings of tools and algorithms for the construction and analysis of systems (TACAS’01), Genoa, Italy, April 2001. Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York, pp 268–283

Chen F, Roşu G (2003) Towards monitoring-oriented programming: a paradigm combining specification and implementation. In: Proceedings of the 3rd workshop on runtime verification (RV’03), Boulder, CO, July 2003. Electronic notes in theoretical computer science, vol 89. Elsevier, Amsterdam, pp 106–125

Clavel M, Durán FJ, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Quesada JF (1999) Maude: specification and programming in rewriting logic. Maude System documentation at http://maude.csl.sri.com/papers

Clavel M, Durán FJ, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Quesada JF (1999) The Maude system. In: Narendran P, Rusinowitch M (eds) Proceedings of the 10th international conference on rewriting techniques and applications (RTA-99), Trento, Italy, July 1999. Lecture notes in computer science, vol 1631. Springer, Berlin Heidelberg New York, pp 240–243

Clavel M, Durán FJ, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Quesada JF (2000) A Maude tutorial. Manuscript at: http://maude.csl.sri.com/papers

Corbett J, Dwyer MB, Hatcliff J, Pasareanu CS, Robby Laubach S, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: Proceedings of the 22nd international conference on software engineering, Limerick, Ireland, June 2000. ACM Press, New York, pp 439–448

Demartini C, Iosif R, Sisto R (1999) A deadlock detection tool for concurrent Java programs. Software Pract Exper 29(7):577–603

Drusinsky D (2000) The Temporal Rover and the ATG Rover. In: Havelund K, Penix J, Visser W (eds) SPIN model checking and software verification. Lecture notes in computer science, vol 1885. Springer, Berlin Heidelberg New York, pp 323–330

Gabbay DM (1989) The declarative past and imperative future: executable temporal logic for interactive systems. In: Banieqbal B, Barringer H, Pnueli A (eds) Proceedings of the 1st conference on temporal logic in specification, Altrincham, UK, April 1989. Lecture notes in computer science, vol 398. Springer, Berlin Heidelberg New York, pp 409–448

Godefroid P (1997) Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM symposium on principles of programming languages, Paris, France, January 1997. ACM Press, New York, pp 174–186

Gunter E, Peled D (2002) Tracing the executions of concurrent programs. In: Havelund K, Roşu G (eds) Proceedings of runtime verification (RV’02), Copenhagen, July 2002. Electronic notes in theoretical computer science, vol 70. Elsevier, Amsterdam

Havelund K, Johnson S, Roşu G (2001) Specification and error pattern based program monitoring. In: Proceedings of the European Space Agency workshop on on-board autonomy, Noordwijk, The Netherlands, October 2001, pp 323–330

Havelund K, Lowry M, Penix J (2001) Formal analysis of a space craft controller using SPIN. IEEE Trans Software Eng 27(8):749–765

Havelund K, Pressburger T (1998) Model checking Java programs using Java PathFinder. Int J Software Tools Technol Trans 2(4):366–381. Special issue of STTT containing selected submissions to the 4th SPIN workshop, Paris, France, November 1998

Havelund K, Roşu G (2001a) Java PathExplorer – a runtime verification tool. In: Proceedings of the 6th international symposium on artificial intelligence, robotics and automation in space: a new space odyssey, Montreal, 18–21 June 2001. Canadian Space Agency. Paper AM126 on CD-ROM

Havelund K, Roşu G (2001b) Monitoring Java programs with Java PathExplorer. In: Havelund K, Roşu G (eds) Proceedings of Runtime Verification (RV’01), Paris, July 2001. Electronic notes in theoretical computer science, vol 55. Elsevier, Amsterdam

Havelund K, Roşu G (2001c) Monitoring programs using rewriting. In: Proceedings of the international conference on automated software engineering (ASE’01). Institute of Electrical and Electronics Engineers. Coronado Island, CA, November 2001, pp 135–143

Havelund K, Shankar N (1996) Experiments in theorem proving and model checking for protocol verification. In: Gaudel MC, Woodcock J (eds) Proceedings of FME’96: Industrial Benefit and Advances in Formal Methods, Oxford, UK, March 1996. Lecture notes in computer science, vol 1051. Springer, Berlin Heidelberg New York, pp 662–681

Holzmann GJ (1997) The model checker SPIN. IEEE Trans Software Eng 23(5):279–295 1997. Special issue on formal methods in software practice

Holzmann GJ, Smith MH (1999) A practical method for verifying event-driven software. In: Proceedings of the international conference on software engineering (ICSE’99), Los Angeles, May 1999. IEEE/ACM Press, New York, pp 597–607

Hsiang J (1981) Refutational theorem proving using term rewriting systems. PhD thesis, University of Illinois at Champaign-Urbana

JavaCC. Available at: http://www.webgain.com/products/java_cc

JTrek. Available at: http://www.compaq.com/java/download

Lee I, Kannan S, Kim M, Sokolsky O, Viswanathan M (1999) Runtime assurance based on formal specifications. In: Proceedings of the international conference on parallel and distributed processing techniques and applications, Las Vegas, USA, June 1999. CSREA Press

Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin Heidelberg New York

Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin Heidelberg New York

Markey N (2003) Temporal logic with past is exponentially more succinct. EATCS Bull 79:122–128

Meseguer J (1992) Conditional rewriting logic as a unified model of concurrency. Theor Comput Sci 1:73–155

Meseguer J (1997) Membership algebra as a logical framework for equational specification. In: Proceedings of the workshop on algebraic development techniques (WADT’97), Tarquinia, Italy, June 1998. Lecture notes in computer science, vol 1376. Springer, Berlin Heidelberg New York, pp 18–61

Park DY, Stern U, Skakkebaek JU, Dill DL (2000) Java model checking. In: Proceedings of the automated software engineering conference, Grenoble, France, September 2000. IEEE Computer Society, New York, pp 253–256

Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium on foundations of computer science, Providence, RI, October 1977, pp 46–77

Roşu G, Havelund K (2001) Synthesizing dynamic programming algorithms from linear temporal logic formulae. Technical Report TR 01-08, NASA – RIACS, Moffett Field, CA

Sen K, Roşu G, Agha G (2003) Runtime safety analysis of multithreaded programs. In: Proceedings of the 4th joint European software engineering conference and ACM SIGSOFT symposium on the foundations of software engineering (ESEC/FSE’03), Helsinki, September 2003. ACM Press, New York

Stoller SD (2000) Model-checking multi-threaded distributed Java programs. In: Havelund K, Penix J, Visser W (eds) SPIN model checking and software verification. Lecture notes in computer science, vol 1885. Springer, Berlin Heidelberg New York, pp 224–244

Visser W, Havelund K, Brat G, Park S (2000) Model checking programs. In: Proceedings of the 15th IEEE international conference on automated software engineering (ASE’2000), Grenoble, France, September 2000. IEEE Press, New York, pp 3–12