Pith. sign in

REVIEW 2 major objections 4 minor 37 references

Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art

T0 review · 2 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read PDR proves loops that fixed templates cannot

desk verdict Solid empirical baseline for PDR-based software verification, but the theoretical justification for the new KIPDR lifting step does not hold as written; the paper deserves a serious referee but needs major revision. read the letter →

arxiv 1908.06271 v2 pith:L2BCYVXB submitted 2019-08-17 cs.SE

Dirk Beyer , Matthias Dangl This is my paper · ORCID
classification cs.SE
keywords softwareverificationproperty-directedreachabilityIC3k-inductioninvariantgenerationCraiginterpolationcounterexampletoinductionloopinvariants
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Property-directed reachability (PDR) learns inductive invariants by turning failed induction attempts into proof obligations, and it has been highly successful on hardware. This paper asks whether that idea can work for ordinary C programs: it implements a standalone PDR verifier and KIPDR, an invariant generator that feeds PDR-style lemmas into k-induction, and evaluates both on 5,591 verification tasks plus seven hand-crafted programs. The headline finding is that KIPDR proves programs that template-based data-flow analyses cannot, by discovering invariants such as $y = z$ after a shared initialization, $|x| \bmod 4 = 0$, and $(x \& 5) = 5$ without being given a template. It also reports that on the loop-heavy benchmark subcategory, KIPDR solves fewer tasks than the best competing verifiers but uses substantially less CPU time on the tasks it does solve. A sympathetic reader would take the paper's central claim to be that PDR is a viable, sometimes faster route to exactly the class of invariants that fixed-template analyses miss.

What carries the argument

The load-bearing machinery is KIPDR, a k-induction procedure extended with a property-directed learning loop. The central operation is lift: given a concrete counterexample-to-induction state $s$, Craig interpolation between $s = s_n$ and the failed induction query produces a predicate $C$ that contains $s$ and whose every state is also a $k$-predecessor of a bad state; the negation of $C$ becomes a proof obligation. A second operation, strengthen, takes a successfully proved obligation and drops components to make it a stronger invariant before conjoining it to the internally maintained invariant. These two operations convert the standard k-induction failure--no counterexample in $k$ steps, but cannot rule out the next step--into concrete lemmas that subsequent induction checks can use.

What would settle it

Run the same KIPDR configuration with the SMT solver swapped for one whose interpolation engine returns only trivial interpolants, on the crafted tasks mod4.c and bin-suffix-5.c. If those tasks are no longer proved while the template-based configurations still time out, then the claim that PDR itself, rather than a particular solver's interpolants, computes the hard invariants is falsified.

Watch

Extended reading notes

Core claim

On its own terms, the paper's discovery is that the PDR ingredient can be transplanted into k-induction as a continuously-refined invariant generator, and that in this role it finds invariants outside the reach of the evaluated abstract domains. The algorithm KIPDR wraps k-induction in the PDR loop: when an induction-step check fails on the safety property or on a proof obligation, it takes the satisfying predecessor state, lifts it via Craig interpolation to a set of states that all lead to a bad state, negates that set to form a new proof obligation, and attempts to prove the obligation inductively. On the seven crafted tasks, this mechanism yields proofs for all seven, whereas the Boxes, equality-template, and parity-template data-flow combinations solve only four; on the 2019 loop benchmark it achieves lower median CPU time than the category winner on mutually solved tasks. The paper's stated conclusion is the strongest claim: PDR can be an effective and efficient technique for computing invariants that are difficult to obtain, including programs where the PDR-based approach is more efficient than the best invariant generator from the competition's loop subcategory.

Load-bearing premise

The practical power of KIPDR rests on the SMT solver returning a precise summary of a failed induction step; if the solver can only produce trivial summaries, the learned proof obligations become useless and the algorithm's advantage over template analyses disappears.

Editorial extensions

If this is right

  • The released standalone CTIGAR implementation outperforms the only other pure PDR verifier for C (more correct results, no wrong proofs) and is positioned as the reference baseline for future PDR-for-software work.
  • KIPDR as an auxiliary invariant generator lets k-induction prove 449 bug-free benchmark tasks that plain k-induction cannot prove.
  • On the same bug-free tasks, a data-flow invariant generator based on Boxes plus simple templates proves 1,117, so KIPDR is complementary rather than dominant.
  • On the seven crafted tasks, KIPDR proves all seven, including the three that defeat every evaluated template combination.
  • On the 208-task loop benchmark, KIPDR has lower median CPU time than the best three competitors on the tasks all solve, supporting the paper's conclusion that PDR can be both effective and efficient for hard invariants.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper shows that one solver produces no suitable interpolants for some crafted tasks while another solves all seven, which implies the practical effectiveness of KIPDR is partly a property of the SMT solver's interpolation engine rather than of the algorithm alone; a solver-robustness study would be a direct next step.
  • Because KIPDR needed no template for $|x| \bmod 4 = 0$ or $(x \& 5) = 5$, a natural extension is to test it against data-flow analyses with an open-ended template family, such as arbitrary linear congruences or low-bit masks, to find where templated approaches catch up.
  • The paper reports that KIPDR solves some Linux-driver tasks by chaining a weaker invariant into a stronger one (for example, a reference counter greater than 0, then equal to 1); this suggests the algorithm can be used as a general lemma-discovery layer, not just a final proof engine.
  • Its success on the seven crafted examples is an existence proof, not a distributional statement: on the broad benchmark set data-flow remains far more effective, so the paper's practical message is to keep a template-free PDR component as a fallback rather than a replacement.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The manuscript reports an implementation and empirical evaluation of property-directed reachability (PDR) for software verification. The authors contribute two artifacts: CPAchecker-CTIGAR, an adaptation of CTIGAR within CPAchecker, and KIPDR, an extension of k-induction that uses failed induction attempts to generate auxiliary invariants. The evaluation covers 5,591 SV-COMP 2018 tasks, a set of generated path programs, seven hand-crafted example programs, and the SV-COMP 2019 ReachSafety-Loops subcategory. The main findings are that CPAchecker-CTIGAR is a viable baseline compared with Vvt-CTIGAR, that KIPDR is less effective than data-flow-based invariant generation on the large benchmark set, and that there nevertheless exist programs (e.g., eq2.c, mod4.c, bin-suffix-5.c) for which KIPDR finds invariants that the evaluated template-based analyses cannot find, and on which KIPDR is competitive with or faster than the best SV-COMP verifiers. The paper provides a replication package and uses BenchExec for controlled measurements.

Significance. If the formal issue in Section 3 is repaired, this is a valuable contribution: it provides an open-source reference implementation, a careful experimental methodology on externally collected benchmarks, and an explicit, falsifiable existence claim about PDR's ability to generate nontrivial loop invariants. The paper is appropriately modest in its conclusions, explicitly refuting Hypotheses 2 and 3 and framing Hypothesis 4 as an existence statement. The replication package and the use of BenchExec resource control are clear strengths, as is the authors' willingness to report the number of wrong proofs and wrong alarms. The main weakness is formal: the central algorithm's lift operation is specified incorrectly, and no soundness theorem is supplied for Algorithm 1.

major comments (2)
  1. [§3, lift contract and Craig-interpolation implementation] The specification of lift is not logically coherent as written. For a CTI s there is, by construction, a model of Inv(s_n) ∧ ⋀_{i=n}^{n+k-1}(Q(s_i)∧T(s_i,s_{i+1})) ∧ ¬Q(s_{n+k}) with s = s_n, so the formula B = Inv(s_n) ∧ ... ⇒ ¬Q(s_{n+k}) is false on that model; hence A⇒B does not hold and ordinary Craig interpolation between A and B is not applicable. In addition, the displayed requirement on C has the path variables s_{n+1},...,s_{n+k} under the implicit universal quantification of the implication, so it expresses that every k-step path from a C-state reaches ¬Q, not that each C-state has some k-step path to ¬Q; the latter is what the prose claims and what a CTI generalization needs. The Table 1 example is a witness to the problem: for eq2.c with k=1 and C = y≠z, a loop-body transition from a y≠z state can stay inside the loop and keep Q true, so the displayed condition is false for C. Because lines 12-14 of Algorithm 1 justify 'return false' from a violation of a proof obligation ¬C via the premise that every state in C is a k-predecessor of ¬Q, the soundness of false answers and the theoretical invariant-generation claim are unsupported. Please repair the lift contract (e.g., with an existential quantifier over the intermediate path or with sequence interpolants), prove that the produced interpolant C is a subset of the k-predecessors of ¬Q, and state the resulting soundness property of Algorithm 1.
  2. [§3, Algorithm 1 (global correctness)] Independent of the lift contract, Algorithm 1 is presented without a soundness or termination statement. The paper's conclusion treats KIPDR as an invariant generator, but the only guarantees given are the empirically observed zero wrong proofs; the operations on Oprev/O at lines 2-3 and the eager increment of k at line 33 are heuristics that are never related to a formal invariant of the algorithm. A short theorem, or at least an explicit correctness argument, stating that every predicate added to InternalInv in line 23 is a true invariant and that 'return true' in line 32 implies P holds, would be needed for the algorithm to be usable as a verification procedure beyond the reported runs. The absence of such a statement is particularly relevant because the paper advertises KIPDR as a sound auxiliary-invariant generator.
minor comments (4)
  1. [§4.8, Table 3] The phrase 'rather the null hypothesis holds' is too strong; the evidence supports 'no substantial improvement on this benchmark set', not a statistical null hypothesis. Please reword or provide a significance test.
  2. [§4.10, Table 7 and further discussion] The paper should state explicitly whether the KI←KIPDR rows in Table 7 were obtained with MathSAT5, and whether any of the seven examples depended on solver-specific interpolation behavior; the text discusses this issue for Ultimate Automizer but not for KIPDR.
  3. [Figures 6-11] The figures omit the common header (lines 1-9) while the text refers to it; showing or explicitly referencing the header is necessary for standalone readability of the example programs.
  4. [§4.2, Hypothesis 2] Hypothesis 2 is worded as an improvement over plain k-induction, which the data (449 solved tasks vs. 0) would actually support; the experimental refutation is against data-flow-based auxiliary invariants. Please rephrase the hypothesis so that the tested claim matches the comparison actually made.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the evaluation is benchmark-driven and the central KIPDR claims are checked against external SV-COMP results; the Craig-interpolation justification of lift has a proof gap but that is a correctness issue, not a circular reduction.

full rationale

The paper's load-bearing claims are empirical: KIPDR is measured against the external SV-COMP suite, independent verifiers (Ultimate Automizer, Ultimate Taipan, VeriAbs, Skink, VIAP), and the authors' own k-induction baseline. No parameter is fitted to the target results and then reported as a prediction; the seven hand-crafted examples are existence witnesses, and Table 7 shows that external tools also solve most of them. The references to the authors' earlier k-induction work [5] provide the algorithmic framework, but the present effectiveness comparison does not reduce to those citations. The one serious defect is in Section 3: the paper claims 'We can implement lift using Craig interpolation between A : s = sn and B : Inv(sn) ∧ ... ⇒ ¬Q(sn+k), because s is a CTI, and therefore we know that A⇒B holds.' For a genuine CTI s, B(s) is false while A(s) is true, so A⇒B does not follow; if B is instead read as the path-to-¬Q formula, then A∧B is satisfiable and ordinary Craig interpolation is inapplicable. This is an omitted or incorrect soundness proof for the lift operation, and hence a correctness risk for KIPDR's auxiliary invariants, not a circularity: the algorithm's invariant-generation step is not defined in terms of the safety conclusion it is used to prove, and no fitted constant or self-citation forces the reported results. The empirical evidence of zero wrong proofs in Tables 3, 6, and 8 mitigates but does not remove this concern; the circularity score remains 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper introduces no fitted numeric constants, no ad hoc parameters in the algorithms, and no new physical or formal entities. The central empirical evaluation relies on standard background (Craig interpolation, PDR, k-induction), on the assumption that the chosen C-to-transition-system encoding is faithful, and on the correctness of the SV-COMP benchmark labels and scoring. These are reasonable domain assumptions for an empirical software-verification study, but they should be stated explicitly.

assumptions (5)
  • standard math Craig interpolation theorem: for formulas A and B with A implies B, there exists an interpolant C with A implies C and C implies B.
    Used to implement the lift function in Section 3, which turns a counterexample-to-induction state into a predicate over CTI states.
  • domain assumption The C program is faithfully encoded as a transition system with initial predicate I, transition relation T, and safety property P.
    All algorithms and experiments in Sections 2 to 4 operate on this encoding, following the notation introduced at the start of Section 2.
  • domain assumption The SV-COMP benchmark tasks and their safe/unsafe labels are correct.
    The scoring in Section 4.6 and all effectiveness claims in Tables 2 to 8 depend on the correctness of these labels.
  • domain assumption The SMT solver MathSAT5 produces sound and sufficiently useful interpolants for KIPDR and CTIGAR.
    Section 3 relies on interpolation for lift, and Section 4.10 notes that MathSAT5 does not generate suitable interpolants for some examples, so this is a load-bearing tooling assumption.
  • domain assumption The SV-COMP scoring schema is a meaningful quality measure for comparing verifiers.
    Sections 4.6 and 4.11 use the community score to rank configurations, which weights proofs, alarms, and incorrect results in a specific way.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art." pith.science (2026). https://pith.science/paper/L2BCYVXB

@misc{pith2026190806271,
  author       = {Pith},
  title        = {Pith review of: Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/L2BCYVXB}},
  note         = {Machine review of arXiv:1908.06271}
}
read the original abstract

Property-directed reachability (PDR) is a SAT/SMT-based reachability algorithm that incrementally constructs inductive invariants. After it was successfully applied to hardware model checking, several adaptations to software model checking have been proposed. We contribute a replicable and thorough comparative evaluation of the state of the art: We (1) implemented a standalone PDR algorithm and, as improvement, a PDR-based auxiliary-invariant generator for k-induction, and (2) performed an experimental study on the largest publicly available benchmark set of C verification tasks, in which we explore the effectiveness and efficiency of software verification with PDR. The main contribution of our work is to establish a reproducible baseline for ongoing research in the area by providing a well-engineered reference implementation and an experimental evaluation of the existing techniques.

Figures

Figures reproduced from arXiv: 1908.06271 by the authors.

Figure 1
Figure 1. Example C program eq2.c loop, y and z are (still) equal to each other. Since y and z are equal before the loop, and are always incremented together within the loop, the invariant y = z is inductive. However, since there is no direct connection between y and z but only an indirect one via their shared dependency on w, naïve data-flow-based techniques may fail to find this invariant. In fact, we tried several configur… view at source ↗
Figure 2
Figure 2. Consecution check makes sure to only conjoin to frame [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. If phase 1 results in a proof obligation [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Quantile plot for accumulated number of solved tasks [PITH_FULL_IMAGE:figures/full_fig_p021_4.png]
Figure 5
Figure 5. Figure 5: Quantile plot of accumulated number of bug-free task [PITH_FULL_IMAGE:figures/full_fig_p023_5.png]
Figure 6
Figure 6. Figure 6: Program const.c 9 int main(void) { 10 unsigned int w = __VERIFIER_nondet_uint(); 11 unsigned int x = w; 12 unsigned int y = __VERIFIER_nondet_uint(); 13 unsigned int z = y; 14 while (__VERIFIER_nondet_uint()) { 15 if (__VERIFIER_nondet_uint()) { 16 ++w; ++x; 17 } else …
Figure 7
Figure 7. Figure 7: Program eq1.c are the same as in [PITH_FULL_IMAGE:figures/full_fig_p026_7.png]
Figure 8
Figure 8. Figure 8: Program even.c 9 int main(void) { 10 unsigned int x = 1; 11 while (__VERIFIER_nondet_int()) { 12 x += 2; 13 } 14 __VERIFIER_assert(x % 2); 15 return 0; 16 } [PITH_FULL_IMAGE:figures/full_fig_p027_8.png]
Figure 9
Figure 9. Figure 9: Program odd.c shown in [PITH_FULL_IMAGE:figures/full_fig_p027_9.png]
Figure 10
Figure 10. Figure 10: Program mod4.c 9 int main(void) { 10 unsigned int x = 5; 11 while (__VERIFIER_nondet_int()) { 12 x += 8; 13 } 14 __VERIFIER_assert((x & 5) == 5); 15 return 0; 16 } [PITH_FULL_IMAGE:figures/full_fig_p028_10.png]
Figure 11
Figure 11. Figure 11: Program bin-suffix-5.c approach that we created for the study in this paper. Those verifiers are, in alphabetical order, Skink, Ultimate Automizer, Ultimate Kojak, Ultimate Taipan, VeriAbs, and VIAP. Please note that the results of those six verifiers were obtained in…
Figure 12
Figure 12. Figure 12: Quantile plot for accumulated score of solved tasks [PITH_FULL_IMAGE:figures/full_fig_p030_12.png]
Figure 13
Figure 13. Figure 13: Scatter plot comparing the CPU times spent on tasks b [PITH_FULL_IMAGE:figures/full_fig_p031_13.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

37 extracted references · 18 canonical work pages

  1. [1]

    In: Proc

    Ball, T., Podelski, A., Rajamani, S.K.: Boolean and carte sian abstraction for model checking C programs. In: Proc. TACAS. pp. 268–283. LNCS 2031 , Springer (2001). https://doi.org/10.1007/3-540-45319-9_19

    doi:10.1007/3-540-45319-9_19 2001

  2. [2]

    In: Proc

    Ball, T., Rajamani, S.K.: The Slam project: Debugging system soft- ware via static analysis. In: Proc. POPL. pp. 1–3. ACM (2002) . https://doi.org/10.1145/503272.503274

    arXiv 2002

  3. [3]

    IEEE Intelligent Systems 29(1), 20–29 (2014)

    Beckert, B., Hähnle, R.: Reasoning and verification: Stat e of the art and current trends. IEEE Intelligent Systems 29(1), 20–29 (2014). https://doi.org/10.1109/MIS.2014.3

    work page doi:10.1109/mis.2014.3 2014

  4. [4]

    In: Proc

    Beyer, D.: Software verification with validation of resul ts (Report on SV- COMP 2017). In: Proc. TACAS. pp. 331–349. LNCS 10206, Spring er (2017). https://doi.org/10.1007/978-3-662-54580-5_20

    work page doi:10.1007/978-3-662-54580-5_20 2017

  5. [5]

    In: Proc

    Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction w ith continuously- refined invariants. In: Proc. CA V. pp. 622–640. LNCS 9206, Sp ringer (2015). https://doi.org/10.1007/978-3-319-21690-4_42

    work page doi:10.1007/978-3-319-21690-4_42 2015

  6. [6]

    Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-b ased software verification. J. Autom. Reasoning 60(3), 299–335 (2018). https://doi.org/10.1007/s10817-017-9432-6

    doi:10.1007/s10817-017-9432-6 2018

  7. [7]

    In: Proc

    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A .: Path invariants. In: Proc. PLDI. pp. 300–309. ACM (2007). https://doi.org/10.1145/1250734.1250769

    arXiv 2007

  8. [8]

    In: Proc

    Beyer, D., Keremoglu, M.E.: CP Achecker: A tool for configurable soft- ware verification. In: Proc. CA V. pp. 184–190. LNCS 6806, Spr inger (2011). https://doi.org/10.1007/978-3-642-22110-1_16

    doi:10.1007/978-3-642-22110-1_16 2011

Show all 37 references
  1. [9]

    Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1–29 (2019). https://doi.org/10.1007/s10009-017-0469-y

    2019 doi

  2. [10]

    Zenodo (2019)

    Beyer, D., Dangl, M.: Replication package for article ‘S oftware verification with PDR: Implementation and empirical evaluation of the state o f the art’. Zenodo (2019). https://doi.org/10.5281/zenodo.3370037

    2019 doi

  3. [11]

    In: Proc

    Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic m odel checking with- out BDDs. In: Proc. TACAS. pp. 193–207. LNCS 1579, Springer ( 1999). https://doi.org/10.1007/3-540-49059-0_14

    1999 doi

  4. [12]

    In: Proc

    Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Count erexample to induction- guided abstraction-refinement (CTIGAR). In: Proc. CA V. pp. 831–848. LNCS 8559, Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_55

    2014 doi

  5. [13]

    In: Proc

    Bradley, A.R.: SAT-based model checking without unroll ing. In: Proc. VMCAI. pp. 70–87. LNCS 6538, Springer (2011). https://doi.org/10.1007/978-3-642-18275-4_7

    2011 doi

  6. [14]

    Formal Asp

    Bradley, A.R., Manna, Z.: Property-directed increment al invari- ant generation. Formal Asp. Comput. 20(4-5), 379–405 (2008). https://doi.org/10.1007/s00165-008-0080-9

    2008 doi

  7. [15]

    In: Proc

    Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooi meijer, P., Luca, M., O’Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodrig uez, D.: Moving fast with software verification. In: Proc. NFM. pp. 3–11. LNCS 905 8, Springer (2015). https://doi.org/10.1007/978-3-319-17524-9_1

    2015 doi

  8. [16]

    In: Proc

    Cimatti, A., Griggio, A.: Software model checking via IC 3. In: Proc. CA V. pp. 277–

  9. [17]

    FMSD 49(3), 190–218 (2016)

    Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinit e-state invariant checking with IC3 and predicate abstraction. FMSD 49(3), 190–218 (2016). https://doi.org/10.1007/s10703-016-0257-4

    2016 doi

  10. [18]

    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Co unterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003). https://doi.org/10.1145/876638.876643

    2003

  11. [19]

    A new form of the Herbrand-G entzen theorem

    Craig, W.: Linear reasoning. A new form of the Herbrand-G entzen theorem. J. Symb. Log. 22(3), 250–268 (1957). https://doi.org/10.2307/2963593

    1957 doi

  12. [20]

    In: Proc

    Graf, S., Saïdi, H.: Construction of abstract state grap hs with Pvs. In: Proc. CA V. pp. 72–83. LNCS 1254, Springer (1997). https://doi.org/10.1007/3-540-63166-6_10

    1997 doi

  13. [21]

    In: Pro c

    Günther, H., Laarman, A., Weissenbacher, G.: Vienna Ver ification Tool: IC3 for parallel software (competition contribution). In: Pro c. TACAS. pp. 954–957. LNCS 9636, Springer (2016)

    2016

  14. [22]

    In: Proc

    Gurfinkel, A., Chaki, S.: Boxes: A symbolic abstract doma in of boxes. In: Proc. SAS. pp. 287–303 (2010). https://doi.org/10.1007/978-3-642-15769-1_18

    2010 doi

  15. [23]

    In: Proc

    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verifi- cation framework. In: Proc. CA V. pp. 343–361. LNCS 9206, Spr inger (2015). https://doi.org/10.1007/978-3-319-21690-4_20

    2015 doi

  16. [24]

    In: Proc

    Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: A framew ork for verifying C pro- grams (competition contribution). In: Proc. TACAS. pp. 447 –450. LNCS 9035, Springer (2015). https://doi.org/10.1007/978-3-662-46681-0_41

    2015 doi

  17. [25]

    In: Proc

    Heizmann, M., Hoenicke, J., Podelski, A.: Software mode l checking for people who love automata. In: Proc. CA V. pp. 36–52. LNCS 8044, Sprin ger (2013). https://doi.org/10.1007/978-3-642-39799-8_2

    2013 doi

  18. [26]

    ACM Co mputing Surveys 41(4) (2009)

    Jhala, R., Majumdar, R.: Software model checking. ACM Co mputing Surveys 41(4) (2009). https://doi.org/10.1145/1592434.1592438

    2009

  19. [27]

    In: Proc

    Jovanovic, D., Dutertre, B.: Property-directed k-indu ction. In: Proc. FMCAD. pp. 85–92. IEEE (2016). https://doi.org/10.1109/FMCAD.2016.7886665

    2016

  20. [28]

    In: Proc

    Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In: Proc. Int. Workshop on Parallel and Distributed Methods in V erification. pp. 55–

  21. [29]

    In: Proc

    Khoroshilov, A.V., Mutilin, V.S., Petrenko, A.K., Zakh arov, V.: Establishing Linux driver verification process. In: Proc. Ershov Memorial Conf erence. pp. 165–176. LNCS 5947, Springer (2009). https://doi.org/10.1007/978-3-642-11486-1_14

    2009 doi

  22. [30]

    In: Proc

    Lange, T., Prinz, F., Neuhäußer, M.R., Noll, T., Katoen, J.: Improving generaliza- tion in software IC3. In: Proc. SPIN’18. pp. 85–102. LNCS 108 69, Springer (2018). https://doi.org/10.1007/978-3-319-94111-0_5

    2018 doi

  23. [31]

    In: Proc

    Lange, T., Neuhäußer, M.R., Noll, T.: IC3 software model checking on control flow automata. In: Proc. FMCAD. pp. 97–104 (2015)

    2015

  24. [32]

    In: Proc

    McMillan, K.L.: Interpolation and SAT-based model chec king. In: Proc. CA V. pp. 1–13. LNCS 2725, Springer (2003). https://doi.org/10.1007/978-3-540-45069-6_1

    2003 doi

  25. [33]

    Wiley Publish- ing, 3rd edn

    Myers, G.J., Sandler, C., Badgett, T.: The Art of Softwar e Testing. Wiley Publish- ing, 3rd edn. (2011)

    2011

  26. [34]

    Wahl, T.: The k-induction principle (2013), available a t http://www.ccs.neu.edu/home/wahl/Publications/k-induction.pdf

    2013

  27. [35]

    PhD Thesis, University of Pas- sau, Software Systems Lab (2017)

    Wendler, P.: Towards practical predicate analysis. PhD Thesis, University of Pas- sau, Software Systems Lab (2017)

    2017

  28. [62]

    https://doi.org/10.4204/EPTCS.72

    EPTCS 72 (2011). https://doi.org/10.4204/EPTCS.72

    2011 doi

  29. [293]

    https://doi.org/10.1007/978-3-642-31424-7_23

    LNCS 7358, Springer (2012). https://doi.org/10.1007/978-3-642-31424-7_23

    2012 doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.