{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:03:44Z","timestamp":1743001424422,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642277047"},{"type":"electronic","value":"9783642277054"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_11","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T12:18:06Z","timestamp":1327493886000},"page":"130-145","source":"Crossref","is-referenced-by-count":6,"title":["A Comparison of Intermediate Verification Languages: Boogie and Sireum\/Pilar"],"prefix":"10.1007","author":[{"given":"Loren","family":"Segal","sequence":"first","affiliation":[]},{"given":"Patrice","family":"Chalin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-69149-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M. Barnett","year":"2008","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 144\u2013152. Springer, Heidelberg (2008)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","first-page":"243","volume-title":"Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005","year":"2005","unstructured":"de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.): Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, November 1-4. LNCS, vol.\u00a04111, pp. 243\u2013258. Springer, Heidelberg (2005)"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/s10817-009-9142-9","volume":"44","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Moska\u0142, M., Schulte, W., Wolff, B.: Hol-boogiean interactive prover-backend for the verifying c compiler. Journal of Automated Reasoning\u00a044, 111\u2013144 (2010), \n                  \n                    http:\/\/dx.doi.org\/10.1007\/s10817-009-9142-9","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-04167-9_14","volume-title":"Formal Methods for Components and Objects","author":"J. Chrz\u0105szcz","year":"2009","unstructured":"Chrz\u0105szcz, J., Huisman, M., Schubert, A.: BML and Related Tools. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol.\u00a05751, pp. 278\u2013297. Springer, Heidelberg (2009)"},{"key":"11_CR5","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby.: Expressing checkable properties of dynamic systems: The bandera specification language. International Journal on Software Tools for Technology Transfer (STFTT) (2002)"},{"issue":"8","key":"11_CR6","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E. Dijkstra","year":"1975","unstructured":"Dijkstra, E.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"11_CR8","unstructured":"Flanagan, D., Matsumoto, Y.: The Ruby Programming Language, 1st edn. O\u2019Reilly (2008)"},{"key":"11_CR9","unstructured":"Google Code: cofoja: Contracts for Java, \n                  \n                    http:\/\/code.google.com\/p\/cofoja\/"},{"key":"11_CR10","unstructured":"Grigore, R.: FreeBoogie, \n                  \n                    http:\/\/code.google.com\/p\/freeboogie"},{"key":"11_CR11","unstructured":"Grigore, R.: Efficiency of Extended Static Checkers. Tech. rep., PhD Research Plan. UCD Dublin (December 2007)"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Boston (1999)"},{"key":"11_CR13","unstructured":"Leino, K.R.M.: This is Boogie 2. Tech. Rep. KRML 178, Microsoft Research (June 2008)"},{"key":"11_CR14","unstructured":"Leino, K.: This is Boogie 2. Manuscript KRML 178 (2008)"},{"key":"11_CR15","unstructured":"Leino, K.: Verification tools at Microsoft (January 2009); Invited talk, Digiteo seminar"},{"key":"11_CR16","unstructured":"Robby: Sireum website, \n                  \n                    http:\/\/www.sireum.org"},{"key":"11_CR17","unstructured":"Robby: Sireum: A Software Analysis Platform. SAnToS, Kansas State Univerity (February 2007)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference Held Jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 267\u2013276 (2003)","DOI":"10.1145\/940071.940107"},{"key":"11_CR19","unstructured":"Segal, L.: Automatic program verification and test case generation of ruby programs. Tech. Rep. DSRG-TR-2011-02, Concordia University (2011)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Segal, L., Chalin, P.: A comparison of intermediate verification languages: Boogie and sireum\/pilar. Tech. Rep. DSRG-TR-2011-01, Concordia University (2011)","DOI":"10.1007\/978-3-642-27705-4_11"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T12:54:54Z","timestamp":1556196894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}