{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T11:14:51Z","timestamp":1783422891617,"version":"3.54.6"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T00:00:00Z","timestamp":1783382400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T00:00:00Z","timestamp":1783382400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2026,8]]},"DOI":"10.1007\/s10703-026-00496-7","type":"journal-article","created":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T10:24:41Z","timestamp":1783419881000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Adjointness in property directed reachability analysis"],"prefix":"10.1007","volume":"69","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8495-5925","authenticated-orcid":false,"given":"Mayuko","family":"Kori","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4624-9752","authenticated-orcid":false,"given":"Flavio","family":"Ascari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3433-723X","authenticated-orcid":false,"given":"Filippo","family":"Bonchi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7771-4154","authenticated-orcid":false,"given":"Roberto","family":"Bruni","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7424-9576","authenticated-orcid":false,"given":"Roberta","family":"Gori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,7]]},"reference":[{"key":"496_CR1","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Proc. Of VMCAI 2011. Lecture notes in computer science","author":"AR Bradley","year":"2011","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: Jhala R, Schmidt DA (eds) Proc. Of VMCAI 2011, Lecture notes in computer science, vol 6538. Springer, Berlin, Heidelberg, pp. 70\u201387. https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7."},{"key":"496_CR2","unstructured":"E\u00e9n N, Mishchenko A, Brayton RK (2011) Efficient implementation of property directed reachability. In: Bjesse P, Slobodov\u00e1 A (eds) Proc. of FMCAD 2011. FMCAD Inc, pp. 125\u2013134. http:\/\/dl.acm.org\/citation.cfm?id=2157675."},{"key":"496_CR3","doi-asserted-by":"publisher","unstructured":"Seufert T, Scholl C (2018) Combining PDR and reverse PDR for hardware model checking. In: Madsen J, Coskun AK (eds) Proc. of DATE 2018, IEEE, pp. 49\u201354. https:\/\/doi.org\/10.23919\/DATE.2018.8341978","DOI":"10.23919\/DATE.2018.8341978"},{"key":"496_CR4","doi-asserted-by":"publisher","unstructured":"Seufert T, Scholl C (2019) fbPDR: In-depth combination of forward and backward analysis in property directed reachability. In: Teich J, Fummi F (eds) Proc. of DATE 2019, IEEE, pp. 456\u2013461. https:\/\/doi.org\/10.23919\/DATE.2019.8714819","DOI":"10.23919\/DATE.2019.8714819"},{"key":"496_CR5","unstructured":"Gurfinkel A (2015) IC3, PDR, and friends. https:\/\/arieg.bitbucket.io\/pdf\/gurfinkel_ssft15.pdf"},{"key":"496_CR6","doi-asserted-by":"publisher","unstructured":"Hoder K, Bjptysetrner N (2012) Generalized property directed reachability. In: Cimatti A, Sebastiani R (eds) Proc. of SAT 2012, Lecture Notes in Computer Science, vol. 7317. Springer, pp. 157\u2013171. https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"496_CR7","volume-title":"Principles of abstract interpretation","author":"P Cousot","year":"2021","unstructured":"Cousot P (2021) Principles of abstract interpretation. MIT Press"},{"issue":"POPL","key":"496_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498676","volume":"6","author":"YMY Feldman","year":"2022","unstructured":"Feldman YMY, Sagiv M, Shoham S, Wilcox JR (2022) Property-directed reachability as abstract interpretation in the monotone theory. Proc ACM Program Lang 6(POPL):1\u201331. https:\/\/doi.org\/10.1145\/3498676","journal-title":"Proc ACM Program Lang"},{"key":"496_CR9","doi-asserted-by":"publisher","unstructured":"Batz K, Junges S, Kaminski BL, Katoen J, Matheja C, Schr\u00f6er P (2020) PrIC3: property directed reachability for MDPs. In: Lahiri SK, Wang C (eds) Proc. of CAV 2020, Part II. Lecture Notes in Computer Science, vol. 12225. Springer, pp. 512\u2013538. https:\/\/doi.org\/10.1007\/978-3-030-53291-8_27.","DOI":"10.1007\/978-3-030-53291-8_27"},{"key":"496_CR10","doi-asserted-by":"publisher","unstructured":"Kori M, Urabe N, Katsumata S, Suenaga K, Hasuo I (2022) The lattice-theoretic essence of property directed reachability analysis. In: Shoham S, Vizel Y (eds) Proc. of CAV 2022, Part I. Lecture Notes in Computer Science, vol. 13371. Springer, pp. 235\u2013256. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_12.","DOI":"10.1007\/978-3-031-13185-1_12"},{"issue":"3\/4","key":"496_CR11","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","volume":"23","author":"FW Lawvere","year":"1969","unstructured":"Lawvere FW (1969) Adjointness in foundations. Dialectica 23(3\/4):281\u2013296. https:\/\/doi.org\/10.1111\/j.1746-8361.1969.tb01194.x","journal-title":"Dialectica"},{"key":"496_CR12","unstructured":"Levy PB. Call-By-Push-Value: a Functional\/Imperative synthesis. Semantics"},{"key":"496_CR13","unstructured":"Seufert T, Scholl C (2017) Sequential verification using reverse PDR. In: Gro\u00dfe D, Drechsler R (eds) Proc. of MBMV 2017, Shaker Verlag, pp. 79\u201390"},{"key":"496_CR14","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J (2008) Principles of model checking. MIT Press."},{"key":"496_CR15","doi-asserted-by":"publisher","unstructured":"Dehnert C, Junges S, Katoen J, Volk M (2017) A storm is coming: a modern probabilistic model checker. In: Majumdar R, Kuncak V (eds) Proc. of CAV 2017, Part II. Lecture Notes in Computer Science, vol. 10427. Springer, pp. 592\u2013600. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31.","DOI":"10.1007\/978-3-319-63390-9_31"},{"issue":"2","key":"496_CR16","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 (2000) Making abstract interpretations complete. J Acm 47(2):361\u2013416. https:\/\/doi.org\/10.1145\/333979.333989","journal-title":"J Acm"},{"key":"496_CR17","doi-asserted-by":"publisher","unstructured":"Cimatti A, Griggio A (2012) Software model checking via IC3. In: Madhusudan P, Seshia SA (eds) Proc. of CAV 2012, Lecture Notes in Computer Science, vol. 7358. Springer, pp. 277\u2013293. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23","DOI":"10.1007\/978-3-642-31424-7_23"},{"issue":"2","key":"496_CR18","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10009-019-00547-x","volume":"22","author":"T Lange","year":"2020","unstructured":"Lange T, Neuh\u00e4u\u00dfer MR, Noll T, Katoen J (2020) IC3 software model checking. Int J Softw Tools Technol Transf 22(2):135\u2013161. https:\/\/doi.org\/10.1007\/s10009-019-00547-x","journal-title":"Int J Softw Tools Technol Transf"},{"key":"496_CR19","doi-asserted-by":"publisher","unstructured":"Suda M (2014) Property directed reachability for automated planning. In: Chien SA, Do MB, Fern A, Ruml W (eds) Proc. of ICAPS 2014, AAAI. https:\/\/doi.org\/10.1613\/jair.4231","DOI":"10.1613\/jair.4231"},{"key":"496_CR20","doi-asserted-by":"publisher","unstructured":"Cousot P (2000) Partial completeness of abstract fixpoint checking. In: Choueiry BY, Walsh T (eds) Proc. of SARA 2000, Lecture Notes in Computer Science, vol. 1864. Springer, pp. 1\u201325. https:\/\/doi.org\/10.1007\/3-540-44914-0_1","DOI":"10.1007\/3-540-44914-0_1"},{"key":"496_CR21","doi-asserted-by":"publisher","unstructured":"Kori M, Ascari F, Bonchi F, Bruni R, Gori R, Hasuo I (2023) Exploiting adjoints in property directed reachability analysis. In: Enea C, Lal A (eds) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965. Springer, pp. 41\u201363. https:\/\/doi.org\/10.1007\/978-3-031-37703-7_3","DOI":"10.1007\/978-3-031-37703-7_3"},{"key":"496_CR22","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to lattices and order","author":"BA Davey","year":"2002","unstructured":"Davey BA, Priestley HA (2002) Introduction to lattices and order, Second edn. Cambridge University Press","edition":"Second"},{"key":"496_CR23","doi-asserted-by":"crossref","unstructured":"MacLane S (1971) Categories for the working Mathematician. In: Graduate texts in mathematics, vol 5. Springer, New York, p 262","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"496_CR24","doi-asserted-by":"publisher","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL 1977, ACM, pp. 238\u2013252. https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"496_CR25","doi-asserted-by":"publisher","unstructured":"Bonchi F, Ganty P, Giacobazzi R, Pavlovic D (2018) Sound up-to techniques and complete abstract domains. In: Dawar A, Gr\u00e4del E (eds) Proc. of LICS 2018. ACM, pp. 175\u2013184. https:\/\/doi.org\/10.1145\/3209108.3209169","DOI":"10.1145\/3209108.3209169"},{"key":"496_CR26","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner R (1989) Communication and concurrency. Prentice-Hall, Inc., USA"},{"key":"496_CR27","volume-title":"Basic concepts of enriched category theory","author":"GM Kelly","year":"1982","unstructured":"Kelly GM (1982) Basic concepts of enriched category theory, vol 64. CUP Archive"},{"key":"496_CR28","doi-asserted-by":"publisher","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proc. of CAV 2011, Lecture Notes in Computer Science, vol 6806. Springer, pp. 585\u2013591. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"496_CR29","doi-asserted-by":"publisher","unstructured":"Moura LM, Bjptysetrner NS (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Proc. of TACAS 2008. Lecture Notes in Computer Science, vol. 4963. Springer, pp. 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"496_CR30","doi-asserted-by":"publisher","unstructured":"Hartmanns A, Klauck M, Parker D, Quatmann T, Ruijters E (2019) The quantitative verification benchmark set. In: Vojnar T, Zhang L (eds) Proc. of TACAS 2019, Part I. Lecture Notes in Computer Science, vol. 11427. Springer, pp. 344\u2013350. https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"496_CR31","doi-asserted-by":"publisher","unstructured":"Quatmann T, Katoen J (2018) Sound value iteration. In: Chockler H, Weissenbacher G (eds) Proc. of CAV 2018, Part I. Lecture Notes in Computer Science, vol. 10981. Springer, pp. 643\u2013661. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"496_CR32","doi-asserted-by":"publisher","unstructured":"Baier C, Klein J, Leuschner L, Parker D, Wunderlich S (2017) Ensuring the reliability of your model checker: interval iteration for Markov Decision Processes. In: Majumdar R, Kuncak V (eds) Proc. of CAV 2017, Part I. Lecture Notes in Computer Science, vol 10426. Springer, pp. 160\u2013180. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"496_CR33","doi-asserted-by":"publisher","unstructured":"Hartmanns A, Kaminski BL (2020) Optimistic value iteration. In: Lahiri SK, Wang C (eds) Proc. of CAV 2020, Part II. Lecture Notes in Computer Science, vol. 12225. Springer, pp. 488\u2013511. https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","DOI":"10.1007\/978-3-030-53291-8_26"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00496-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-026-00496-7","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00496-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T10:24:55Z","timestamp":1783419895000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-026-00496-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,7]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,8]]}},"alternative-id":["496"],"URL":"https:\/\/doi.org\/10.1007\/s10703-026-00496-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,7]]},"assertion":[{"value":"14 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 April 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 July 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"Not applicable.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}},{"value":"The authors declare no competing interests.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"1"}}