{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T05:48:05Z","timestamp":1768024085287,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642253782","type":"print"},{"value":"9783642253799","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-25379-9_22","type":"book-chapter","created":{"date-parts":[[2011,11,13]],"date-time":"2011-11-13T20:33:47Z","timestamp":1321216427000},"page":"296-313","source":"Crossref","is-referenced-by-count":5,"title":["Automatically Verifying Typing Constraints for a Data Processing Language"],"prefix":"10.1007","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[]},{"given":"Thorsten","family":"Tarrach","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Bytecode level specification language and program logic. Mobius Project, Deliverable D3.1 (2006)"},{"key":"22_CR2","unstructured":"The Microsoft code name \u201dM\u201d modeling language specification (October 2009), \n                    \n                      http:\/\/msdn.microsoft.com\/en-us\/library\/dd548667.aspx"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"22_CR5","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filli\u00e2tre, J., Gim\u00e9nez, E., Herbelin, H., et al.: The Coq proof assistant reference manual, version 8.2. INRIA (2009)"},{"issue":"2","key":"22_CR6","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/1890028.1890031","volume":"33","author":"J. Bengtson","year":"2011","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems\u00a033(2), 8 (2011)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Bierman, G.M., Gordon, A.D., Hri\u0163cu, C., Langworthy, D.: Semantic subtyping with an SMT solver. In: 15th ACM SIGPLAN International Conference on Functional programming (ICFP 2010), pp. 105\u2013116. ACM Press (2010)","DOI":"10.1145\/1863543.1863560"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-71067-7_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S. B\u00f6hme","year":"2008","unstructured":"B\u00f6hme, S., Leino, K.R.M., Wolff, B.: HOL-Boogie \u2014 An Interactive Prover for the Boogie Program-Verifier. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 150\u2013166. Springer, Heidelberg (2008)"},{"key":"22_CR9","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.entcs.2009.09.061","volume":"254","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. Electronic Notes in Theoretical Computer Science\u00a0254, 85\u2013103 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-based modular verification of concurrent C. In: 31st International Conference on Software Engineering (ICSE), pp. 429\u2013430. IEEE (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"22_CR11","unstructured":"DeLine, R., Leino, K.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)"},{"issue":"3","key":"22_CR12","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.: Simplify: A theorem prover for program checking. Journal of the ACM (JACM)\u00a052(3), 473 (2005)","journal-title":"Journal of the ACM (JACM)"},{"key":"22_CR13","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)"},{"issue":"2","key":"22_CR14","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/767193.767195","volume":"3","author":"H. Hosoya","year":"2003","unstructured":"Hosoya, H., Pierce, B.: XDuce: A statically typed XML processing language. ACM Transactions on Internet Technology\u00a03(2), 117\u2013148 (2003)","journal-title":"ACM Transactions on Internet Technology"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-22110-1_38","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2011","unstructured":"Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: Verifying Functional Programs Using Abstract Interpreters. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 470\u2013485. Springer, Heidelberg (2011)"},{"issue":"5","key":"22_CR16","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T. Kleymann","year":"1999","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects of Computing\u00a011(5), 541\u2013566 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"22_CR17","unstructured":"Knowles, K., Tomb, A., Gronski, J., Freund, S., Flanagan, C.: Sage: Unified hybrid checking for first-class types, general refinement types and Dynamic. Technical report, UCSC (2007)"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, C.-H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: 24th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 179\u2013188. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.29"},{"issue":"1","key":"22_CR19","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2007.02.059","volume":"190","author":"H. Lehner","year":"2007","unstructured":"Lehner, H., M\u00fcller, P.: Formal translation of bytecode into BoogiePL. Electronic Notes in Theoretical Computer Science\u00a0190(1), 35\u201350 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"22_CR20","unstructured":"Leino, K.R.M.: This is Boogie 2. TechReport (2008)"},{"issue":"1-3","key":"22_CR21","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.scico.2004.05.016","volume":"55","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M., Millstein, T., Saxe, J.: Generating error traces from verification-condition counterexamples. Science of Computer Programming\u00a055(1-3), 209\u2013226 (2005)","journal-title":"Science of Computer Programming"},{"key":"22_CR22","unstructured":"Marinos, C.: An introduction to functional programming for.NET developers. MSDN Magazine (April 2010)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Meijer, E., Beckman, B., Bierman, G.M.: LINQ: reconciling object, relations and XML in the .NET framework. In: ACM SIGMOD International Conference on Management of Data (SIGMOD), page 706. ACM (2006)","DOI":"10.1145\/1142473.1142552"},{"key":"22_CR24","unstructured":"Morris, J.: Comments on \u201dprocedures and parameters\u201d. Undated and unpublished"},{"issue":"5","key":"22_CR25","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/1387673.1387678","volume":"30","author":"M. Naik","year":"2008","unstructured":"Naik, M., Palsberg, J.: A type system equivalent to a model checker. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a030(5), 29 (2008)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Proof and System-Reliability, pp. 341\u2013367. Kluwer (2002)","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"22_CR27","unstructured":"Pierce, B., Casinghino, C., Greenberg, M., Sj\u00f6berg, V., Yorgey, B.: Software Foundations (2010), \n                    \n                      http:\/\/www.cis.upenn.edu\/~bcpierce\/sf\/"},{"key":"22_CR28","unstructured":"Ranise, S., Tinelli, C.: The satisfiability modulo theories library, SMT-LIB (2006), \n                    \n                      http:\/\/www.SMT-LIB.org"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI), pp. 159\u2013169 (2008)","DOI":"10.1145\/1375581.1375602"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-642-11957-6_28","volume-title":"Programming Languages and Systems","author":"N. Swamy","year":"2010","unstructured":"Swamy, N., Chen, J., Chugh, R.: Enforcing Stateful Authorization and Information Flow Policies in Fine. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 529\u2013549. Springer, Heidelberg (2010)"},{"key":"22_CR31","unstructured":"Tarrach, T.: Automatically verifying \u201cM\u201d modeling language constraints. Master\u2019s thesis, Saarland University (2010)"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25379-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T06:20:19Z","timestamp":1555482019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25379-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253782","9783642253799"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25379-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}