{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,29]],"date-time":"2025-01-29T05:57:41Z","timestamp":1738130261616,"version":"3.33.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"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":[[2009,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>SCOOP is a concurrent programming language with a new semantics for contracts that applies equally well in concurrent and sequential contexts. SCOOP eliminates race conditions and atomicity violations by construction. However, it is still vulnerable to deadlocks. In this paper we describe how far contracts can take us in verifying interesting properties of concurrent systems using modular Hoare rules and show how theorem proving methods developed for sequential Eiffel can be extended to the concurrent case. However, some safety and liveness properties depend upon the environment and cannot be proved using the Hoare rules. To deal with such system properties, we outline a SCOOP Virtual Machine (SVM) as a fair transition system. The SVM makes it feasible to use model-checking and theorem proving methods for checking global temporal logic properties of SCOOP programs. The SVM uses the Hoare rules where applicable to reduce the number of steps in a computation.<\/jats:p>","DOI":"10.1007\/s00165-008-0073-8","type":"journal-article","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T16:53:41Z","timestamp":1204304021000},"page":"319-346","source":"Crossref","is-referenced-by-count":11,"title":["Beyond contracts for concurrency"],"prefix":"10.1145","volume":"21","author":[{"given":"Jonathan S.","family":"Ostroff","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, York University, 4700 Keele Street, M3J 1P3, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Faraz Ahmadi","family":"Torshizi","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, York University, 4700 Keele Street, M3J 1P3, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hai Feng","family":"Huang","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, York University, 4700 Keele Street, M3J 1P3, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Schoeller","sequence":"additional","affiliation":[{"name":"Software Engineering, ETH Zurich, Clausiusstrasse 59, 8092, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Burdy L Cheon Y Cok D Ernst M Kiniry J Leavens GT Leino KRM Poll E (2003) An overview of JML tools and applications. In: Eighth international workshop on formal methods for industrial critical systems (FMICS 03)","DOI":"10.1016\/S1571-0661(04)80810-7"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Barnett M Chang B-YE DeLine R Jacobs B Leino KRM (2005) Boogie: a modular reusable verifier for object-oriented programs. In: Proceedings of FMCO","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_2_4_2","unstructured":"Barnett M DeLine R Jacobs B Fhndrich M Leino KRM Schulte W Venter H (2005) The spec# programming system: challenges and directions. Position paper at VSTTE"},{"issue":"2594","key":"e_1_2_1_2_5_2","first-page":"26","article-title":"Chip revolution poses problems for programmers","volume":"193","author":"Biever C","year":"2007","journal-title":"NewScientist"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Briand LC Labiche Y Sun H (2002) Investigating the use of analysis contracts to support fault isolation in object oriented code. In: ISSTA \u201902: Proceedings of the 2002 ACM SIGSOFT international symposium on software testing and analysis pp 70\u201380. ACM Press New York","DOI":"10.1145\/566172.566183"},{"key":"e_1_2_1_2_7_2","unstructured":"Barnett M Leino KRM Schulte W (2004) The spec# programming system: an overview. In: CASSIS 2004. LNCS vol 3362. Springer Heidelberg"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0033-8"},{"key":"e_1_2_1_2_9_2","unstructured":"Compton M (2000) SCOOP : an investigation of concurrency in Eiffel. Master\u2019s thesis Department of Computer Science The Australian National University"},{"key":"e_1_2_1_2_10_2","unstructured":"ECMA. Eiffel: analysis design and programming language. Standard ECMA-367 2nd edn. June 2006"},{"key":"e_1_2_1_2_11_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 the ACM SIGPLAN 2002 conference on programming language design and implementation","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Fuks O Ostroff JS Paige RF (2004) SECG: The SCOOP-to-Eiffel code generator. JOT J Object Technol 11(3)","DOI":"10.5381\/jot.2004.3.10.a3"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"issue":"4","key":"e_1_2_1_2_14_2","first-page":"72","article-title":"Model checking Java programs using Java pathfinder","volume":"2","author":"Havelund K","year":"2000","journal-title":"Software Tools Technol Transf (STTT)"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Jacobs B Leino KRM Piessens F Schulte W (2005) Safe concurrency for aggregate objects with invariants. In: Third IEEE international conference on software engineering and formal methods (SEFM\u201905) IEEE pp 137\u2013146","DOI":"10.1109\/SEFM.2005.39"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Jones CB (2003) Wanted: a compositional approach to concurrency pp 5\u201315","DOI":"10.1007\/978-0-387-21798-7_1"},{"key":"e_1_2_1_2_17_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: ICFEM pp 420\u2013439","DOI":"10.1007\/11901433_23"},{"key":"e_1_2_1_2_18_2","unstructured":"Leavens GT Leino KRM Muller P (2006) Specification and verification challenges for sequential object-oriented programs. TR 06-14 Department of Computer Science Iowa State University May 2006"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Leavens GT Leino KRM Poll E Ruby C Jacobs B (2000) JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion Minneapolis MN pp 105\u2013106","DOI":"10.1145\/367845.367996"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00165-0"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Mller P (2006) A verification methodology for model fields. In: European symposium on programming (ESOP\u201906)","DOI":"10.1007\/11693024_9"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_2_1_2_23_2","unstructured":"Meyer B (1997) Practice to perfect: the quality first model. Computer"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_2_1_2_26_2","unstructured":"Nienaltowski P (2007) Practical framework for contract-based concurrent object-oriented programming Ph.D. thesis 17031. Ph.D. thesis Department of Computer Science ETH Zurich"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Nienaltowski P Meyer B (2007) Contracts for concurrency. Formal Aspects Comput. doi:10.1007\/s00165-007-0063-2","DOI":"10.1007\/s00165-007-0063-2"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/295558.295560"},{"key":"e_1_2_1_2_29_2","unstructured":"Ostroff J Wang C-W Kerfoot E Torshizi FA (2006) Automated model-based verification of object oriented code. In: Verified software: theories tools experiments (VSTTE Workshop Floc 2006). Microsoft Research MSR-TR-2006-117"},{"key":"e_1_2_1_2_30_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 pp 551\u2013576","DOI":"10.1007\/11531142_24"},{"key":"e_1_2_1_2_31_2","unstructured":"Schoeller B (2006) Eiffel0: an object-oriented language with dynamic frame contracts. Technical Report 542 ETH Zurich"},{"key":"e_1_2_1_2_32_2","unstructured":"Schoeller B (2008) Making classes provable through contracts models and frames. PhD dissertation no. 17610 ETH Z\u00fcrich"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Visser W Havelund K Brat G Park S Lerda F (2003) Model checking programs. Automated Softw Eng J 10","DOI":"10.1023\/A:1022920129859"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-008-0073-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-008-0073-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-008-0073-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,28]],"date-time":"2025-01-28T21:10:53Z","timestamp":1738098653000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-008-0073-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["10.1007\/s00165-008-0073-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-008-0073-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2009,8]]}}}