{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T23:13:28Z","timestamp":1776122008280,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T00:00:00Z","timestamp":1232409600000},"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":[[2009,1,20]]},"DOI":"10.1145\/1481848.1481860","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T14:41:38Z","timestamp":1232462498000},"page":"73-82","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Pragmatic equivalence and safety checking in Cryptol"],"prefix":"10.1145","author":[{"given":"Levent","family":"Erk\u00f6k","sequence":"first","affiliation":[{"name":"Galois, Inc., Portland, OR, USA"}]},{"given":"John","family":"Matthews","sequence":"additional","affiliation":[{"name":"Galois, Inc., Portland, OR, USA"}]}],"member":"320","published-online":{"date-parts":[[2009,1,20]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"CVC3 web site. cs.nyu.edu\/acsys\/cvc3","author":"Barrett Clark","year":"2008","unstructured":"Clark Barrett and Cesare Tinelli . CVC3 web site. cs.nyu.edu\/acsys\/cvc3 , 2008 . Clark Barrett and Cesare Tinelli. CVC3 web site. cs.nyu.edu\/acsys\/cvc3, 2008."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_36"},{"key":"e_1_3_2_1_4_1","volume-title":"The YICES SMT Solver. Available at: yices.csl.sri.com\/tool-paper.pdf","author":"Duterte Bruno","year":"2006","unstructured":"Bruno Duterte and Leonardo de Moura . The YICES SMT Solver. Available at: yices.csl.sri.com\/tool-paper.pdf , 2006 . Bruno Duterte and Leonardo de Moura. The YICES SMT Solver. Available at: yices.csl.sri.com\/tool-paper.pdf, 2006."},{"key":"e_1_3_2_1_5_1","volume-title":"December","author":"Dworkin Morris","year":"2001","unstructured":"Morris Dworkin . Recommendation for block cipher modes of operation: Methods and techniques , December 2001 . URL http:\/\/csrc.nist.gov\/publications\/nistpubs\/800-38a\/sp800-38a.pdf. NIST Special Publication 800-38A. Morris Dworkin. Recommendation for block cipher modes of operation: Methods and techniques, December 2001. URL http:\/\/csrc.nist.gov\/publications\/nistpubs\/800-38a\/sp800-38a.pdf. NIST Special Publication 800-38A."},{"key":"e_1_3_2_1_6_1","unstructured":"Niklas\n      E\u00e9n\n     and \n      Niklas\n      S\u00f6rensson\n    .\n  An extensible SAT-solver\n  . In Enrico Giunchiglia and Armando Tacchella editors SAT volume \n  2919\n   of \n  Lecture Notes in Computer Science pages \n  502\n  --\n  518\n  . \n  Springer 2003\n  . ISBN 3-540-20851-8.  Niklas E\u00e9n and Niklas S\u00f6rensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella editors SAT volume 2919 of Lecture Notes in Computer Science pages 502--518. Springer 2003. ISBN 3-540-20851-8."},{"key":"e_1_3_2_1_8_1","unstructured":"DPTAmit Goel Jim Grundy and Sava Krsti\u0107. DPT web site. http:\/\/sourceforge.net\/projects\/dpt 2008.  DPTAmit Goel Jim Grundy and Sava Krsti\u0107. DPT web site. http:\/\/sourceforge.net\/projects\/dpt 2008."},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD'08)","author":"Hagen George","year":"2008","unstructured":"George Hagen and Cesare Tinelli . Scaling up the formal verification of Lustre programs with SMT-based techniques. In A. Cimatti and R. Jones, editors , Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD'08) , Portland, Oregon, Lecture Notes in Computer Science. Springer , 2008 . URL ftp:\/\/ftp.cs.uiowa.edu\/pub\/tinelli\/papers\/HagTin-FMCAD-08.pdf. George Hagen and Cesare Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In A. Cimatti and R. Jones, editors, Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD'08), Portland, Oregon, Lecture Notes in Computer Science. Springer, 2008. URL ftp:\/\/ftp.cs.uiowa.edu\/pub\/tinelli\/papers\/HagTin-FMCAD-08.pdf."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/265082"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/551796"},{"key":"e_1_3_2_1_13_1","volume-title":"March","author":"Hurd Joe","year":"2007","unstructured":"Joe Hurd . Embedding Cryptol in higher order logic. Available from the author's website , March 2007 . URL http:\/\/www.gilith.com\/research\/papers. Joe Hurd. Embedding Cryptol in higher order logic. Available from the author's website, March 2007. URL http:\/\/www.gilith.com\/research\/papers."},{"key":"e_1_3_2_1_14_1","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"Kroening Daniel","year":"2008","unstructured":"Daniel Kroening and Ofer Strichman . Decision Procedures: An Algorithmic Point of View . Springer , 2008 . Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2008."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1950654.1950674"},{"key":"e_1_3_2_1_16_1","volume-title":"An embedding of Cryptol in HOL-4. Unpublished draft","author":"Li Guodong","year":"2005","unstructured":"Guodong Li and Konrad Slind . An embedding of Cryptol in HOL-4. Unpublished draft , 2005 . Guodong Li and Konrad Slind. An embedding of Cryptol in HOL-4. Unpublished draft, 2005."},{"key":"e_1_3_2_1_17_1","volume-title":"Available at: http:\/\/www.eecs.berkeley.edu\/ alanmi\/abc","author":"Mishchenko Alan","year":"2007","unstructured":"Alan Mishchenko . ABC: System for sequential synthesis and verification. Release 70930 , Available at: http:\/\/www.eecs.berkeley.edu\/ alanmi\/abc , 2007 . Alan Mishchenko. ABC: System for sequential synthesis and verification. Release 70930, Available at: http:\/\/www.eecs.berkeley.edu\/ alanmi\/abc, 2007."},{"key":"e_1_3_2_1_18_1","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS 2283","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS 2283 . Springer , 2002 . T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, 2002."},{"key":"e_1_3_2_1_19_1","unstructured":"NIST. Announcing the AES November 2001. URL http:\/\/csrc.nist.gov\/publications\/fips\/fips197\/fips-197.pdf. FIPS Publication 197.  NIST. Announcing the AES November 2001. URL http:\/\/csrc.nist.gov\/publications\/fips\/fips197\/fips-197.pdf. FIPS Publication 197."},{"key":"e_1_3_2_1_20_1","volume-title":"The jaig Equivalence Checker. Available from Objective Security Company","author":"Nordin Thomas","year":"2005","unstructured":"Thomas Nordin . The jaig Equivalence Checker. Available from Objective Security Company , 2005 . Thomas Nordin. The jaig Equivalence Checker. Available from Objective Security Company, 2005."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217975.1217977"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0028-5"},{"key":"e_1_3_2_1_24_1","volume-title":"Undecidable Theories","author":"Tarski A.","year":"1953","unstructured":"A. Tarski , A. Mostowski , and R. M. Robinson . Undecidable Theories . North-Holland Publishing Company , 1953 . A. Tarski, A. Mostowski, and R. M. Robinson. Undecidable Theories. North-Holland Publishing Company, 1953."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_21"},{"key":"e_1_3_2_1_26_1","article-title":"Efficiently checking propositional refutations in HOL theorem provers","author":"Weber Tjark","year":"2007","unstructured":"Tjark Weber and Hasan Amjad . Efficiently checking propositional refutations in HOL theorem provers . Journal of Applied Logic , July 2007 . URL http:\/\/dx.doi.org\/10.1016\/j.jal.2007.07.003. 10.1016\/j.jal.2007.07.003 Tjark Weber and Hasan Amjad. Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic, July 2007. URL http:\/\/dx.doi.org\/10.1016\/j.jal.2007.07.003.","journal-title":"Journal of Applied Logic"}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Savannah GA USA","acronym":"POPL09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 3rd workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481860","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1481848.1481860","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:10Z","timestamp":1750253410000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481860"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,20]]},"references-count":25,"alternative-id":["10.1145\/1481848.1481860","10.1145\/1481848"],"URL":"https:\/\/doi.org\/10.1145\/1481848.1481860","relation":{},"subject":[],"published":{"date-parts":[[2009,1,20]]},"assertion":[{"value":"2009-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}