{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:54:13Z","timestamp":1760043253054,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377020"},{"type":"electronic","value":"9783031377037"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley\u2019s property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use the second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes.<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_3","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"41-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Exploiting Adjoints in Property Directed Reachability Analysis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8495-5925","authenticated-orcid":false,"given":"Mayuko","family":"Kori","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4624-9752","authenticated-orcid":false,"given":"Flavio","family":"Ascari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3433-723X","authenticated-orcid":false,"given":"Filippo","family":"Bonchi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7771-4154","authenticated-orcid":false,"given":"Roberto","family":"Bruni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7424-9576","authenticated-orcid":false,"given":"Roberta","family":"Gori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"3_CR1","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Batz, K., et al.: PrIC3: property directed reachability for MDPs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 512\u2013538. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_27","DOI":"10.1007\/978-3-030-53291-8_27"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Bonchi, F., Ganty, P., Giacobazzi, R., Pavlovic, D.: Sound up-to techniques and complete abstract domains. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of LICS 2018, pp. 175\u2013184. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209169","DOI":"10.1145\/3209108.3209169"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277\u2013293. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Cousot, P.: Partial completeness of abstract fixpoint checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, pp. 1\u201325. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44914-0_1","DOI":"10.1007\/3-540-44914-0_1"},{"key":"3_CR8","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press (2021)"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd Edn. Cambridge University Press (2002)","DOI":"10.1017\/CBO9780511809088"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"3_CR12","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Bjesse, P., Slobodov\u00e1, A. (eds.) Proc. of FMCAD 2011. pp. 125\u2013134. FMCAD Inc. (2011). http:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Feldman, Y.M.Y., Sagiv, M., Shoham, S., Wilcox, J.R.: Property-directed reachability as abstract interpretation in the monotone theory. Proc. ACM Program. Lang. 6(POPL), 1\u201331 (2022). https:\/\/doi.org\/10.1145\/3498676","DOI":"10.1145\/3498676"},{"issue":"2","key":"3_CR14","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361\u2013416 (2000). https:\/\/doi.org\/10.1145\/333979.333989","journal-title":"J. ACM"},{"key":"3_CR15","unstructured":"Gurfinkel, A.: IC3, PDR, and friends (2015). https:\/\/arieg.bitbucket.io\/pdf\/gurfinkel_ssft15.pdf"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 488\u2013511. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344\u2013350. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Kori, M., Urabe, N., Katsumata, S., Suenaga, K., Hasuo, I.: The lattice-theoretic essence of property directed reachability analysis. In: Shoham, S., Vizel, Y. (eds.) Proceedings of CAV 2022, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 235\u2013256. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_12","DOI":"10.1007\/978-3-031-13185-1_12"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"2","key":"3_CR21","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10009-019-00547-x","volume":"22","author":"T Lange","year":"2019","unstructured":"Lange, T., Neuh\u00e4u\u00dfer, M.R., Noll, T., Katoen, J.-P.: IC3 software model checking. Int. J. Softw. Tools Technol. Trans. 22(2), 135\u2013161 (2019). https:\/\/doi.org\/10.1007\/s10009-019-00547-x","journal-title":"Int. J. Softw. Tools Technol. Trans."},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Levy, P.B.: Call-By-Push-Value: A Functional\/Imperative Synthesis, Semantics Structures in Computation, vol. 2. Springer, Dordrecht (2004). https:\/\/doi.org\/10.1007\/978-94-007-0954-6","DOI":"10.1007\/978-94-007-0954-6"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"MacLane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer-Verlag, New York (1971)","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"3_CR24","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall Inc, USA (1989)"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.-P.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 643\u2013661. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"3_CR27","unstructured":"Seufert, T., Scholl, C.: Sequential verification using reverse PDR. In: Gro\u00dfe, D., Drechsler, R. (eds.) Proceedings of MBMV 2017, pp. 79\u201390. Shaker Verlag (2017)"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Seufert, T., Scholl, C.: Combining PDR and reverse PDR for hardware model checking. In: Madsen, J., Coskun, A.K. (eds.) Proceedings of DATE 2018, pp. 49\u201354. IEEE (2018). https:\/\/doi.org\/10.23919\/DATE.2018.8341978","DOI":"10.23919\/DATE.2018.8341978"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Seufert, T., Scholl, C.: fbPDR: In-depth combination of forward and backward analysis in property directed reachability. In: Teich, J., Fummi, F. (eds.) Proceedings of DATE 2019, pp. 456\u2013461. IEEE (2019). https:\/\/doi.org\/10.23919\/DATE.2019.8714819","DOI":"10.23919\/DATE.2019.8714819"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Suda, M.: Property directed reachability for automated planning. In: Chien, S.A., Do, M.B., Fern, A., Ruml, W. (eds.) Proceedings of ICAPS 2014. AAAI (2014). https:\/\/doi.org\/10.1613\/jair.4231","DOI":"10.1613\/jair.4231"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37703-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:02:46Z","timestamp":1693047766000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"18 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"26% - 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":"11","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)"}}]}}