{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:43:28Z","timestamp":1777347808024,"version":"3.51.4"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030945824","type":"print"},{"value":"9783030945831","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-94583-1_18","type":"book-chapter","created":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T22:02:34Z","timestamp":1642111354000},"page":"355-377","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Making PROGRESS in Property Directed Reachability"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Seufert","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[]},{"given":"Arun","family":"Chandrasekharan","sequence":"additional","affiliation":[]},{"given":"Sven","family":"Reimer","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Welp","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"key":"18_CR1","unstructured":"Baumgartner, J., Ivrii, A., Matsliah, A., Mony, H.: IC3-guided abstraction. In: FMCAD, pp. 182\u2013185 (2012). https:\/\/ieeexplore.ieee.org\/document\/6462571\/"},{"key":"18_CR2","doi-asserted-by":"publisher","unstructured":"Berryhill, R., Ivrii, A., Veira, N., Veneris, A.G.: Learning support sets in IC3 and quip: the good, the bad, and the ugly. In: 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, pp. 140\u2013147. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102252","DOI":"10.23919\/FMCAD.2017.8102252"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS, pp. 193\u2013207 (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition (2017). http:\/\/fmv.jku.at\/hwmcc17\/","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"18_CR5","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: Aiger 1.9 and beyond (2011). http:\/\/fmv.jku.at\/hwmcc11\/beyond1.pdf"},{"key":"18_CR6","unstructured":"Biere, A., Preiner, M.: Hardware model checking competition (2019). http:\/\/fmv.jku.at\/hwmcc19\/"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction guided abstraction refinement (CTIGAR). In: CAV, pp. 831\u2013848 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_55","DOI":"10.1007\/978-3-319-08867-9_55"},{"key":"18_CR8","unstructured":"Bradley, A.: Ic3 reference implementation (2013). https:\/\/github.com\/arbrad\/IC3ref"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: Sat-based model checking without unrolling. In: VMCAI, pp. 70\u201387 (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15\u201318 November 2009, Austin, Texas, USA, pp. 69\u201376. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351141","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-04772-5_40","volume-title":"Computer Aided Systems Theory - EUROCAST 2009","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Effective bit-width and under-approximation. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2009. LNCS, vol. 5717, pp. 304\u2013311. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04772-5_40"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RE Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358\u2013372. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_28"},{"key":"18_CR14","unstructured":"Chockler, H., Ivrii, A., Matsliah, A., Moran, S., Nevo, Z.: Incremental formal verification of hardware. In: FMCAD, pp. 135\u2013143 (2011). http:\/\/dl.acm.org\/citation.cfm?id=2157676"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-60045-0_66","volume-title":"Computer Aided Verification","author":"DL Dill","year":"1995","unstructured":"Dill, D.L., Wong-Toi, H.: Verification of real-time systems by successive over and under approximation. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 409\u2013422. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60045-0_66"},{"key":"18_CR17","unstructured":"E\u00e9n, N., Mishchenko, A., Amla, N.: A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. In: Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, 20\u201323 October 2010, pp. 181\u2013188. IEEE (2010). https:\/\/ieeexplore.ieee.org\/document\/5770948\/"},{"key":"18_CR18","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125\u2013134 (2011). http:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: SAT, pp. 502\u2013518 (2003). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"18_CR20","unstructured":"Franz\u00e9n, A.: Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. Ph.D. thesis, University of Trento, Italy (2010). http:\/\/eprints-phd.biblio.unitn.it\/345\/"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Griggio, A., Roveri, M.: Comparing different variants of the ic3 algorithm for hardware model checking. IEEE Trans. CAD Integr. Circuits Syst. 35(6), 1026\u20131039 (2016). https:\/\/doi.org\/10.1109\/TCAD.2015.2481869","DOI":"10.1109\/TCAD.2015.2481869"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-642-31424-7_38","volume-title":"Computer Aided Verification","author":"Z Hassan","year":"2012","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Incremental, inductive CTL model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 532\u2013547. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_38"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in IC3. In: FMCAD, pp. 157\u2013164 (2013). https:\/\/ieeexplore.ieee.org\/document\/6679405\/","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Ho, Y., Mishchenko, A., Brayton, R.K.: Property directed reachability with word-level abstraction. In: 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, pp. 132\u2013139. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102251","DOI":"10.23919\/FMCAD.2017.8102251"},{"issue":"1&2","key":"18_CR25","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0743-1066(93)90018-C","volume":"15","author":"JN Hooker","year":"1993","unstructured":"Hooker, J.N.: Solving the incremental satisfiability problem. J. Log. Program. 15(1 & 2), 177\u2013186 (1993)","journal-title":"J. Log. Program."},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Ivrii, A., Gurfinkel, A.: Pushing to the top. In: FMCAD, pp. 65\u201372 (2015). https:\/\/www.cs.utexas.edu\/users\/hunt\/FMCAD\/FMCAD15\/papers\/paper39.pdf","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D Kroening","year":"2004","unstructured":"Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O.: Abstraction-based satisfiability solving of presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 308\u2013320. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_24"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)","DOI":"10.1515\/9781400864041"},{"key":"18_CR29","first-page":"613","volume":"185","author":"CM Li","year":"2009","unstructured":"Li, C.M., Manya, F.: Maxsat, hard and soft constraints. Handb. Satisf. 185, 613\u2013631 (2009)","journal-title":"Handb. Satisf."},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2\u201317. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_2"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Mishchenko, A., E\u00e9n, N., Brayton, R.K., Baumgartner, J., Mony, H., Nalla, P.K.: GLA: gate-level abstraction revisited. In: Design, Automation and Test in Europe, DATE 13, Grenoble, France, 18\u201322 March 2013, pp. 1399\u20131404. EDA Consortium San Jose, CA, USA\/ACM DL (2013). https:\/\/doi.org\/10.7873\/DATE.2013.286","DOI":"10.7873\/DATE.2013.286"},{"issue":"6","key":"18_CR32","doi-asserted-by":"publisher","first-page":"1234","DOI":"10.1109\/TC.2012.53","volume":"62","author":"T Nopper","year":"2013","unstructured":"Nopper, T., Scholl, C.: Symbolic model checking for incomplete designs with flexible modeling of unknowns. IEEE Trans. Comput. 62(6), 1234\u20131254 (2013)","journal-title":"IEEE Trans. Comput."},{"key":"18_CR33","unstructured":"Preiner, M., Biere, A., Froleyks, N.: Hardware model checking competition 2020 (2020). http:\/\/fmv.jku.at\/hwmcc20\/"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: TACAS, pp. 31\u201345 (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_3","DOI":"10.1007\/978-3-540-24730-2_3"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"Scheibler, K., Winterer, F., Seufert, T., Teige, T., Scholl, C., Becker, B.: ICP and IC3. In: Design, Automation & Test in Europe Conference & Exhibition, DATE 2021 (2021). https:\/\/doi.org\/10.23919\/DATE51398.2021.9473970","DOI":"10.23919\/DATE51398.2021.9473970"},{"key":"18_CR36","doi-asserted-by":"publisher","unstructured":"Seufert, T., Scholl, C.: fbpdr: In-depth combination of forward and backward analysis in property directed reachability. In: Design, Automation & Test in Europe Conference & Exhibition, DATE 2019, Florence, Italy, 25\u201329 March 2019, pp. 456\u2013461. IEEE (2019). https:\/\/doi.org\/10.23919\/DATE.2019.8714819","DOI":"10.23919\/DATE.2019.8714819"},{"key":"18_CR37","unstructured":"Seufert, T., Scholl, C., Chandrasekharan, A., Reimer, S., Welp, T.: Reproduction artifact (2021). https:\/\/abs.informatik.uni-freiburg.de\/src\/projects_view.php?projectID=23"},{"key":"18_CR38","unstructured":"Seufert, T., Winterer, F., Scholl, C., Scheibler, K., Paxian, T., Becker, B.: Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR. arXiv preprint arXiv:2105.09169 (2021). https:\/\/arxiv.org\/abs\/2105.09169"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP-a new search algorithm for satisfiability. In: ICCAD, pp. 220\u2013227 (1996). https:\/\/doi.org\/10.1109\/ICCAD.1996.569607","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"18_CR40","unstructured":"Tseitin, G.: On the complexity of derivations in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logics (1968)"},{"key":"18_CR41","unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Lazy abstraction and SAT-based reachability in hardware model checking. In: FMCAD, pp. 173\u2013181 (2012). https:\/\/ieeexplore.ieee.org\/document\/6462570\/"},{"key":"18_CR42","doi-asserted-by":"publisher","unstructured":"Wang, D., et al.: Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, 18\u201322 June 2001, pp. 35\u201340. ACM (2001). https:\/\/doi.org\/10.1145\/378239.378260","DOI":"10.1145\/378239.378260"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-94583-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T00:06:56Z","timestamp":1642118816000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-94583-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030945824","9783030945831"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-94583-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"14 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Philadelphia, PA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 January 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl22.sigplan.org\/home\/VMCAI-2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"37% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}