{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:54Z","timestamp":1774837974967,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":65,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,12]],"date-time":"2018-07-12T00:00:00Z","timestamp":1531353600000},"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":["CCF-1566363,CCF-1652517"],"award-info":[{"award-number":["CCF-1566363,CCF-1652517"]}],"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":[[2018,7,12]]},"DOI":"10.1145\/3213846.3213877","type":"proceedings-article","created":{"date-parts":[[2018,7,12]],"date-time":"2018-07-12T17:46:44Z","timestamp":1531417604000},"page":"344-355","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["piCoq: parallel regression proving for large-scale verification projects"],"prefix":"10.1145","author":[{"given":"Karl","family":"Palmskog","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmet","family":"Celik","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milos","family":"Gligoric","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,7,12]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178245"},{"key":"e_1_3_2_1_3_1","volume-title":"Proof General: A Generic Tool for Proof Development. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 38\u201343","author":"Aspinall David","year":"2000","unstructured":"David Aspinall . 2000 . Proof General: A Generic Tool for Proof Development. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 38\u201343 . David Aspinall. 2000. Proof General: A Generic Tool for Proof Development. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 38\u201343."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39320-4_29"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_4"},{"key":"e_1_3_2_1_6_1","volume-title":"https:\/\/bazel.io\/blog\/","author":"Blog WebPage","year":"2018","unstructured":"BazelBlog WebPage 2018. Bazel - Blog . ( 2018 ). https:\/\/bazel.io\/blog\/ . BazelBlogWebPage 2018. Bazel - Blog. (2018). https:\/\/bazel.io\/blog\/."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568248"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786823"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2013.30"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Jeanderson Candido Luis Melo and Marcelo d\u2019Amorim. 2017. Test Suite Parallelization in Open-Source Projects: A Study on Its Usage and Impact. In Automated Software Engineering. 838\u2013848.   Jeanderson Candido Luis Melo and Marcelo d\u2019Amorim. 2017. Test Suite Parallelization in Open-Source Projects: A Study on Its Usage and Impact. In Automated Software Engineering. 838\u2013848.","DOI":"10.1109\/ASE.2017.8115695"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Ahmet Celik Karl Palmskog and Milos Gligoric. 2017. iCoq: Regression Proof Selection for Large-Scale Verification Projects. In Automated Software Engineering. 171\u2013182.   Ahmet Celik Karl Palmskog and Milos Gligoric. 2017. iCoq: Regression Proof Selection for Large-Scale Verification Projects. In Automated Software Engineering. 171\u2013182.","DOI":"10.1109\/ASE.2017.8115630"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3183493"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Soham Sundar Chakraborty and Vipul Shah. 2011. Towards an Approach and Framework for Test-execution Plan Derivation. In Automated Software Engineering. 488\u2013491.  Soham Sundar Chakraborty and Vipul Shah. 2011. Towards an Approach and Framework for Test-execution Plan Derivation. In Automated Software Engineering. 488\u2013491.","DOI":"10.1109\/ASE.2011.6100106"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_17_1","unstructured":"Cyril Cohen. 2017. finmap. (2017). https:\/\/github.com\/math-comp\/finmap.  Cyril Cohen. 2017. finmap. (2017). https:\/\/github.com\/math-comp\/finmap."},{"key":"e_1_3_2_1_18_1","unstructured":"Al Danial. 2017. cloc - counts blank lines comment lines and physical lines of source code in many programming languages. (2017).  Al Danial. 2017. cloc - counts blank lines comment lines and physical lines of source code in many programming languages. (2017)."},{"key":"e_1_3_2_1_19_1","unstructured":"https:\/\/github.com\/ AlDanial\/cloc.  https:\/\/github.com\/ AlDanial\/cloc."},{"key":"e_1_3_2_1_20_1","unstructured":"Coq development team. 2018. Coq Package Index. (2018). https:\/\/coq.inria.fr\/ opam\/www\/.  Coq development team. 2018. Coq Package Index. (2018). https:\/\/coq.inria.fr\/ opam\/www\/."},{"key":"e_1_3_2_1_21_1","unstructured":"MathComp development team. 2018. Mathematical Components Project. (2018). https:\/\/math-comp.github.io\/math-comp\/  MathComp development team. 2018. Mathematical Components Project. (2018). https:\/\/math-comp.github.io\/math-comp\/"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2889222"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_18"},{"key":"e_1_3_2_1_24_1","unstructured":"FomegacGit 2016. Fomegac Git repository. (2016). https:\/\/github.com\/skeuchel\/ fomegac.git.  FomegacGit 2016. Fomegac Git repository. (2016). https:\/\/github.com\/skeuchel\/ fomegac.git."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3098222"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0001-5"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771784"},{"key":"e_1_3_2_1_28_1","volume-title":"Java Concurrency in Practice","author":"Goetz Brian","unstructured":"Brian Goetz , Tim Peierls , Joshua Bloch , Joseph Bowbeer , David Holmes , and Doug Lea . 2006. Java Concurrency in Practice . Addison-Wesley . Brian Goetz, Tim Peierls, Joshua Bloch, Joseph Bowbeer, David Holmes, and Doug Lea. 2006. Java Concurrency in Practice. Addison-Wesley."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_30_1","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier Georges","year":"2010","unstructured":"Georges Gonthier and Assia Mahboubi . 2010 . An introduction to small scale reflection in Coq . Journal of Formalized Reasoning 3 , 2 (2010), 95 \u2013 152 . Georges Gonthier and Assia Mahboubi. 2010. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning 3, 2 (2010), 95\u2013152.","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Thomas Hales Mark Adams Gertrud Bauer Tat Dat Dang John Harrison Le Truong Hoang Cezary Kaliszyk Victor Magron Sean McLaughlin Tat Thang Nguyen Quang Truong Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason Rute Alexey Solovyev Thi Hoai An Ta Nam Trung Tran Thi Diep Trieu Josef Urban Ky Vu and Roland Zumkeller. 2017. A Formal Proof of the Kepler Conjecture. Forum of Mathematics Pi 5 (2017).  Thomas Hales Mark Adams Gertrud Bauer Tat Dat Dang John Harrison Le Truong Hoang Cezary Kaliszyk Victor Magron Sean McLaughlin Tat Thang Nguyen Quang Truong Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason Rute Alexey Solovyev Thi Hoai An Ta Nam Trung Tran Thi Diep Trieu Josef Urban Ky Vu and Roland Zumkeller. 2017. A Formal Proof of the Kepler Conjecture. Forum of Mathematics Pi 5 (2017).","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970358"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_34_1","volume-title":"Barnett","author":"Kushneryk Colin J. W.","year":"2010","unstructured":"Colin J. W. Kushneryk and Paul D . Barnett . 2010 . Parallel Test Execution . (2010). https:\/\/patents.google.com\/patent\/US20120102462A1\/en. Colin J. W. Kushneryk and Paul D. Barnett. 2010. Parallel Test Execution. (2010). https:\/\/patents.google.com\/patent\/US20120102462A1\/en."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950361"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176926"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635920"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-SEIP.2017.16"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Springer.   Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Springer.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_42_1","unstructured":"OPAM 2018. OCaml Package Manager. (2018). https:\/\/opam.ocaml.org.  OPAM 2018. OCaml Package Manager. (2018). https:\/\/opam.ocaml.org."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2972206.2972224"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029894.1029928"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/101514.101522"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_31"},{"key":"e_1_3_2_1_47_1","volume-title":"Surface Effects for Deterministic Parallelism. In Symposium on Trends in Functional Programming. ftp:\/\/ftp-sop. inria.fr\/indes\/TFP15\/TFP2015_submission_5.pdf","author":"Rodrigues Vitor","year":"2015","unstructured":"Vitor Rodrigues and Matthew Fluet . 2015 . Surface Effects for Deterministic Parallelism. In Symposium on Trends in Functional Programming. ftp:\/\/ftp-sop. inria.fr\/indes\/TFP15\/TFP2015_submission_5.pdf Vitor Rodrigues and Matthew Fluet. 2015. Surface Effects for Deterministic Parallelism. In Symposium on Trends in Functional Programming. ftp:\/\/ftp-sop. inria.fr\/indes\/TFP15\/TFP2015_submission_5.pdf"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.536955"},{"key":"e_1_3_2_1_49_1","volume-title":"Universe Polymorphism in Coq. In International Conference on Interactive Theorem Proving. 499\u2013514","author":"Sozeau Matthieu","year":"2014","unstructured":"Matthieu Sozeau and Nicolas Tabareau . 2014 . Universe Polymorphism in Coq. In International Conference on Interactive Theorem Proving. 499\u2013514 . Matthieu Sozeau and Nicolas Tabareau. 2014. Universe Polymorphism in Coq. In International Conference on Interactive Theorem Proving. 499\u2013514."},{"key":"e_1_3_2_1_50_1","unstructured":"Speeding up the build 2018. Speeding up the build. (2018). http:\/\/docs.travis-ci. com\/user\/speeding-up-the-build.  Speeding up the build 2018. Speeding up the build. (2018). http:\/\/docs.travis-ci. com\/user\/speeding-up-the-build."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566187"},{"key":"e_1_3_2_1_52_1","unstructured":"StructTact 2018. StructTact library. (2018). https:\/\/github.com\/uwplse\/StructTact.  StructTact 2018. StructTact library. (2018). https:\/\/github.com\/uwplse\/StructTact."},{"key":"e_1_3_2_1_53_1","volume-title":"Coq Manual: Asynchronous and Parallel Proof Processing.","author":"Tassi Enrico","year":"2019","unstructured":"Enrico Tassi . 2019 . Coq Manual: Asynchronous and Parallel Proof Processing. (2019). Enrico Tassi. 2019. Coq Manual: Asynchronous and Parallel Proof Processing. (2019)."},{"key":"e_1_3_2_1_54_1","unstructured":"https:\/\/coq.inria.fr\/refman\/addendum\/parallel-proof-processing.html.  https:\/\/coq.inria.fr\/refman\/addendum\/parallel-proof-processing.html."},{"key":"e_1_3_2_1_55_1","volume-title":"Coq Manual: Utilities.","author":"Development Team The Coq","year":"2018","unstructured":"The Coq Development Team . 2018 . Coq Manual: Utilities. (2018). https:\/\/coq. inria.fr\/refman\/practical-tools\/utilities.html. The Coq Development Team. 2018. Coq Manual: Utilities. (2018). https:\/\/coq. inria.fr\/refman\/practical-tools\/utilities.html."},{"key":"e_1_3_2_1_56_1","volume-title":"https:\/\/travis-ci.org","author":"CI","year":"2018","unstructured":"Travis CI 2018. Travis CI. ( 2018 ). https:\/\/travis-ci.org . TravisCI 2018. Travis CI. (2018). https:\/\/travis-ci.org."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1002\/smr.1838"},{"key":"e_1_3_2_1_58_1","volume-title":"PIDE as front-end technology for Coq. CoRR abs\/1304.6626","author":"Wenzel Makarius","year":"2013","unstructured":"Makarius Wenzel . 2013. PIDE as front-end technology for Coq. CoRR abs\/1304.6626 ( 2013 ). http:\/\/arxiv.org\/abs\/1304.6626 Makarius Wenzel. 2013. PIDE as front-end technology for Coq. CoRR abs\/1304.6626 (2013). http:\/\/arxiv.org\/abs\/1304.6626"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_30"},{"key":"e_1_3_2_1_60_1","volume-title":"Asynchronous User Interaction and Tool Integration in Isabelle\/PIDE. In International Conference on Interactive Theorem Proving. 515\u2013 530","author":"Wenzel Makarius","year":"2014","unstructured":"Makarius Wenzel . 2014 . Asynchronous User Interaction and Tool Integration in Isabelle\/PIDE. In International Conference on Interactive Theorem Proving. 515\u2013 530 . Makarius Wenzel. 2014. Asynchronous User Interaction and Tool Integration in Isabelle\/PIDE. In International Conference on Interactive Theorem Proving. 515\u2013 530."},{"key":"e_1_3_2_1_61_1","volume-title":"Scaling Isabelle Proof Document Processing. (December","author":"Wenzel Makarius","year":"2017","unstructured":"Makarius Wenzel . 2017. Scaling Isabelle Proof Document Processing. (December 2017 ). http:\/\/sketis.net\/wp-content\/uploads\/2017\/12\/Isabelle_Scaling_Dec-2017. Makarius Wenzel. 2017. Scaling Isabelle Proof Document Processing. (December 2017). http:\/\/sketis.net\/wp-content\/uploads\/2017\/12\/Isabelle_Scaling_Dec-2017."},{"key":"e_1_3_2_1_62_1","unstructured":"pdf.  pdf."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1002\/stv.430"}],"event":{"name":"ISSTA '18: International Symposium on Software Testing and Analysis","location":"Amsterdam Netherlands","acronym":"ISSTA '18","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3213846.3213877","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3213846.3213877","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3213846.3213877","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:42Z","timestamp":1750212462000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3213846.3213877"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,12]]},"references-count":65,"alternative-id":["10.1145\/3213846.3213877","10.1145\/3213846"],"URL":"https:\/\/doi.org\/10.1145\/3213846.3213877","relation":{},"subject":[],"published":{"date-parts":[[2018,7,12]]},"assertion":[{"value":"2018-07-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}