{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:32:14Z","timestamp":1750221134121,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T00:00:00Z","timestamp":1557705600000},"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":[[2019,5,13]]},"DOI":"10.1145\/3317550.3321451","type":"proceedings-article","created":{"date-parts":[[2019,5,10]],"date-time":"2019-05-10T19:01:58Z","timestamp":1557514918000},"page":"30-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards Automatic Inference of Inductive Invariants"],"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,5,13]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"IEEE Standard for System Verilog--Unified Hardware Design Specification and Verification Language. IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012) pages 1--1315 Feb 2018.  IEEE Standard for System Verilog--Unified Hardware Design Specification and Verification Language. IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012) pages 1--1315 Feb 2018."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243422"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808445"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_2_1_5_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_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"volume-title":"Dirty cow vulnerability. https:\/\/dirtycow.mnja\/","year":"2017","key":"e_1_3_2_1_10_1","unstructured":"CVE-2016-5195. Dirty cow vulnerability. https:\/\/dirtycow.mnja\/ , 2017 . CVE-2016-5195. Dirty cow vulnerability. https:\/\/dirtycow.mnja\/, 2017."},{"key":"e_1_3_2_1_11_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_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337240"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_18_1","unstructured":"A. Goel and K. Sakallah. Averroes 2. http:\/\/www.github.com\/aman-goel\/avr.  A. Goel and K. Sakallah. Averroes 2. http:\/\/www.github.com\/aman-goel\/avr."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2019.8715289"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_11"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254112"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_23_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_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022187"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_30_1","volume-title":"Specifying systems: 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_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_56"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_35_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_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694452"},{"key":"e_1_3_2_1_38_1","volume-title":"https:\/\/www.microsoft.com\/en-us\/research\/project\/project-everest-verified-secure-implementations-https-ecosystem\/","author":"Research M.","year":"2016","unstructured":"M. Research . Everest project. https:\/\/www.microsoft.com\/en-us\/research\/project\/project-everest-verified-secure-implementations-https-ecosystem\/ , 2016 . M. 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_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_1_41_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_42_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_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_44_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."}],"event":{"name":"HotOS '19: Workshop on Hot Topics in Operating Systems","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Bertinoro Italy","acronym":"HotOS '19"},"container-title":["Proceedings of the Workshop on Hot Topics in Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3317550.3321451","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3317550.3321451","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:27Z","timestamp":1750208547000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3317550.3321451"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,13]]},"references-count":44,"alternative-id":["10.1145\/3317550.3321451","10.1145\/3317550"],"URL":"https:\/\/doi.org\/10.1145\/3317550.3321451","relation":{},"subject":[],"published":{"date-parts":[[2019,5,13]]},"assertion":[{"value":"2019-05-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}