{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:01Z","timestamp":1772163961847,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,11,6]],"date-time":"2011-11-06T00:00:00Z","timestamp":1320537600000},"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":[[2011,11,6]]},"DOI":"10.1145\/2070337.2070357","type":"proceedings-article","created":{"date-parts":[[2011,11,21]],"date-time":"2011-11-21T14:55:03Z","timestamp":1321887303000},"page":"47-60","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Enhancing spark's contract checking facilities using symbolic execution"],"prefix":"10.1145","author":[{"given":"Jason","family":"Belt","sequence":"first","affiliation":[{"name":"Kansas State University, Manhattan, KS, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[{"name":"Kansas State University, Manhattan, KS, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Robby","sequence":"additional","affiliation":[{"name":"Kansas State University, Manhattan, KS, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrice","family":"Chalin","sequence":"additional","affiliation":[{"name":"Concordia University, Montreal, PQ, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Hardin","sequence":"additional","affiliation":[{"name":"Rockwell Collins Advanced Technology Center, Cedar Rapids, IA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xianghua","family":"Deng","sequence":"additional","affiliation":[{"name":"Google Inc., Mountain View, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,11,6]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_17"},{"key":"e_1_3_2_1_2_1","volume-title":"High Integrity Software -- the SPARK Approach to Safety and Security","author":"Barnes J.","year":"2003","unstructured":"J. Barnes . High Integrity Software -- the SPARK Approach to Safety and Security . Addison-Wesley , 2003 . J. Barnes. High Integrity Software -- the SPARK Approach to Safety and Security. Addison-Wesley, 2003."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770397"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986317"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595762"},{"key":"e_1_3_2_1_6_1","first-page":"209","volume-title":"8th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. R. Engler . Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs . In 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , pages 209 -- 224 . USENIX Association , 2008 . C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 209--224. USENIX Association, 2008."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.01.023"},{"key":"e_1_3_2_1_8_1","unstructured":"AdaCore\/SofCheck CodePeer tool set. http:\/\/www.adacore.com\/home\/products\/codepeer\/toolset\/.  AdaCore\/SofCheck CodePeer tool set. http:\/\/www.adacore.com\/home\/products\/codepeer\/toolset\/."},{"key":"e_1_3_2_1_9_1","unstructured":"The Coq proof assistant. http:\/\/coq.inria.fr\/.  The Coq proof assistant. http:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_13_1","volume-title":"August","author":"Dutertre B.","year":"2006","unstructured":"B. Dutertre and L. de Moura . The Yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf , August 2006 . B. Dutertre and L. de Moura. The Yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf, August 2006."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770379"},{"key":"e_1_3_2_1_15_1","unstructured":"Frama-C website. http:\/\/frama-c.com\/.  Frama-C website. http:\/\/frama-c.com\/."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_17_1","volume-title":"Workshop on Software Model Checking","author":"Grieskamp W.","year":"2005","unstructured":"W. Grieskamp , N. Tillmann , and W. Schulte . XRT--exploring runtime for .NET: Architecture and applications . Workshop on Software Model Checking , 2005 . W. Grieskamp, N. Tillmann, and W. Schulte. XRT--exploring runtime for .NET: Architecture and applications. Workshop on Software Model Checking, 2005."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/356674.356677"},{"key":"e_1_3_2_1_19_1","unstructured":"The AdaCore Hi-Lite project. http:\/\/www.open-do.org\/projects\/hi-lite\/.  The AdaCore Hi-Lite project. http:\/\/www.open-do.org\/projects\/hi-lite\/."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_2_1_21_1","volume-title":"Proving SPARK verification conditions with SMT solvers","author":"Jackson P.","year":"2009","unstructured":"P. Jackson and G. Passmore . Proving SPARK verification conditions with SMT solvers , 2009 . Draft journal article. http:\/\/homepages.inf.ed.ac.uk\/pbj\/papers\/vct-dec09-draft.pdf. P. Jackson and G. Passmore. Proving SPARK verification conditions with SMT solvers, 2009. Draft journal article. http:\/\/homepages.inf.ed.ac.uk\/pbj\/papers\/vct-dec09-draft.pdf."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_24_1","volume-title":"Decision Procedures -- An Algorithmic Point of View","author":"Kroening D.","year":"2008","unstructured":"D. Kroening and O. Strichman . Decision Procedures -- An Algorithmic Point of View . Springer , 2008 . D. Kroening and O. Strichman. Decision Procedures -- An Algorithmic Point of View. Springer, 2008."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_9"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the International Symposium on Secure Software Engineering","author":"Rossebo B.","year":"2006","unstructured":"B. Rossebo , P. Oman , J. Alves-Foss , R. Blue , and P. Jaszkowiak . Using SPARK-Ada to model and verify a MILS message router . In Proceedings of the International Symposium on Secure Software Engineering , 2006 . B. Rossebo, P. Oman, J. Alves-Foss, R. Blue, and P. Jaszkowiak. Using SPARK-Ada to model and verify a MILS message router. In Proceedings of the International Symposium on Secure Software Engineering, 2006."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/800216.806586"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792786.1792798"},{"key":"e_1_3_2_1_30_1","unstructured":"Victor website. http:\/\/homepages.inf.ed.ac.uk\/pbj\/spark\/victor.html.  Victor website. http:\/\/homepages.inf.ed.ac.uk\/pbj\/spark\/victor.html."}],"event":{"name":"SIGAda '11: ACM SIGAda Annual International Conference","location":"Denver Colorado USA","acronym":"SIGAda '11","sponsor":["SIGAda ACM Special Interest Group on Ada Programming Language","SIGAPP ACM Special Interest Group on Applied Computing","SIGPLAN ACM Special Interest Group on Programming Languages","Ada Europe Ada Europe","SIGBED ACM Special Interest Group on Embedded Systems","SIGCAS ACM Special Interest Group on Computers and Society","SIGCSE ACM Special Interest Group on Computer Science Education"]},"container-title":["Proceedings of the 2011 ACM annual international conference on Special interest group on the ada programming language"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2070337.2070357","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2070337.2070357","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:54:52Z","timestamp":1750226092000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2070337.2070357"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,6]]},"references-count":28,"alternative-id":["10.1145\/2070337.2070357","10.1145\/2070337"],"URL":"https:\/\/doi.org\/10.1145\/2070337.2070357","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2070336.2070357","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2011,11,6]]},"assertion":[{"value":"2011-11-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}