Draft:Property-Directed Reachability


Property-Directed Reachability (PDR), also known as Incremental Construction of Inductive Clauses for Indubitable Correctness (IC3),[1] is an algorithm for model checking safety properties in transition systems. PDR was developed in 2011 by Aaron Bradley.[2]

PDR proves or refutes the correctness of safety properties through the incremental construction of relatively inductive frames, which overapproximate the reachable state space within a given number of steps. If two identical adjacent frames are constructed, the specified property is an inductive invariant. Otherwise, a counterexample is provided as a sequence of transitions from the initial state to a state violating the specified property.[3]

PDR has been extended from LTL formulas in the Boolean domain to evaluate quantifier-free bit vectors,[4] software engineering,[2] and parameter synthesis.[5]

References

  1. ^ Bradley, Aaron R. (2011), "SAT-Based Model Checking without Unrolling", in Jhala, Ranjit; Schmidt, David (eds.), Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, vol. 6538, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 70–87, doi:10.1007/978-3-642-18275-4_7, ISBN 978-3-642-18274-7, retrieved 2026-03-25
  2. ^ a b Cimatti, Alessandro; Griggio, Alberto (2012), "Software Model Checking via IC3", in Madhusudan, P.; Seshia, Sanjit A. (eds.), Computer Aided Verification, vol. 7358, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 277–293, doi:10.1007/978-3-642-31424-7_23, ISBN 978-3-642-31423-0, retrieved 2026-03-25
  3. ^ Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick, eds. (2018). Handbook of Model Checking. Cham: Springer International Publishing. doi:10.1007/978-3-319-10575-8. ISBN 978-3-319-10574-1.
  4. ^ Welp, Tobias; Kuehlmann, Andreas (2013). "QF BV Model Checking with Property Directed Reachability". Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE Conference Publications: 791–796. Bibcode:2013date.conf..168W. doi:10.7873/DATE.2013.168. ISBN 978-1-4673-5071-6.{{cite journal}}: CS1 maint: periodical has ISBN (link)
  5. ^ Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano (October 2013). "Parameter synthesis with IC3". Formal Methods in Computer-Aided Design. IEEE: 165–168. Bibcode:2013fmca.conf...30C. doi:10.1109/FMCAD.2013.6679406. ISBN 978-0-9835678-3-7.{{cite journal}}: CS1 maint: periodical has ISBN (link)

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.