{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:49:17Z","timestamp":1790927357323,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,8,18]],"date-time":"2013-08-18T00:00:00Z","timestamp":1376784000000},"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":[[2013,8,18]]},"DOI":"10.1145\/2491411.2491452","type":"proceedings-article","created":{"date-parts":[[2013,8,20]],"date-time":"2013-08-20T14:07:21Z","timestamp":1377007641000},"page":"345-355","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":91,"title":["Differential assertion checking"],"prefix":"10.1145","author":[{"given":"Shuvendu K.","family":"Lahiri","sequence":"first","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rahul","family":"Sharma","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chris","family":"Hawblitzel","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108813"},{"key":"e_1_3_2_1_4_1","first-page":"214","volume-title":"Formal Methods (FM\u201911), LNCS 6664","author":"Barthe G.","year":"2011","unstructured":"G. Barthe , J. M. Crespo , and C. Kunz . Relational verification using product programs . In Formal Methods (FM\u201911), LNCS 6664 , pages 200\u2013 214 , 2011 . G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using product programs. In Formal Methods (FM\u201911), LNCS 6664, pages 200\u2013214, 2011."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254086"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426901"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480921"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_9_1","first-page":"340","volume-title":"TACAS \u201908","author":"de Moura L.","year":"2008","unstructured":"L. de Moura and N. Bj\u00f8rner . Z3: An e\ufb03cient SMT solver . In TACAS \u201908 , pages 337\u2013 340 , 2008 . L. de Moura and N. Bj\u00f8rner. Z3: An e\ufb03cient SMT solver. In TACAS \u201908, pages 337\u2013340, 2008."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-005-3861-2"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630034"},{"key":"e_1_3_2_1_13_1","first-page":"83","volume-title":"Computer-Aided Verification (CAV \u201997), LNCS 1254","author":"Graf S.","year":"1997","unstructured":"S. Graf and H. Sa\u00a8\u0131di . Construction of abstract state graphs with PVS . In Computer-Aided Verification (CAV \u201997), LNCS 1254 , pages 72\u2013 83 , June 1997 . S. Graf and H. Sa\u00a8\u0131di. Construction of abstract state graphs with PVS. In Computer-Aided Verification (CAV \u201997), LNCS 1254, pages 72\u201383, June 1997."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806812"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134319"},{"key":"e_1_3_2_1_16_1","first-page":"299","volume-title":"Conference on Automated Deduction (CADE\u201913)","author":"Hawblitzel C.","year":"2013","unstructured":"C. Hawblitzel , M. Kawaguchi , S. K. Lahiri , and H. Reb\u02c6 elo. Towards modularly comparing programs using automated theorem provers . In Conference on Automated Deduction (CADE\u201913) , LNCS 7898, pages 282\u2013 299 , 2013 . C. Hawblitzel, M. Kawaguchi, S. K. Lahiri, and H. Reb\u02c6 elo. Towards modularly comparing programs using automated theorem provers. In Conference on Automated Deduction (CADE\u201913), LNCS 7898, pages 282\u2013299, 2013."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103662"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882362.1882405"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/586094.586095"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_3_2_1_26_1","first-page":"166","volume-title":"Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201998)","author":"Pnueli A.","year":"1998","unstructured":"A. Pnueli , M. Siegel , and E. Singerman . Translation validation . In Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201998) , pages 151\u2013 166 , 1998 . A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201998), pages 151\u2013166, 1998."},{"key":"e_1_3_2_1_27_1","unstructured":"Software-artifact Infrastructure Repository. Available at http:\/\/sir.unl.edu\/portal\/index.html.  Software-artifact Infrastructure Repository. Available at http:\/\/sir.unl.edu\/portal\/index.html."},{"key":"e_1_3_2_1_28_1","first-page":"363","volume-title":"Computer Aided Verification (CAV\u201994), LNCS 818","author":"Sokolsky O.","year":"1994","unstructured":"O. Sokolsky and S. A. Smolka . Incremental model checking in the modal mu-calculus . In Computer Aided Verification (CAV\u201994), LNCS 818 , pages 351\u2013 363 , 1994 . O. Sokolsky and S. A. Smolka. Incremental model checking in the modal mu-calculus. In Computer Aided Verification (CAV\u201994), LNCS 818, pages 351\u2013363, 1994."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_1_30_1","unstructured":"The Boogie Verifier. Available at http:\/\/boogie.codeplex.com.  The Boogie Verifier. Available at http:\/\/boogie.codeplex.com."},{"key":"e_1_3_2_1_31_1","unstructured":"Verisec Suite. Available at http:\/\/se.cs.toronto.edu\/index.php\/Verisec_Suite.  Verisec Suite. Available at http:\/\/se.cs.toronto.edu\/index.php\/Verisec_Suite."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-3402-z"}],"event":{"name":"ESEC\/FSE'13: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","location":"Saint Petersburg Russia","acronym":"ESEC\/FSE'13","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491411.2491452","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491411.2491452","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:41Z","timestamp":1750231721000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491411.2491452"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8,18]]},"references-count":33,"alternative-id":["10.1145\/2491411.2491452","10.1145\/2491411"],"URL":"https:\/\/doi.org\/10.1145\/2491411.2491452","relation":{},"subject":[],"published":{"date-parts":[[2013,8,18]]},"assertion":[{"value":"2013-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}