Submission declined on 21 July 2026 by Jerodlycett (talk). Most of the sources refer to it as IC3 not PDR. Please either choose IC3 as the name or provide more citations that its primary name is PDR.
Where to get help
How to improve a draft
You can also browse Wikipedia:Featured articles and Wikipedia:Good articles to find examples of Wikipedia's best writing on topics similar to your proposed article. Improving your odds of a speedy review To improve your odds of a faster review, tag your draft with relevant WikiProject tags using the button below. This will let reviewers know a new draft has been submitted in their area of interest. For instance, if you wrote about a female astronomer, you would want to add the Biography, Astronomy, and Women scientists tags. Editor resources
|  |
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
edit- ↑ 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
- 1 2 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
- ↑ 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.
- ↑ 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.
- ↑ 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.