{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:12Z","timestamp":1775873412637,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":58,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T00:00:00Z","timestamp":1572134400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CSR-1814507"],"award-info":[{"award-number":["CSR-1814507"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,10,27]]},"DOI":"10.1145\/3341301.3359651","type":"proceedings-article","created":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T13:34:22Z","timestamp":1571664862000},"page":"370-384","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["I4"],"prefix":"10.1145","author":[{"given":"Haojun","family":"Ma","sequence":"first","affiliation":[{"name":"University of Michigan"}]},{"given":"Aman","family":"Goel","sequence":"additional","affiliation":[{"name":"University of Michigan"}]},{"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[{"name":"University of Michigan"}]},{"given":"Manos","family":"Kapritsos","sequence":"additional","affiliation":[{"name":"University of Michigan"}]},{"given":"Baris","family":"Kasikci","sequence":"additional","affiliation":[{"name":"University of Michigan"}]},{"given":"Karem A.","family":"Sakallah","sequence":"additional","affiliation":[{"name":"University of Michigan"}]}],"member":"320","published-online":{"date-parts":[[2019,10,27]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Verification Modulo Theories. http:\/\/www.vmt-lib.org.  Verification Modulo Theories. http:\/\/www.vmt-lib.org."},{"key":"e_1_3_2_1_2_1","unstructured":"Personal communication with authors 2019.  Personal communication with authors 2019."},{"key":"e_1_3_2_1_3_1","volume-title":"The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org","author":"Barrett C.","year":"2016","unstructured":"C. Barrett , P. Fontaine , and C. Tinelli . The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org , 2016 . C. Barrett, P. Fontaine, and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243422"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808445"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_2_1_7_1","volume-title":"USENIX Conference on Operating Systems Design and Implementation","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. Engler . Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs . In USENIX Conference on Operating Systems Design and Implementation , 2008 . C. Cadar, D. Dunbar, and D. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Conference on Operating Systems Design and Implementation, 2008."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"e_1_3_2_1_14_1","volume-title":"Dirty cow vulnerability. https:\/\/dirtycow.ninja\/","year":"2017","unstructured":"CVE-2016--5195. Dirty cow vulnerability. https:\/\/dirtycow.ninja\/ , 2017 . CVE-2016--5195. Dirty cow vulnerability. https:\/\/dirtycow.ninja\/, 2017."},{"key":"e_1_3_2_1_15_1","unstructured":"C. development team. The coq proof assistant reference manual. http:\/\/coq.inria.fr\/distrib\/current\/refman\/.  C. development team. The coq proof assistant reference manual. http:\/\/coq.inria.fr\/distrib\/current\/refman\/."},{"key":"e_1_3_2_1_16_1","volume-title":"Hornice learning for synthesizing invariants and contracts. arXiv preprint arXiv:1712.09418","author":"D'Souza D.","year":"2017","unstructured":"D. D'Souza , P. Ezudheen , P. Garg , P. Madhusudan , and D. Neider . Hornice learning for synthesizing invariants and contracts. arXiv preprint arXiv:1712.09418 , 2017 . D. D'Souza, P. Ezudheen, P. Garg, P. Madhusudan, and D. Neider. Hornice learning for synthesizing invariants and contracts. arXiv preprint arXiv:1712.09418, 2017."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_3_2_1_18_1","first-page":"1","volume-title":"Proceedings of the 2012 System, Software, SoC and Silicon Debug Conference","author":"Engblom J.","year":"2012","unstructured":"J. Engblom . A review of reverse debugging . In Proceedings of the 2012 System, Software, SoC and Silicon Debug Conference , pages 1 -- 6 . IEEE, 2012 . J. Engblom. A review of reverse debugging. In Proceedings of the 2012 System, Software, SoC and Silicon Debug Conference, pages 1--6. IEEE, 2012."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2000.870435"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15025-8_15"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_2"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2019.8715289"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_11"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08755-9_9"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254112"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_31_1","first-page":"165","volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI'14","author":"Hawblitzel C.","year":"2014","unstructured":"C. Hawblitzel , J. Howell , J. R. Lorch , A. Narayan , B. Parno , D. Zhang , and B. Zill . Ironclad apps: End-to-end security via automated full-system verification . In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI'14 , pages 165 -- 181 , Berkeley, CA, USA , 2014 . USENIX Association. C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI'14, pages 165--181, Berkeley, CA, USA, 2014. USENIX Association."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_2_1_33_1","first-page":"137","volume-title":"NASA Conference Publication","author":"Ireland A.","year":"1997","unstructured":"A. Ireland and J. Stark . On the automatic discovery of loop invariants . In NASA Conference Publication , pages 137 -- 152 . Citeseer , 1997 . A. Ireland and J. Stark. On the automatic discovery of loop invariants. In NASA Conference Publication, pages 137--152. Citeseer, 1997."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"e_1_3_2_1_35_1","volume-title":"a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM), 11(2):256--290","author":"Jackson D.","year":"2002","unstructured":"D. Jackson . Alloy : a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM), 11(2):256--290 , 2002 . D. Jackson. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM), 11(2):256--290, 2002."},{"key":"e_1_3_2_1_36_1","volume-title":"Property-directed inference of universal invariants or proving their absence. Journal of the ACM (JACM), 64(1):7","author":"Karbyshev A.","year":"2017","unstructured":"A. Karbyshev , N. Bj\u00f8rner , S. Itzhaky , N. Rinetzky , and S. Shoham . Property-directed inference of universal invariants or proving their absence. Journal of the ACM (JACM), 64(1):7 , 2017 . A. Karbyshev, N. Bj\u00f8rner, S. Itzhaky, N. Rinetzky, and S. Shoham. Property-directed inference of universal invariants or proving their absence. Journal of the ACM (JACM), 64(1):7, 2017."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_40_1","volume-title":"the TLA+ language and tools for hardware and software engineers","author":"Lamport L.","year":"2002","unstructured":"L. Lamport . Specifying systems : the TLA+ language and tools for hardware and software engineers . Addison-Wesley Longman Publishing Co., Inc. , 2002 . L. Lamport. Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc., 2002."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","first-page":"849","DOI":"10.1007\/978-3-319-08867-9_56","volume-title":"Computer-Aided Verification (CAV)","author":"Lee S.","year":"2014","unstructured":"S. Lee and K. A. Sakallah . Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction . In Computer-Aided Verification (CAV) , volume LNCS 8559 , pages 849 -- 865 , Vienna, Austria, July 2014 . Springer . S. Lee and K. A. Sakallah. Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction. In Computer-Aided Verification (CAV), volume LNCS 8559, pages 849--865, Vienna, Austria, July 2014. Springer."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_1_44_1","volume-title":"Everest project. https:\/\/www.microsoft.com\/en-us\/research\/project\/project-everest-verified-secure-implementations-https-ecosystem\/","author":"Research Microsoft","year":"2016","unstructured":"Microsoft Research . Everest project. https:\/\/www.microsoft.com\/en-us\/research\/project\/project-everest-verified-secure-implementations-https-ecosystem\/ , 2016 . Microsoft Research. Everest project. https:\/\/www.microsoft.com\/en-us\/research\/project\/project-everest-verified-secure-implementations-https-ecosystem\/, 2016."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , M. Wenzel , and L. C. Paulson . Isabelle\/HOL: A Proof Assistant for Higher-order Logic . Springer-Verlag, Berlin , Heidelberg , 2002 . T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg, 2002."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908118"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694452"},{"key":"e_1_3_2_1_49_1","first-page":"263","volume-title":"5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE'05)","author":"Sen K.","year":"2005","unstructured":"K. Sen , D. Marinov , and G. Agha . CUTE: A concolic unit testing engine for C . In 5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE'05) , pages 263 -- 272 , 2005 . K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In 5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE'05), pages 263--272, 2005."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026879"},{"key":"e_1_3_2_1_51_1","volume-title":"Chord: a scalable peer-to-peer lookup protocol for internet applications","author":"Stoica I.","year":"2003","unstructured":"I. Stoica , R. Morris , D. Liben-Nowell , D. R. Karger , M. F. Kaashoek , F. Dabek , and H. Balakrishnan . Chord: a scalable peer-to-peer lookup protocol for internet applications . IEEE\/ACM Transactions on Networking (TON) , 11(1):17--32, 2003 . I. Stoica, R. Morris, D. Liben-Nowell, D. R. Karger, M. F. Kaashoek, F. Dabek, and H. Balakrishnan. Chord: a scalable peer-to-peer lookup protocol for internet applications. IEEE\/ACM Transactions on Networking (TON), 11(1):17--32, 2003."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1145\/2034773.2034811","volume-title":"Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming","author":"Swamy N.","year":"2011","unstructured":"N. Swamy , J. Chen , C. Fournet , P. Strub , K. Bhargavan , and J. Yang . Secure distributed programming with value-dependent types. In M. M. T. Chakravarty, Z. Hu, and O. Danvy, editors , Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming , pages 266 -- 278 . ACM, 2011 . N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In M. M. T. Chakravarty, Z. Hu, and O. Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, pages 266--278. ACM, 2011."},{"key":"e_1_3_2_1_53_1","volume-title":"July 20","author":"Team A. S.","year":"2008","unstructured":"A. S. Team . Amazon S3 availability event : July 20 , 2008 . http:\/\/status.aws.amazon.com\/s3-20080720.html, 2008. A. S. Team. Amazon S3 availability event: July 20, 2008. http:\/\/status.aws.amazon.com\/s3-20080720.html, 2008."},{"key":"e_1_3_2_1_54_1","unstructured":"The Associated Press. General Electric acknowledges Northeastern blackout bug. http:\/\/www.securityfocus.com\/news\/8032 2004.  The Associated Press. General Electric acknowledges Northeastern blackout bug. http:\/\/www.securityfocus.com\/news\/8032 2004."},{"key":"e_1_3_2_1_55_1","first-page":"1","article-title":"Pretend synchrony: synchronous verification of asynchronous distributed programs","volume":"59","author":"von Gleissenthall K.","year":"2019","unstructured":"K. von Gleissenthall , R. G. Kici , A. Bakst , D. Stefan , and R. Jhala . Pretend synchrony: synchronous verification of asynchronous distributed programs . PACMPL, 3(POPL) : 59 : 1 -- 59 :30, 2019 . K. von Gleissenthall, R. G. Kici, A. Bakst, D. Stefan, and R. Jhala. Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL, 3(POPL):59:1--59:30, 2019.","journal-title":"PACMPL, 3(POPL)"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737958"},{"key":"e_1_3_2_1_57_1","volume-title":"The Fourth USENIX Workshop on Hot Topics in Parallelism","author":"Yang J.","year":"2012","unstructured":"J. Yang , A. Cui , S. Stolfo , and S. Sethumadhavan . Concurrency attacks . In The Fourth USENIX Workshop on Hot Topics in Parallelism , 2012 . J. Yang, A. Cui, S. Stolfo, and S. Sethumadhavan. Concurrency attacks. In The Fourth USENIX Workshop on Hot Topics in Parallelism, 2012."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2655056"}],"event":{"name":"SOSP '19: ACM SIGOPS 27th Symposium on Operating Systems Principles","location":"Huntsville Ontario Canada","acronym":"SOSP '19","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX Assoc USENIX Assoc"]},"container-title":["Proceedings of the 27th ACM Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341301.3359651","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341301.3359651","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341301.3359651","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:12:56Z","timestamp":1750201976000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341301.3359651"}},"subtitle":["incremental inference of inductive invariants for verification of distributed protocols"],"short-title":[],"issued":{"date-parts":[[2019,10,27]]},"references-count":58,"alternative-id":["10.1145\/3341301.3359651","10.1145\/3341301"],"URL":"https:\/\/doi.org\/10.1145\/3341301.3359651","relation":{},"subject":[],"published":{"date-parts":[[2019,10,27]]},"assertion":[{"value":"2019-10-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}