{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:26:50Z","timestamp":1750307210933,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T00:00:00Z","timestamp":1327363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2012,1,24]]},"DOI":"10.1145\/2103776.2103782","type":"proceedings-article","created":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T16:47:19Z","timestamp":1327423639000},"page":"37-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A hoare calculus for the verification of synchronous languages"],"prefix":"10.1145","author":[{"given":"Manuel","family":"Gesell","sequence":"first","affiliation":[{"name":"TU Kaiserslautern, Kaiserslautern, Germany"}]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[{"name":"TU Kaiserslautern, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2012,1,24]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/358568.358586"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2714-2","volume-title":"Verification of Sequential and Concurrent Programs","author":"Apt K.","year":"1997","unstructured":"K. Apt and E.-R. Olderog . Verification of Sequential and Concurrent Programs . Springer , 2 edition, 1997 . K. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer, 2 edition, 1997."},{"key":"e_1_3_2_1_5_1","series-title":"LNCS","first-page":"158","volume-title":"J.-P","author":"Ball T.","year":"2002","unstructured":"T. Ball , A. Podelski , and S. Rajamani . Relative completeness of abstraction refinement for software model checking . In J.-P . Katoen and P. Stevens, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2280 of LNCS , pages 158 -- 172 , Grenoble, France, 2002 . Springer . T. Ball, A. Podelski, and S. Rajamani. Relative completeness of abstraction refinement for software model checking. In J.-P. Katoen and P. Stevens, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2280 of LNCS, pages 158--172, Grenoble, France, 2002. Springer."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_3_2_1_7_1","unstructured":"G. Berry. The constructive semantics of pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org\/ July 1999.  G. Berry. The constructive semantics of pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org\/ July 1999."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/355592.365646"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_13"},{"key":"e_1_3_2_1_10_1","volume-title":"Oldenburg","author":"Brandt J.","year":"2011","unstructured":"J. Brandt and K. Schneider . Round trip to asynchrony and synchrony. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV) , Oldenburg , Germany , 2011 . J. Brandt and K. Schneider. Round trip to asynchrony and synchrony. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Oldenburg, Germany, 2011."},{"key":"e_1_3_2_1_12_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-15670-4","volume-title":"Seminar on Concurrency (CONCUR)","author":"Brookes S.","year":"1985","unstructured":"S. Brookes . On the axiomatic treatment of concurrency . In S. Brookes, A. Roscoe, and G. Winskel, editors, Seminar on Concurrency (CONCUR) , volume 197 of LNCS , pages 1 -- 34 , Pittsburgh, Pennsylvania, USA , 1985 . Springer . S. Brookes. On the axiomatic treatment of concurrency. In S. Brookes, A. Roscoe, and G. Winskel, editors, Seminar on Concurrency (CONCUR), volume 197 of LNCS, pages 1--34, Pittsburgh, Pennsylvania, USA, 1985. Springer."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/321707.321720"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040026.56959.91"},{"key":"e_1_3_2_1_15_1","first-page":"841","volume-title":"Handbook of Theoretical Computer Science","author":"Cousot P.","year":"1990","unstructured":"P. Cousot . Methods and logics for proving programs . In J. van Leeuwen, editor, Handbook of Theoretical Computer Science , volume B: Formal Models and Semantics, chapter 15 , pages 841 -- 993 . Elsevier , 1990 . P. Cousot. Methods and logics for proving programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 15, pages 841--993. Elsevier, 1990."},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/BFb0058036","volume-title":"Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"de Boer F.","year":"1997","unstructured":"F. de Boer , U. Hannemann , and W.-P. de Roever . Hoare-style compositional proof systems for reactive shared variable concurrency . In S. Ramesh and G. Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS) , volume 1346 of LNCS , pages 267 -- 283 , Kharagpur, India , 1997 . Springer . F. de Boer, U. Hannemann, and W.-P. de Roever. Hoare-style compositional proof systems for reactive shared variable concurrency. In S. Ramesh and G. Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1346 of LNCS, pages 267--283, Kharagpur, India, 1997. Springer."},{"key":"e_1_3_2_1_17_1","volume-title":"Cambridge University Press","author":"de Roever W.","year":"2001","unstructured":"W. de Roever . Concurrency Verification . Cambridge University Press , 2001 . W. de Roever. Concurrency Verification. Cambridge University Press, 2001."},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/3-540-40911-4_13","volume-title":"Integrated Formal Methods (IFM)","author":"Dingel J.","year":"2000","unstructured":"J. Dingel . Towards a unified development methodology for shared-variable parallel and distributed programs . In W. Grieskamp, T. Santen, and B. Stoddart, editors, Integrated Formal Methods (IFM) , volume 1945 of LNCS , pages 214 -- 234 , Dagstuhl, Germany , 2000 . Springer . J. Dingel. Towards a unified development methodology for shared-variable parallel and distributed programs. In W. Grieskamp, T. Santen, and B. Stoddart, editors, Integrated Formal Methods (IFM), volume 1945 of LNCS, pages 214--234, Dagstuhl, Germany, 2000. Springer."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233800"},{"key":"e_1_3_2_1_20_1","series-title":"Symposia in Applied Mathematics","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer Science","author":"Floyd R.","year":"1967","unstructured":"R. Floyd . Assigning meanings to programs. In J. Schwartz, editor, Mathematical Aspects of Computer Science , volume 19 of Symposia in Applied Mathematics , pages 19 -- 32 , Providence, Rhode Island, USA , 1967 . American Mathematical Society. R. Floyd. Assigning meanings to programs. In J. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Symposia in Applied Mathematics, pages 19--32, Providence, Rhode Island, USA, 1967. American Mathematical Society."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/535661"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/530328"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_25_1","series-title":"LNCS","first-page":"185","volume-title":"J. Joyce and C.-J","author":"Joyce J.","year":"1994","unstructured":"J. Joyce and C.-J. Seger . The HOL-Voss system: Model-checking inside a general-purpose theorem-prover . In J. Joyce and C.-J . Seger, editors, Theorem Proving in Higher Order Logics (TPHOL), volume 780 of LNCS , pages 185 -- 198 , Vancouver, British Columbia, Canada, 1994 . Springer . J. Joyce and C.-J. Seger. The HOL-Voss system: Model-checking inside a general-purpose theorem-prover. In J. Joyce and C.-J. Seger, editors, Theorem Proving in Higher Order Logics (TPHOL), volume 780 of LNCS, pages 185--198, Vancouver, British Columbia, Canada, 1994. Springer."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_39"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/307988.307989"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289062"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993.357247"},{"key":"e_1_3_2_1_31_1","volume-title":"The concurrent assignment representation of synchronous systems. Parallel Computing, 9(2):227--256","author":"Martin A.","year":"1989","unstructured":"A. Martin and J. Tucker . The concurrent assignment representation of synchronous systems. Parallel Computing, 9(2):227--256 , 1989 . A. Martin and J. Tucker. The concurrent assignment representation of synchronous systems. Parallel Computing, 9(2):227--256, 1989."},{"key":"e_1_3_2_1_32_1","volume-title":"Thinking and programming in parallel","author":"Metaxas P.","year":"1997","unstructured":"P. Metaxas . Thinking and programming in parallel , 1997 . Lecture Notes . P. Metaxas. Thinking and programming in parallel, 1997. Lecture Notes."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/360569.360659"},{"key":"e_1_3_2_1_34_1","volume-title":"NVIDIA CUDA Compute Unified Device Architecture -- Programming Guide","author":"Nvidia Corporation","year":"2008","unstructured":"Nvidia Corporation . NVIDIA CUDA Compute Unified Device Architecture -- Programming Guide . Nvidia Corporation , 2008 . Nvidia Corporation. NVIDIA CUDA Compute Unified Device Architecture -- Programming Guide. Nvidia Corporation, 2008."},{"key":"e_1_3_2_1_35_1","volume-title":"An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319--340","author":"Owicki S.","year":"1976","unstructured":"S. Owicki and D. Gries . An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319--340 , 1976 . S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319--340, 1976."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"e_1_3_2_1_38_1","volume-title":"Compiling Esterel","author":"Potop-Butucaru D.","year":"2007","unstructured":"D. Potop-Butucaru , S. Edwards , and G. Berry . Compiling Esterel . Springer , 2007 . D. Potop-Butucaru, S. Edwards, and G. Berry. Compiling Esterel. Springer, 2007."},{"key":"e_1_3_2_1_40_1","first-page":"78","volume-title":"Application of Concurrency to System Design (ACSD)","author":"Schneider K.","year":"2008","unstructured":"K. Schneider and J. Brandt . Performing causality analysis by bounded model checking . In Application of Concurrency to System Design (ACSD) , pages 78 -- 87 , Xi'an, China, 2008 . IEEE Computer Society . K. Schneider and J. Brandt. Performing causality analysis by bounded model checking. In Application of Concurrency to System Design (ACSD), pages 78--87, Xi'an, China, 2008. IEEE Computer Society."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.028"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2005.24"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1360612.1360617"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90033-3"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.01.024"},{"key":"e_1_3_2_1_46_1","volume-title":"October","author":"Tini S.","year":"2001","unstructured":"S. Tini . An axiomatic semantics for Esterel. Theoretical Computer Science (TCS), 269(1--2):231--282 , October 2001 . S. Tini. An axiomatic semantics for Esterel. Theoretical Computer Science (TCS), 269(1--2):231--282, October 2001."}],"event":{"name":"POPL '12: The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"Philadelphia Pennsylvania USA","acronym":"POPL '12"},"container-title":["Proceedings of the sixth workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103776.2103782","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2103776.2103782","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:35Z","timestamp":1750241195000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103776.2103782"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,24]]},"references-count":42,"alternative-id":["10.1145\/2103776.2103782","10.1145\/2103776"],"URL":"https:\/\/doi.org\/10.1145\/2103776.2103782","relation":{},"subject":[],"published":{"date-parts":[[2012,1,24]]},"assertion":[{"value":"2012-01-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}