Exploiting adjoints in property directed reachability analysis

DOI10.1007/978-3-031-37703-7_3zbMATH Open1545.68072MaRDI QIDQ6535527FDOQ6535527

Authors: Flavio Ascari, Filippo Bonchi, Roberto Bruni, Roberta Gori, Ichiro Hasuo 

Publication date: 12 January 2024

Recommendations

• The Lattice-Theoretic Essence of Property Directed Reachability Analysis
• Property directed polyhedral abstraction
• Property directed abstract interpretation
• scientific article; zbMATH DE number 1884411
• Generalized property directed reachability

zbMATH Keywords

lattice theoryadjointsMDPsover-approximationPDR

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• SAT-Based Model Checking without Unrolling
• Generalized property directed reachability
• Title not available (Why is that?)
• Making abstract interpretations complete
• Property directed reachability for automated planning
• Principles of abstract interpretation
• Ensuring the reliability of your model checker: interval iteration for Markov decision processes
• Optimistic value iteration
• \textsf{PrIC3}: property directed reachability for MDPs
• Sound value iteration
• Title not available (Why is that?)
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis
• Sound up-to techniques and complete abstract domains

This page was built for publication: Exploiting adjoints in property directed reachability analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535527)