{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T10:19:29Z","timestamp":1780827569520,"version":"3.54.1"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,4,1]],"date-time":"2005-04-01T00:00:00Z","timestamp":1112313600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Software Eng"],"published-print":{"date-parts":[[2005,4]]},"DOI":"10.1007\/s10515-005-6205-y","type":"journal-article","created":{"date-parts":[[2005,4,12]],"date-time":"2005-04-12T20:29:20Z","timestamp":1113337760000},"page":"151-197","source":"Crossref","is-referenced-by-count":143,"title":["Rewriting-Based Techniques for Runtime Verification"],"prefix":"10.1007","volume":"12","author":[{"given":"Grigore","family":"Ro\u015fu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"6205_CR1","first-page":"87","volume-title":"Proc. of ASM\u201903: Abstract State Machines, Vol. 2589 of Lecture Notes in Computer Science","author":"C. Artho","year":"2003","unstructured":"Artho, C., Drusinsky, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., Ro\u015fu, G., and Visser, W. 2003. Experiments with test case generation and runtime analysis. In Proc. of ASM\u201903: Abstract State Machines, Vol. 2589 of Lecture Notes in Computer Science, Taormina, Italy, Springer, pp. 87\u2013107."},{"key":"6205_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., and Rajamani, S. 2001. Boolean and cartesian abstractions for model checking c programs. In Proc. of TACAS\u201901: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Genova, Italy.","DOI":"10.1007\/3-540-45319-9_19"},{"key":"6205_CR3","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A. Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J.-P., and Meseguer, J. 2000. Specification and proof in membership equational logic. Theoretical Computer Science, 236:35\u2013132.","journal-title":"Theoretical Computer Science"},{"issue":"8","key":"6205_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E. 1986. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"key":"6205_CR5","first-page":"106","volume-title":"Proc. of RV\u201903: the Third International Workshop on Runtime Verification, Vol. 89 of Electronic Notes in Theoretical Computer Science","author":"F. Chen","year":"2003","unstructured":"Chen, F. and Ro\u015fu, G. 2003. Towards monitoring-oriented programming: A paradigm combining specification and implementation. In Proc. of RV\u201903: the Third International Workshop on Runtime Verification, Vol. 89 of Electronic Notes in Theoretical Computer Science, Elsevier Science, Boulder, Colorado, USA, pp. 106\u2013125."},{"key":"6205_CR6","unstructured":"Clavel, M. 2001. The ITP tool. In Logic, Language and Information. Proc. of the First Workshop on Logic and Language, Kronos, pp. 55\u201362."},{"key":"6205_CR7","doi-asserted-by":"crossref","unstructured":"Clavel, M., Dur\u00e1n, F.J., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., and Quesada., J.F. 1999. Maude: Specification and programming in rewriting logic, Maude System documentation at http:\/\/maude.csl.sri.com\/papers.","DOI":"10.1007\/3-540-48685-2_18"},{"key":"6205_CR8","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F.J., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., and Quesada., J.F. 2002. Maude: Specification and programming in rewriting logic. Theoretical Computer Science, 285:187\u2013243.","journal-title":"Theoretical Computer Science"},{"key":"6205_CR9","volume-title":"Proc. of ICSE\u201900: International Conference on Software Engineering","author":"J. Corbett","year":"2000","unstructured":"Corbett, J., Dwyer, M.B., Hatcliff, J., Pasareanu, C.S., Robby, Laubach S., and Zheng., H. 2000. Bandera: Extracting finite-state models from java source code. In Proc. of ICSE\u201900: International Conference on Software Engineering, Limerich, Ireland, ACM Press."},{"key":"6205_CR10","unstructured":"Dahm., M. BCEL. +http:\/\/jakarta.apache.org\/bcel+."},{"issue":"7","key":"6205_CR11","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. Demartini","year":"1999","unstructured":"Demartini, C., Iosif, R., and Sisto., R. 1999. A deadlock detection tool for concurrent java programs. Software Practice and Experience, 29(7):577\u2013603.","journal-title":"Software Practice and Experience"},{"key":"6205_CR12","first-page":"323","volume-title":"Proc. of SPIN\u201900: SPIN Model Checking and Software Verification, Vol. 1885 of Lecture Notes in Computer Science","author":"D. Drusinsky","year":"2000","unstructured":"Drusinsky, D. 2000. The temporal rover and the atg rover. In Proc. of SPIN\u201900: SPIN Model Checking and Software Verification, Vol. 1885 of Lecture Notes in Computer Science, Springer Stanford, California, USA, pp. 323\u2013330."},{"key":"6205_CR13","first-page":"114","volume-title":"Proc. of CAV\u201903: Computer Aided Verification, Vol. 2725 of Lecture Notes in Computer Science","author":"D. Drusinsky","year":"2003","unstructured":"Drusinsky, D. 2003. Monitoring temporal rules combined with time series. In Proc. of CAV\u201903: Computer Aided Verification, Vol. 2725 of Lecture Notes in Computer Science, Springer-Verlag, Boulder, Colorado, USA, pp. 114\u2013118."},{"key":"6205_CR14","doi-asserted-by":"crossref","unstructured":"Fidge, C.J. 1988. Partial orders for parallel debugging. In Proc. of the 1988 ACM SIGPLAN and SIGOPS workshop on Parallel and Distributed Debugging, ACM, pp. 183\u2013194.","DOI":"10.1145\/68210.69233"},{"key":"6205_CR15","volume-title":"Proc. of RV\u201902: The Second International Workshop on Runtime Verification, volume 70 of Electronic Notes in Theoretical Computer Science","author":"B. Finkbeiner","year":"2002","unstructured":"Finkbeiner, B., Sankaranarayanan, S., and Sipma, H. 2002. Collecting statistics over runtime executions. In Proc. of RV\u201902: The Second International Workshop on Runtime Verification, volume 70 of Electronic Notes in Theoretical Computer Science, Elsevier, Paris, France."},{"key":"6205_CR16","volume-title":"Proc. of RV\u201901: The First International Workshop on Runtime Verification, Vol. 55(2) of Electronic Notes in Theoretical Computer Science","author":"B. Finkbeiner","year":"2001","unstructured":"Finkbeiner, B. and Sipma, H. 2001. Checking finite traces using alternating automata. In Proc. of RV\u201901: The First International Workshop on Runtime Verification, Vol. 55(2) of Electronic Notes in Theoretical Computer Science, Elsevier Science, Paris, France."},{"key":"6205_CR17","first-page":"412","volume-title":"Proc. of ASE\u201901: International Conference on Automated Software Engineering","author":"D. Giannakopoulou","year":"2001","unstructured":"Giannakopoulou, D. and Havelund, K. 2001. Automata-based verification of temporal properties on running programs. In Proc. of ASE\u201901: International Conference on Automated Software Engineering, Institute of Electrical and Electronics Engineers, Coronado Island, California, pp. 412\u2013416."},{"key":"6205_CR18","doi-asserted-by":"crossref","unstructured":"Godefroid, P. 1997. Model checking for programming languages using verisoft. In Proc. of POPL\u201997: the 24th ACM Symposium on Principles of Programming Languages, Paris, France, pp. 174\u2013186.","DOI":"10.1145\/263699.263717"},{"key":"6205_CR19","doi-asserted-by":"crossref","unstructured":"Goguen, J., Lin, K., Ro\u015fu, G., Mori, A., and Warinschi, B. 2000. An overview of the Tatami project. In Cafe: An Industrial-Strength Algebraic Formal Method, Elsevier, pp. 61\u201378.","DOI":"10.1016\/B978-044450556-9\/50063-0"},{"issue":"1","key":"6205_CR20","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/321992.321997","volume":"24","author":"J. Goguen","year":"1977","unstructured":"Goguen, J., Thatcher, J., Wagner, E., and Wright, J. 1977. Initial algebra semantics and continuous algebras. Journal of the Association for Computing Machinery, 24(1):68\u201395.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"6205_CR21","doi-asserted-by":"crossref","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., and Jouannaud, J.-P. 2000. Introducing OBJ. In Software Engineering with OBJ: Algebraic Specification in Action, Kluwer.","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"6205_CR22","volume-title":"Proc. of RV\u201902: Second International Workshop on Runtime Verification, volume 70 of Electronic Notes in Theoretical Computer Science","author":"E. Gunter","year":"2002","unstructured":"Gunter, E. and Peled, D. 2002. Tracing the executions of concurrent programs. In Proc. of RV\u201902: Second International Workshop on Runtime Verification, volume 70 of Electronic Notes in Theoretical Computer Science, Elsevier, Copenhagen, Denmark."},{"key":"6205_CR23","first-page":"552","volume-title":"Proc. of CAV\u201900: Computer Aided Verification, Vol. 1885 of Lecture Notes in Computer Science","author":"E.L. Gunter","year":"2003","unstructured":"Gunter, E.L., Kurshan, R.P., and Peled, D. 2003. PET: An interactive software testing tool. In Proc. of CAV\u201900: Computer Aided Verification, Vol. 1885 of Lecture Notes in Computer Science, Springer-Verlag, Chicago, Illinois, USA, pp. 552\u2013556."},{"key":"6205_CR24","unstructured":"Gunter, E.L. and Peled, D. 2000. Using functional languages in formal methods: The PET system. In Parallel and Distributed Processing Techniques and Applications, CSREA, pp. 2981\u20132986."},{"key":"6205_CR25","volume-title":"Proc. of the European Space Agency workshop on On-Board Autonomy","author":"K. Havelund","year":"2001","unstructured":"Havelund, K., Johnson, S., and Ro\u015fu, G. 2001. Specification and error pattern based program monitoring. In Proc. of the European Space Agency workshop on On-Board Autonomy, Noordwijk, The Netherlands."},{"issue":"8","key":"6205_CR26","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K. Havelund","year":"2001","unstructured":"Havelund, K., Lowry, M.R., and Penix, J. 2001. Formal analysis of a space craft controller using SPIN. IEEE Transactions on Software Engineering, 27(8):749\u2013765, An earlier version occurred in the Proc. of SPIN\u201998: the fourth SPIN workshop, Paris, France, 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"6205_CR27","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K. and Pressburger, T. 2000. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4):366\u2013381, Special issue containing selected submissions to SPIN\u201998: the fourth SPIN workshop, Paris, France, 1998.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"6205_CR28","unstructured":"Havelund, K. and Ro\u015fu, G. 2001. Java PathExplorer\u2014A Runtime verification tool. In Proc. of i-SAIRAS\u201901: the 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space, Montreal, Canada."},{"key":"6205_CR29","first-page":"97","volume-title":"Proc. of RV\u201901: the First International Workshop on Runtime Verification, volume 55 of Electronic Notes in Theoretical Computer Science","author":"K. Havelund","year":"2001","unstructured":"Havelund, K. and Ro\u015fu, G. 2001. Monitoring Java programs with java pathexplorer. In Proc. of RV\u201901: the First International Workshop on Runtime Verification, volume 55 of Electronic Notes in Theoretical Computer Science, Paris, France, Elsevier Science, pp. 97\u2013114."},{"key":"6205_CR30","first-page":"135","volume-title":"Proc. of ASE\u201901: International Conference on Automated Software Engineering","author":"K. Havelund","year":"2001","unstructured":"Havelund, K. and Ro\u015fu, G. 2001. Monitoring programs using rewriting. In Proc. of ASE\u201901: International Conference on Automated Software Engineering, Institute of Electrical and Electronics Engineers, Coronado Island, California, USA, pp. 135\u2013143."},{"key":"6205_CR31","unstructured":"Havelund, K. and Ro\u015fu, G. 2001. Testing linear temporal logic formulae on finite execution traces. Technical Report TR 01-08, RIACS, Written 20."},{"key":"6205_CR32","unstructured":"Havelund, K. and Ro\u015fu, G. to appear Efficient monitoring of safety properties. Software Tools and Technology Transfer."},{"key":"6205_CR33","first-page":"342","volume-title":"Proc. of TACAS\u201902: Tools and Algorithms for Construction and Analysis of Systems, Vol. 2280 of Lecture Notes in Computer Science","author":"K. Havelund","year":"2002","unstructured":"Havelund, K. and Ro\u015fu, G. 2002. Synthesizing monitors for safety properties. In Proc. of TACAS\u201902: Tools and Algorithms for Construction and Analysis of Systems, Vol. 2280 of Lecture Notes in Computer Science, Springer, Grenoble, France, pp. 342\u2013356."},{"key":"6205_CR34","first-page":"662","volume-title":"Proc. of FME\u201996: Industrial Benefit and Advances in Formal Methods, Vol. 1051 of Lecture Notes in Computer Science","author":"K. Havelund","year":"1996","unstructured":"Havelund, K. and Shankar, N. 1996. Experiments in theorem proving and model checking for protocol verification. In Proc. of FME\u201996: Industrial Benefit and Advances in Formal Methods, Vol. 1051 of Lecture Notes in Computer Science, Springer, Oxford, England, pp. 662\u2013681"},{"key":"6205_CR35","volume-title":"Proc. of ICSE\u201999: International Conference on Software Engineering","author":"G.J. Holzmann","year":"1999","unstructured":"Holzmann, G.J. and Smith, M.H. 1999. A practical method for verifying event-driven software. In Proc. of ICSE\u201999: International Conference on Software Engineering, IEEE\/ACM, Los Angeles, California, USA."},{"key":"6205_CR36","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft, J. and Ullman, J. 1979. Introduction to Automata Theory, Languages, and Computation. Reading, Massachusetts: Addison-Wesley."},{"key":"6205_CR37","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"J. Hsiang","year":"1985","unstructured":"Hsiang, J. 1985. Refutational theorem proving using term rewriting systems. Artificial Intelligence, 25:255\u2013300.","journal-title":"Artificial Intelligence"},{"key":"6205_CR38","volume-title":"Proc. of RV\u201901: First International Workshop on Runtime Verification, Vol. 55 of Electronic Notes in Theoretical Computer Science","author":"M. Kim","year":"2001","unstructured":"Kim, M., Kannan, S., Lee, I., and Sokolsky, O. 2001. Java-MaC: A Run-time assurance tool for Java. In Proc. of RV\u201901: First International Workshop on Runtime Verification, Vol. 55 of Electronic Notes in Theoretical Computer Science, Elsevier Science, Paris, France."},{"key":"6205_CR39","volume-title":"Proc. of RV\u201901: First International Workshop on Runtime Verification, volume 55 of Electronic Notes in Theoretical Computer Science","author":"D. Kortenkamp","year":"2001","unstructured":"Kortenkamp, D., Milam, T., Simmons, R., and Fernandez, J. 2001. Collecting and analyzing data from distributed control programs. In Proc. of RV\u201901: First International Workshop on Runtime Verification, volume 55 of Electronic Notes in Theoretical Computer Science, Elsevier Science, Paris, France."},{"key":"6205_CR40","doi-asserted-by":"crossref","unstructured":"Kupferman, O. and Vardi, M.Y. 1998. Freedom, weakness, and determinism: From linear-time to branching-Time. In Proc. of the IEEE Symposium on Logic in Computer Science, pp. 81\u201392.","DOI":"10.1109\/LICS.1998.705645"},{"key":"6205_CR41","doi-asserted-by":"crossref","unstructured":"Kupferman, O. and Vardi, M.Y. 1999. Model checking of safety properties. In Proc. of CAV\u201999: Conference on Computer-Aided Verification, Trento, Italy.","DOI":"10.1007\/3-540-48683-6_17"},{"key":"6205_CR42","doi-asserted-by":"crossref","unstructured":"Kupferman, O. and Zuhovitzky, S. 2002. An improved algorithm for the membership problem for extended regular expressions. In Proc. of the International Symposium on Mathematical Foundations of Computer Science, Vol. 2420 of Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-45687-2_37"},{"key":"6205_CR43","unstructured":"Lee, I., Kannan, S., Kim, M., Sokolsky, O., and Viswanathan, M. 1999. Runtime assurance based on formal specifications. In Proc. of PDPTA\u201999: International Conference on Parallel and Distributed Processing Techniques and Applications, Las Vegas, Nevada, USA."},{"key":"6205_CR44","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z. and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems. New York: Springer."},{"key":"6205_CR45","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z. and Pnueli, 1995. Temporal Verification of Reactive Systems: Safety. New York: Springer."},{"key":"6205_CR46","first-page":"251","volume-title":"Proc. of CONCUR\u201903: International Conference on Concurrency Theory, Vol. 2761 of Lecture Notes in Computer Science","author":"N. Markey","year":"2003","unstructured":"Markey, N. and Schnoebelen, P. 2003. Model checking a path (Preliminary Report). In Proc. of CONCUR\u201903: International Conference on Concurrency Theory, Vol. 2761 of Lecture Notes in Computer Science, Springer, Marseille, France, pp. 251\u2013265."},{"key":"6205_CR47","doi-asserted-by":"crossref","unstructured":"Meseguer, J. 1992. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 73\u2013155.","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"6205_CR48","first-page":"18","volume-title":"Proc. of WADT\u201997: Workshop on Algebraic Development Techniques, Vol. 1376 of Lecture Notes in Computer Science","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J. 1998. Membership algebra as a logical framework for equational specification. In Proc. of WADT\u201997: Workshop on Algebraic Development Techniques, Vol. 1376 of Lecture Notes in Computer Science, Springer, Tarquinia, Italy, pp. 18\u201361."},{"key":"6205_CR49","unstructured":"O\u2019Malley, T., Richardson, D., and Dillon, L. 1996. Efficient specification-based oracles for critical systems. In Proc. of the California Software Symposium."},{"key":"6205_CR50","doi-asserted-by":"crossref","unstructured":"Park, D.Y., Stern, U., and Dill, D.L. 2000. Java model checking. In Proc. of the First International Workshop on Automated Program Analysis, Testing and Verification, Limerick, Ireland.","DOI":"10.1109\/ASE.2000.873671"},{"key":"6205_CR51","doi-asserted-by":"crossref","unstructured":"Pnueli, A. 1977. The temporal logic of programs. In Proc. of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201377.","DOI":"10.1109\/SFCS.1977.32"},{"key":"6205_CR52","unstructured":"Richardson, D.J., Aha, S.L., and O\u2019Malley, T.O. 1992. Specification-based test oracles for reactive systems. In Proc. of ICSE\u201992: International Conference on Software Engineering, Melbourne, Australia, pp. 105\u2013118."},{"key":"6205_CR53","unstructured":"Ro\u015fu, G. and Havelund, K. 2001. Synthesizing dynamic programming algorithms from linear temporal logic formulae. RIACS Technical report TR 01-08."},{"key":"6205_CR54","first-page":"499","volume-title":"Proc. of RTA\u201903: Rewriting Techniques and Applications, Vol. 2706 of Lecture Notes in Computer Science","author":"G. Ro\u015fu","year":"2003","unstructured":"Ro\u015fu, G. and Viswanathan, M. 2003. Testing extended regular language membership incrementally by rewriting. In Proc. of RTA\u201903: Rewriting Techniques and Applications, Vol. 2706 of Lecture Notes in Computer Science, Valencia, Spain, Springer-Verlag, pp. 499\u2013514."},{"issue":"4","key":"6205_CR55","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., and Anderson, T. 1997. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 15(4):391\u2013411.","journal-title":"ACM Transactions on Computer Systems"},{"key":"6205_CR56","doi-asserted-by":"crossref","unstructured":"Sen, A. and Garg, V.K. 2003. Partial order trace analyzer (POTA) for distrubted programs. In Proc. of RV\u201903: the Third International Workshop on Runtime Verification, Vol. 89 of Electronic Notes in Theoretical Computer Science, Boulder, Elsevier Science, Colorado, USA.","DOI":"10.1016\/S1571-0661(04)81041-7"},{"key":"6205_CR57","first-page":"162","volume-title":"Proc. of RV\u201903: the Third International Workshop on Runtime Verification, volume 89 of Electronic Notes in Theoretical Computer Science","author":"K. Sen","year":"2003","unstructured":"Sen, K. and Ro\u015fu, G. 2003. Generating optimal monitors for extended regular expressions. In Proc. of RV\u201903: the Third International Workshop on Runtime Verification, volume 89 of Electronic Notes in Theoretical Computer Science, Elsevier Science, Boulder, Colorado, USA, pp. 162\u2013181."},{"key":"6205_CR58","volume-title":"Proc. of ESEC\/FSE\u201903: European Software Engineering Conference and ACM SIGSOFT International Symposium on the Foundations of Software Engineering","author":"K. Sen","year":"2003","unstructured":"Sen, K., Ro\u015fu, G., and Agha, G. 2003. Runtime safety analysis of multithreaded programs. In Proc. of ESEC\/FSE\u201903: European Software Engineering Conference and ACM SIGSOFT International Symposium on the Foundations of Software Engineering. ACM, Helsinki, Finland."},{"key":"6205_CR59","unstructured":"Shankar, N., Owre, S., and Rushby, J.M. 1993. PVS Tutorial. Computer science laboratory, SRI International, Menlo Park, CA, 1993. Also appears in Tutorial Notes, Formal Methods Europe \u201893: Industrial-Strength Formal Methods, Odense, Denmark, pp. 357\u2013406."},{"issue":"3","key":"6205_CR60","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P. and Clarke, E.M. 1985. The Complexity of propositional linear temporal logics. Journal of the ACM (JACM), 32(3):733\u2013749.","journal-title":"Journal of the ACM (JACM)"},{"key":"6205_CR61","first-page":"224","volume-title":"Proc. of SPIN\u201900: SPIN Model Checking and Software Verification, Vol. 1885 of Lecture Notes in Computer Science","author":"S.D. Stoller","year":"2000","unstructured":"Stoller, S.D. 2000. Model-checking multi-threaded distributed java programs. In Proc. of SPIN\u201900: SPIN Model Checking and Software Verification, Vol. 1885 of Lecture Notes in Computer Science, Springer, Stanford, California, USA, pp. 224\u2013244."},{"key":"6205_CR62","volume-title":"Proc. of ASE\u201900: International Conference on Automated Software Engineering","author":"W. Visser","year":"2000","unstructured":"Visser, W., Havelund, K., Brat, G., and Park, S. 2000. Model checking programs. In Proc. of ASE\u201900: International Conference on Automated Software Engineering, IEEE CS Press, Grenoble, France."},{"key":"6205_CR63","doi-asserted-by":"crossref","unstructured":"Yamamoto, H. 2000. An automata-based recognition algorithm for semi-extended regular expressions. In Proc. of the International Symposium on Mathematical Foundations of Computer Science, Vol. 1893 of Lecture Notes in Computer Science, pp. 699\u2013708.","DOI":"10.1007\/3-540-44612-5_65"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-005-6205-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-005-6205-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-005-6205-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T20:05:03Z","timestamp":1586203503000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-005-6205-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,4]]},"references-count":63,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["6205"],"URL":"https:\/\/doi.org\/10.1007\/s10515-005-6205-y","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,4]]}}}