{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:29Z","timestamp":1772164049335,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,12,2]],"date-time":"2012-12-02T00:00:00Z","timestamp":1354406400000},"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,12,2]]},"DOI":"10.1145\/2402676.2402697","type":"proceedings-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T12:08:34Z","timestamp":1354190914000},"page":"53-62","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A DSL for cross-domain security"],"prefix":"10.1145","author":[{"given":"David S.","family":"Hardin","sequence":"first","affiliation":[{"name":"Rockwell Collins, Cedar Rapids, IA, USA"}]},{"given":"Konrad L.","family":"Slind","sequence":"additional","affiliation":[{"name":"Rockwell Collins, Bloomington, MN, USA"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, USA"}]},{"given":"Tuang-Hung","family":"Pham","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, USA"}]}],"member":"320","published-online":{"date-parts":[[2012,12,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_2_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories","author":"Barrett C.","year":"2010","unstructured":"C. Barrett , A. Stump , and C. Tinelli . The SMT-LIB standard: Version 2.0. In A. Gupta and D. Kroening, editors , Proceedings of the 8th International Workshop on Satisfiability Modulo Theories ( Edinburgh, England) , 2010 . C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB standard: Version 2.0. In A. Gupta and D. Kroening, editors, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England), 2010."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_15"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869542.1869625"},{"key":"e_1_3_2_1_7_1","volume-title":"Universite Paris","author":"Filliatre J.-C.","year":"2011","unstructured":"J.-C. Filliatre . Deductive Program Verification. Th\u00e0se d'habilitation , Universite Paris 11, Dec. 2011 . J.-C. Filliatre. Deductive Program Verification. Th\u00e0se d'habilitation, Universite Paris 11, Dec. 2011."},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","first-page":"175","volume-title":"Proceedings of CAV","author":"Ganzinger H.","year":"2004","unstructured":"H. Ganzinger , G. Hagen , R. Nieuwenhuis , A. Oliveras , and C. Tinelli . DPLL(T): Fast decision procedures . In Proceedings of CAV , volume 3114 of LNCS , pages 175 -- 188 . Springer , 2004 . H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In Proceedings of CAV, volume 3114 of LNCS, pages 175--188. Springer, 2004."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1637837.1637856"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2028067.2028068"},{"key":"e_1_3_2_1_12_1","unstructured":"R. C. Inc. Turnstile High Assurance Guard Homepage. http:\/\/www.rockwellcollins.com\/.  R. C. Inc. Turnstile High Assurance Guard Homepage. http:\/\/www.rockwellcollins.com\/."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572286"},{"key":"e_1_3_2_1_14_1","volume-title":"TU Munich","author":"Krauss A.","year":"2009","unstructured":"A. Krauss . Automating recursive definitions and termination proofs in higher order logic. PhD thesis , TU Munich , 2009 . A. Krauss. Automating recursive definitions and termination proofs in higher order logic. PhD thesis, TU Munich, 2009."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_2_1_17_1","series-title":"LNCS","volume-title":"Proceedings of FPCA","author":"Meijer E.","year":"1991","unstructured":"E. Meijer , M. Fokkinga , and R. Paterson . Functional programming with bananas, lenses, envelopes, and barbed wire . In Proceedings of FPCA , volume 523 of LNCS , 1991 . E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes, and barbed wire. In Proceedings of FPCA, volume 523 of LNCS, 1991."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"Milner R.","year":"1997","unstructured":"R. Milner , M. Tofte , R. Harper , and D. MacQueen . The Definition of Standard ML (Revised) . The MIT Press , 1997 . R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803003010"},{"key":"e_1_3_2_1_23_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1007\/3-540-61580-6_22","volume-title":"Dagstuhl Seminar on Partial Evaluation","author":"Sestoft P.","year":"1996","unstructured":"P. Sestoft . ML pattern match compilation and partial evaluation . In Dagstuhl Seminar on Partial Evaluation , volume 1110 of LNCS , pages 446 -- 464 , 1996 . P. Sestoft. ML pattern match compilation and partial evaluation. In Dagstuhl Seminar on Partial Evaluation, volume 1110 of LNCS, pages 446--464, 1996."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_3_2_1_26_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-642-23702-7_23","volume-title":"Proceedings of Static Analysis","author":"Suter P.","year":"2011","unstructured":"P. Suter , A. K\u00f6ksal , and V. Kuncak . Satisfiability modulo recursive programs . In E. Yahav, editor, Proceedings of Static Analysis , volume 6887 of LNCS , pages 298 -- 315 . Springer , 2011 . P. Suter, A. K\u00f6ksal, and V. Kuncak. Satisfiability modulo recursive programs. In E. Yahav, editor, Proceedings of Static Analysis, volume 6887 of LNCS, pages 298--315. Springer, 2011."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1539-9_13"}],"event":{"name":"HILT'12: ACM SIGAda Annual","location":"Boston Massachusetts USA","acronym":"HILT'12","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","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 2012 ACM conference on High integrity language technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2402676.2402697","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2402676.2402697","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:12Z","timestamp":1750225692000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2402676.2402697"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12,2]]},"references-count":25,"alternative-id":["10.1145\/2402676.2402697","10.1145\/2402676"],"URL":"https:\/\/doi.org\/10.1145\/2402676.2402697","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2402709.2402697","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2012,12,2]]},"assertion":[{"value":"2012-12-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}