{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T06:37:20Z","timestamp":1648708640057},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,5,1]],"date-time":"2013-05-01T00:00:00Z","timestamp":1367366400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present MODL, a Dynamic Logic and a deductive verification calculus for a core Java-like language that includes multi-threading. The calculus is based on symbolic execution. Even though we currently do not handle non-atomic loops, employing the technique of symmetry reduction allows us to verify systems without limits on state space or thread number. We have instantiated our logic for (restricted) multi-threaded Java programs and implemented the verification calculus within the KeY system. We demonstrate our approach by verifying a central method of the StringBuffer class from the Java standard library in the presence of unbounded concurrency.<\/jats:p>","DOI":"10.1007\/s00165-012-0261-4","type":"journal-article","created":{"date-parts":[[2012,10,29]],"date-time":"2012-10-29T19:07:41Z","timestamp":1351537661000},"page":"405-437","source":"Crossref","is-referenced-by-count":0,"title":["A Dynamic Logic for deductive verification of multi-threaded programs"],"prefix":"10.1145","volume":"25","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[{"name":"Institute for Theoretical Informatics, Karlsruhe Institute of Technology, 76131, Karlsruhe, Germany"}]},{"given":"Vladimir","family":"Klebanov","sequence":"additional","affiliation":[{"name":"Institute for Theoretical Informatics, Karlsruhe Institute of Technology, 76131, Karlsruhe, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.019"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/1119479.1119480"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80018-3"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.4.549"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Beckert B H\u00e4hnle R Schmitt PH (eds) (2007) Verification of object-oriented software: the KeY approach. LNCS vol 4334. Springer Berlin","DOI":"10.1007\/978-3-540-69061-0"},{"key":"e_1_2_1_2_6_2","unstructured":"Bradbury JS Jalbert K (2009) Defining a catalog of programming anti-patterns for concurrent Java. In: Proceedings of the 3rd international workshop on software patterns and quality (SPAQu\u201909) pp 6\u201311"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Beckert B Platzer A (2006) Dynamic logic with non-rigid functions: a basis for object-oriented program verification. In: Furbach U Shankar N (eds) Proceedings of international joint conference on automated reasoning Seattle USA. LNCS vol 4130 pp 266\u2013280. Springer Berlin","DOI":"10.1007\/11814771_23"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0073-x"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"de Boer FS (2007) A sound and complete shared-variable concurrency model for multi-threaded Java programs. In: Bonsangue MM Johnsen EB (eds) Formal methods for open object-based distributed systems. Proceedings of 9th IFIP WG 6.1 International Conference FMOODS 2007 Paphos Cyprus June 6\u20138 2007. LNCS vol 4468. Springer Berlin pp 252\u2013268","DOI":"10.1007\/978-3-540-72952-5_16"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Delzanno G Raskin J-F Van Begin L (2002) Towards the automated verification of multithreaded Java programs. In: Katoen J-P Stevens P (eds) Proceedings of 8th international conference on tools and algorithms for the construction and analysis of systems (TACAS). LNCS vol 2280. Springer Berlin pp 173\u2013187","DOI":"10.1007\/3-540-46002-0_13"},{"key":"e_1_2_1_2_11_2","unstructured":"Eytani Y Ur S (2004) Compiling a benchmark of documented multi-threaded bugs. In: Proceedings of 18th international parallel and distributed processing symposium (IPDPS 2004). IEEE Computer Society"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Freund SN (2004) Atomizer: a dynamic atomicity checker for multithreaded programs. In: POPL \u201904: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM New York pp 256\u2013267","DOI":"10.1145\/964001.964023"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Leino KRM Lillibridge M Nelson G Saxe JB Stata R (2002) Extended static checking for Java. In: Proceedings of ACM SIGPLAN 2002 conference on programming language design and implementation. ACM Press Berlin pp 234\u2013245","DOI":"10.1145\/543552.512558"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Greenhouse A Scherlis WL (2002) Assuring and evolving concurrent programs: annotations and policy. In: ICSE \u201902: Proceedings of the 24th international conference on software engineering pp 453\u2013463","DOI":"10.1145\/581339.581395"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_2_16_2","unstructured":"Jacks is an automated compiler killing suite. http:\/\/www.sourceware.org\/mauve\/jacks.html"},{"key":"e_1_2_1_2_17_2","unstructured":"Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis Oxford University"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Jacobs B Poll E (2001) A logic for the Java modeling language JML. In: Proceedings of 4th international conference on fundamental approaches to software engineering (FASE). Springer Berlin pp 284\u2013299","DOI":"10.1007\/3-540-45314-8_21"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Jacobs B Smans J Piessens F Schulte W (2006) A statically verifiable programming model for concurrent object-oriented programs. In: Liu Z He J (eds) Proceedings of 8th international conference on formal engineering methods ICFEM Macao China. LNCS vol 4260. Springer Berlin pp 420\u2013439","DOI":"10.1007\/11901433_23"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Klebanov V (2004) A JMM-faithful non-interference calculus for Java. In: Proceedings of 4th international workshop on Scientific engineering of distributed Java applications Luxembourg-Kirchberg. LNCS vol 3409. Springer Berlin pp 101\u2013111","DOI":"10.1007\/978-3-540-31869-9_10"},{"key":"e_1_2_1_2_23_2","unstructured":"Klebanov V (2009) Extending the reach and power of deductive program verification. PhD thesis Department of Computer Science Universit\u00e4t Koblenz-Landau"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Khurshid S Pasareanu CS Visser W (2003) Generalized symbolic execution for model checking and testing. In: Garavel H Hatcliff J (eds) Proceedings of 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS). LNCS vol 2619. Springer Berlin pp 553\u2013568","DOI":"10.1007\/3-540-36577-X_40"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Manna Z Pnueli A (1991) Completing the temporal picture. In: Selected papers of the 16th international colloquium on automata languages and programming. Elsevier Amsterdam pp 97\u2013130","DOI":"10.1016\/0304-3975(91)90041-Y"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90035-3"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/23005.23008"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Poetzsch-Heffter A M\u00fcller P (1999) A programming logic for sequential Java. In: Swierstra D (ed) Proceedings of ESOP \u201999. LNCS vol 1576. Springer Berlin","DOI":"10.1007\/3-540-49099-X_11"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez E Dwyer MB Flanagan C Hatcliff J Leavens GT Robby (2005) Extending JML for modular specification and verification of multi-threaded programs. In: ECOOP. LNCS vol 3586. Springer Berlin pp 551\u2013576","DOI":"10.1007\/11531142_24"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Robby Dwyer MB Hatcliff J (2003) Bogor: an extensible and highly-modular software model checking framework. In: ESEC\/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on foundations of software engineering. ACM New York pp 267\u2013276","DOI":"10.1145\/949952.940107"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Robby Dwyer MB Hatcliff J Iosif R (2003) Space-reduction strategies for model checking dynamic software. In: Proceedings SoftMC 2003 workshop on software model checking ENTCS 89","DOI":"10.1016\/S1571-0661(05)80001-5"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.598"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Vafeiadis V Parkinson MJ (2007) A marriage of Rely\/Guarantee and Separation Logic. In: Caires L Vasconcelos VT (eds) Proceedings 18th international conference on concurrency theory (CONCUR 2007) Lisbon Portugal. LNCS vol 4703. Springer Berlin pp 256\u2013271","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Yahav E (2001) Verifying safety properties of concurrent Java programs using 3-valued logic. In: POPL \u201901: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM Press New York pp 27\u201340","DOI":"10.1145\/360204.360206"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Zee K Kuncak V Rinard MC (2008) Full functional verification of linked data structures. In: Gupta R Amarasinghe SP (eds) Proceedings of the ACM SIGPLAN 2008 conference on programming language design and implementation Tucson AZ USA June 7\u201313 2008. ACM New York pp 349\u2013361","DOI":"10.1145\/1379022.1375624"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0261-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0261-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0261-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:53:47Z","timestamp":1641484427000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0261-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,5]]}},"alternative-id":["10.1007\/s00165-012-0261-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0261-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5]]}}}