Draft:Property-Directed Reachability
Model checking algorithm
From Wikipedia, the free encyclopedia
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]
 | Review waiting, please be patient.
This may take 2 months or more, since drafts are reviewed in no specific order. There are 3,789 pending submissions waiting for review.
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
Reviewer tools
|
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,[5] and parameter synthesis.[6]