{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T00:50:12Z","timestamp":1725670212404},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642287558"},{"type":"electronic","value":"9783642287565"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_3","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:57:15Z","timestamp":1332449835000},"page":"18-32","source":"Crossref","is-referenced-by-count":7,"title":["The Guardol Language and Verification System"],"prefix":"10.1007","author":[{"given":"David","family":"Hardin","sequence":"first","affiliation":[]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Whalen","sequence":"additional","affiliation":[]},{"given":"Tuan-Hung","family":"Pham","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-25379-9_15","volume-title":"Certified Programs and Proofs","author":"S. B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3\u2019s Bit-Vector Proofs in HOL4 and Isabelle\/HOL. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 183\u2013198. Springer, Heidelberg (2011)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 150\u2013153. Springer, Heidelberg (2010)"},{"key":"3_CR3","unstructured":"Filli\u00e2tre, J.-C.: Deductive Program Verification. Th\u00e8se d\u2019habilitation, Universit\u00e9 Paris (December 11, 2011)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: Proc. of IEEE Symposium on Security and Privacy, pp. 11\u201320. IEEE Computer Society Press (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Greve, D.: Assuming termination. In: Proceedings of ACL2 Workshop, ACL2 2009, pp. 114\u2013122. ACM (2009)","DOI":"10.1145\/1637837.1637856"},{"key":"3_CR7","unstructured":"Rockwell\u00a0Collins Inc. Turnstile High Assurance Guard Homepage, http:\/\/www.rockwellcollins.com\/sitecore\/content\/Data\/Products\/Information_Assurance\/Cross_Domain_Solutions\/Turnstile_High_Assurance_Guard.aspx"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Kiezun, A., Ganesh, V., Guo, P., Hooimeijer, P., Ernst, M.: HAMPI: A solver for string constraints. In: Proceedings of ISSTA (2009)","DOI":"10.1145\/1572272.1572286"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Krauss, A.: Automating recursive definitions and termination proofs in higher order logic. PhD thesis, TU Munich (2009)","DOI":"10.1007\/s10817-009-9157-2"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-27940-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.R.M. Leino","year":"2012","unstructured":"Leino, K.R.M.: Automating Induction with an SMT Solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 315\u2013331. Springer, Heidelberg (2012)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/3540543961_7","volume-title":"Functional Programming Languages and Computer Architecture","author":"E. Meijer","year":"1991","unstructured":"Meijer, E., Fokkinga, M., Paterson, R.: Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol.\u00a0523, pp. 124\u2013144. Springer, Heidelberg (1991)"},{"key":"3_CR13","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"S. Miller","year":"2010","unstructured":"Miller, S., Whalen, M., Cofer, D.: Software model checking takes off. CACM\u00a053, 58\u201364 (2010)","journal-title":"CACM"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press (1997)","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"3_CR15","unstructured":"Myreen, M.: Formal verification of machine-code programs. PhD thesis, University of Cambridge (2009)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Peyton Jones, S., et al.: The Haskell 98 language and libraries: The revised report. Journal of Functional Programming\u00a013(1), 0\u2013255 (2003)","DOI":"10.1017\/S0956796803003010"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of sequential imperative programs in Isabelle\/HOL. PhD thesis, TU Munich (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/3-540-61580-6_22","volume-title":"Partial Evaluation","author":"P. Sestoft","year":"1996","unstructured":"Sestoft, P.: ML Pattern Match Compilation and Partial Evaluation. In: Danvy, O., Thiemann, P., Gl\u00fcck, R. (eds.) Dagstuhl Seminar 1996. LNCS, vol.\u00a01110, pp. 446\u2013464. Springer, Heidelberg (1996)"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A Brief Overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: Proceedings of POPL, pp. 199\u2013210. ACM (2010)","DOI":"10.1145\/1707801.1706325"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability Modulo Recursive Programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 298\u2013315. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Whalen, M., Greve, D., Wagner, L.: Model checking information flow. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer (2010)","DOI":"10.1007\/978-1-4419-1539-9_13"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T02:11:04Z","timestamp":1641435064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}