{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:00Z","timestamp":1773655620915,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T00:00:00Z","timestamp":1327449600000},"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,25]]},"DOI":"10.1145\/2103656.2103719","type":"proceedings-article","created":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T11:47:19Z","timestamp":1327405639000},"page":"533-544","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":148,"title":["An executable formal semantics of C with applications"],"prefix":"10.1145","author":[{"given":"Chucky","family":"Ellison","sequence":"first","affiliation":[{"name":"University of Illinois, Urbana, IL, USA"}]},{"given":"Grigore","family":"Rosu","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana, IL, USA"}]}],"member":"320","published-online":{"date-parts":[[2012,1,25]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_2_2_1","volume-title":"A Computational Logic Handbook","author":"Boyer R. S.","year":"1998","unstructured":"R. S. Boyer and J. S. Moore . A Computational Logic Handbook . Academic Press , second edition, 1998 . R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, second edition, 1998."},{"key":"e_1_3_2_2_3_1","series-title":"LNCS","volume-title":"A High-Performance Logical Framework","author":"Clavel M.","year":"2007","unstructured":"M. Clavel , F. Dur\u00e1n , S. Eker , J. Meseguer , P. Lincoln , N. Mart\u0131-Oliet , and C. Talcott . All About Maude , A High-Performance Logical Framework , volume 4350 of LNCS . Springer , 2007 . M. Clavel, F. Dur\u00e1n, S. Eker, J. Meseguer, P. Lincoln, N. Mart\u0131-Oliet, and C. Talcott. All About Maude, A High-Performance Logical Framework, volume 4350 of LNCS. Springer, 2007."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1631687.1596591"},{"key":"e_1_3_2_2_7_1","volume-title":"On Duff's device","author":"Duff T.","year":"1988","unstructured":"T. Duff . On Duff's device , 1988 . URL http:\/\/www.lysator.liu.se\/c\/duffs-device.html. Msg. to the comp.lang.c Usenet group. T. Duff. On Duff's device, 1988. URL http:\/\/www.lysator.liu.se\/c\/duffs-device.html. Msg. to the comp.lang.c Usenet group."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03429-9_10"},{"key":"e_1_3_2_2_9_1","volume-title":"GNU compiler collection","author":"F.","year":"2010","unstructured":"F. GNU compiler collection , 2010 . URL http:\/\/gcc.gnu.org. F. GNU compiler collection, 2010. URL http:\/\/gcc.gnu.org."},{"key":"e_1_3_2_2_10_1","volume-title":"C language testsuites: \"C-torture\" version 4.4.2","author":"F.","year":"2010","unstructured":"F. C language testsuites: \"C-torture\" version 4.4.2 , 2010 . URL http:\/\/gcc.gnu.org\/onlinedocs\/gccint\/C-Tests.html. F. C language testsuites: \"C-torture\" version 4.4.2, 2010. URL http:\/\/gcc.gnu.org\/onlinedocs\/gccint\/C-Tests.html."},{"key":"e_1_3_2_2_11_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/3-540-56992-8_17","volume-title":"Computer Science Logic","author":"Gurevich Y.","year":"1993","unstructured":"Y. Gurevich and J. K. Huggins . The semantics of the C programming language . In Computer Science Logic , volume 702 of LNCS , pages 274 -- 308 , 1993 . Y. Gurevich and J. K. Huggins. The semantics of the C programming language. In Computer Science Logic, volume 702 of LNCS, pages 274--308, 1993."},{"key":"e_1_3_2_2_12_1","volume-title":"A Retargetable C Compiler: Design and Implementation","author":"Hanson D. R.","year":"1995","unstructured":"D. R. Hanson and C. W. Fraser . A Retargetable C Compiler: Design and Implementation . Addison-Wesley , 1995 . D. R. Hanson and C. W. Fraser. A Retargetable C Compiler: Design and Implementation. Addison-Wesley, 1995."},{"key":"e_1_3_2_2_16_1","volume-title":"Self-published","author":"Jones D. M.","year":"2008","unstructured":"D. M. Jones . The New C Standard : An Economic and Cultural Commentary . Self-published , December 2008 . URL http:\/\/www.knosof.co.uk\/cbook\/cbook.html. D. M. Jones. The New C Standard: An Economic and Cultural Commentary. Self-published, December 2008. URL http:\/\/www.knosof.co.uk\/cbook\/cbook.html."},{"key":"e_1_3_2_2_17_1","volume-title":"The C Programming Language","author":"Kernighan B. W.","year":"1988","unstructured":"B. W. Kernighan and D. M. Ritchie . The C Programming Language . Prentice Hall , second edition, 1988 . B. W. Kernighan and D. M. Ritchie. The C Programming Language. Prentice Hall, second edition, 1988."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647478.727796"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328465"},{"key":"e_1_3_2_2_21_1","volume-title":"The international obfuscated C code contest","author":"Noll L. C.","year":"2010","unstructured":"L. C. Noll , S. Cooper , P. Seebach , and L. A. Broukhis . The international obfuscated C code contest , 2010 . URL http:\/\/www.ioccc.org\/. L. C. Noll, S. Cooper, P. Seebach, and L. A. Broukhis. The international obfuscated C code contest, 2010. URL http:\/\/www.ioccc.org\/."},{"key":"e_1_3_2_2_23_1","volume-title":"NICTA","author":"Norrish M.","year":"2008","unstructured":"M. Norrish . A formal semantics for CC. Technical report , NICTA , 2008 . URL http:\/\/nicta.com.au\/people\/norrishm\/attachments\/bibliographies_and_papers\/C-TR.pdf. M. Norrish. A formal semantics for CC. Technical report, NICTA, 2008. URL http:\/\/nicta.com.au\/people\/norrishm\/attachments\/bibliographies_and_papers\/C-TR.pdf."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0920-5489(01)00059-9"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000366X"},{"key":"e_1_3_2_2_27_1","first-page":"60","article-title":"The origins of structural operational semantics","volume":"60","author":"Plotkin G. D.","year":"2004","unstructured":"G. D. Plotkin . The origins of structural operational semantics . Journal Of Logic and Algebraic Programming , 60 : 60 -- 61 , 2004 . G. D. Plotkin. The origins of structural operational semantics. Journal Of Logic and Algebraic Programming, 60: 60--61, 2004.","journal-title":"Journal Of Logic and Algebraic Programming"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985928"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04694-0_10"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-642-17796-5_9","volume-title":"13th International Conference on Algebraic Methodology and Software Technology (AMAST'10)","volume":"6486","author":"Rosu G.","year":"2010","unstructured":"G. Rosu , C. Ellison , and W. Schulte . Matching logic: An alternative to Hoare\/Floyd logic . In 13th International Conference on Algebraic Methodology and Software Technology (AMAST'10) , volume 6486 of LNCS, pages 142 -- 162 , 2010 . G. Rosu, C. Ellison, and W. Schulte. Matching logic: An alternative to Hoare\/Floyd logic. In 13th International Conference on Algebraic Methodology and Software Technology (AMAST'10), volume 6486 of LNCS, pages 142--162, 2010."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1927806.1927818"},{"key":"e_1_3_2_2_33_1","volume-title":"ACM SIGSOFT Workshop on Formal Methods in Software Practice","author":"Subramanian S.","year":"1996","unstructured":"S. Subramanian and J. V. Cook . Mechanical verification of C programs . In ACM SIGSOFT Workshop on Formal Methods in Software Practice , January 1996 . S. Subramanian and J. V. Cook. Mechanical verification of C programs. In ACM SIGSOFT Workshop on Formal Methods in Software Practice, January 1996."},{"key":"e_1_3_2_2_34_1","volume-title":"Frequently asked questions","author":"Summit S.","year":"2005","unstructured":"S. Summit . C programming FA Qs : Frequently asked questions , 2005 . URL http:\/\/www.c-faq.com\/. S. Summit. C programming FAQs: Frequently asked questions, 2005. URL http:\/\/www.c-faq.com\/."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_2_36_1","series-title":"LNCS","first-page":"391","volume-title":"Abstract State Machines","author":"Zimmermann W.","year":"2003","unstructured":"W. Zimmermann and A. Dold . A framework for modeling the semantics of expression evaluation with abstract state machines . In Abstract State Machines , volume 2589 of LNCS , pages 391 -- 406 , 2003 . W. Zimmermann and A. Dold. A framework for modeling the semantics of expression evaluation with abstract state machines. In Abstract State Machines, volume 2589 of LNCS, pages 391--406, 2003."}],"event":{"name":"POPL '12: The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Philadelphia PA USA","acronym":"POPL '12","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103656.2103719","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2103656.2103719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:06:22Z","timestamp":1750226782000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103656.2103719"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,25]]},"references-count":29,"alternative-id":["10.1145\/2103656.2103719","10.1145\/2103656"],"URL":"https:\/\/doi.org\/10.1145\/2103656.2103719","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2103621.2103719","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2012,1,25]]},"assertion":[{"value":"2012-01-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}