{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T18:10:13Z","timestamp":1778263813291,"version":"3.51.4"},"publisher-location":"Boston, MA","reference-count":14,"publisher":"Springer US","isbn-type":[{"value":"9781441959058","type":"print"},{"value":"9781441959065","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","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-1-4419-5906-5_863","type":"book-chapter","created":{"date-parts":[[2011,10,27]],"date-time":"2011-10-27T09:53:14Z","timestamp":1319709194000},"page":"981-983","source":"Crossref","is-referenced-by-count":1,"title":["Program Verification and Security"],"prefix":"10.1007","author":[{"given":"Catherine","family":"Meadows","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"863_CR1_863","volume-title":"The B-Book: assigning programs to meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial JR (1996) The B-Book: assigning programs to meanings. Cambridge University Press, Cambridge"},{"issue":"10","key":"863_CR2_863","first-page":"576","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580,\u00a0583","journal-title":"Commun ACM"},{"key":"863_CR3_863","first-page":"19","volume-title":"Assigning meanings to programs","author":"RW Floyd","year":"1967","unstructured":"Floyd RW (1967) Assigning meanings to programs. In: Proceedings of the American Mathematical Society symposia on applied mathematics, New York, vol 19, pp\u00a019\u201331"},{"key":"863_CR4_863","volume-title":"Good. Revised report on Gypsy 2.1\u00a0\u2013 DRAFT, July 1984","author":"I Donald","year":"1984","unstructured":"Donald I (1984) Good. Revised report on Gypsy 2.1\u00a0\u2013 DRAFT, July 1984. Institute for Computing Science, The University of Texas at Austin, Austin"},{"key":"863_CR5_863","volume-title":"Eiffel: the language","author":"B Meyer","year":"1992","unstructured":"Meyer B (1992) Eiffel: the language. Prentice Hall,\u00a0NJ"},{"key":"863_CR6_863","volume-title":"High integrity software: the SPARK approach to safety and security","author":"J Barnes","year":"2003","unstructured":"Barnes J (2003) High integrity software: the SPARK approach to safety and security. Addison-Wesley, Boston"},{"key":"863_CR7_863","volume-title":"The Spec# programming system: an overview","author":"M Barnett","year":"2004","unstructured":"Barnett M, Leino KRM, Schulte W (2004) The Spec# programming system: an overview. In: Proceedings of construction and analysis of safe, secure and interoperable smart devices (CASSIS), Marseilles. LNCS, vol 3362, Springer, New\u00a0York"},{"key":"863_CR8_863","volume-title":"VCC: a practical system for verifying concurrent C","author":"E Cohen","year":"2009","unstructured":"Cohen E, Dahlweid M, Hillebrand M, Leinenbach D, Moskal M, Santen T, Schulte W, Tobies S (2009) VCC: a practical system for verifying concurrent C. In: 22nd International conference on theorem proving in higher order logics (TPHOLs 2009), Munich Germany, LNCS, vol 5674, Springer, Berlin"},{"issue":"7","key":"863_CR9_863","first-page":"504","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning DE, Denning PJ (1977) Certification of programs for secure information flow. Commun ACM 20(7):504\u2013513","journal-title":"Commun ACM"},{"issue":"1","key":"863_CR10_863","first-page":"5","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld A, Myers A (2003) Language-based information flow security. IEEE J Sel Areas Commun 21(1):5\u201319","journal-title":"IEEE J Sel Areas Commun"},{"key":"863_CR11_863","volume-title":"BitBlaze: a new approach to computer security via binary analysis","author":"D Song","year":"2008","unstructured":"Song D, Brumley D, Yin H, Caballero J, Jager I, Kang MG, Liang Z, Newsome J, Poosankam P, Saxena P (2008) BitBlaze: a new approach to computer security via binary analysis. In: Proceedings of ICISS 2008. LNCS, vol 5352, Springer, Berlin"},{"key":"863_CR12_863","unstructured":"Smith M, Siebert A, DiVitto B, Good D (1981) A verified encrypted packet interface. SIGSOFT\u00a06(3)"},{"key":"863_CR13_863","first-page":"85","volume-title":"Formal proof of smart card applets correctness","author":"JL Lanet","year":"1998","unstructured":"Lanet JL, Requet A (1998) Formal proof of smart card applets correctness. In: Proceedings of the third smart card research and advanced application conference (CARDIS\u201998), Louvain-la-Neuve, LNCS, vol 1820, Springer, Berlin, pp\u00a085\u201397"},{"key":"863_CR14_863","volume-title":"SPARK\u00a0\u2013 A state-of-the-practice approach to the common criteria implementation requirements","author":"R Chapman","year":"2001","unstructured":"Chapman R (2001) SPARK\u00a0\u2013 A state-of-the-practice approach to the common criteria implementation requirements. In: 2nd International common criteria conference, Brighton,\u00a0UK"}],"container-title":["Encyclopedia of Cryptography and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-5906-5_863","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T17:27:20Z","timestamp":1778261240000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-5906-5_863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9781441959058","9781441959065"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-5906-5_863","relation":{},"subject":[],"published":{"date-parts":[[2011]]}}}