Pith. sign in

REVIEW 3 major objections 5 minor 30 references

Revisiting DRUP-based Interpolants with CaDiCaL 2.0

T0 review · 3 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

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

Pith's one-line read This paper claims that DRUP-based interpolants can be generated in CaDiCaL 2.0 via its Tracer API without modifying the solver, and that doing so improves the performance of the model checker Avy on hardware verification benchmarks.

desk verdict A genuinely useful engineering contribution--DRUP interpolation on CaDiCaL's Tracer API--whose soundness rests on an unverified DRAT-as-DRUP assumption that a referee should push on. read the letter →

arxiv 2501.02608 v2 pith:GTSECBIY submitted 2025-01-05 cs.LO

Basel Khouri , Yakir Vizel This is my paper · ORCID
classification cs.LO
keywords DRUPproofsCraiginterpolationCaDiLSAT-basedmodelcheckingAvyprooftrimmingminimizationTracerAPI
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

The paper claims that DRUP-based interpolants can be generated inside CaDiCaL 2.0 using its new Tracer API, with no changes to the SAT solver itself, and that this implementation, called Drup2Itp, improves the performance of the interpolation-based model checker Avy. On the HWMCC'19 and HWMCC'20 benchmark suites, Avy with CaDiCaL and Drup2Itp solves more instances and runs faster on average than Avy with Glucose as its solver. The work matters because interpolants are a key ingredient in SAT-based model checking, and CaDiCaL is one of the strongest available SAT solvers, so bringing interpolation to it broadens the toolkit for verification tools. A secondary claim is that proof minimization, which re-solves only the core of the proof before computing an interpolant, substantially shrinks both proof size and interpolant computation time in incremental settings.

What carries the argument

The load-bearing mechanism is the DRUP proof stack maintained by Drup2Itp, together with its trim()/replay() two-phase procedure. trim() walks the proof backwards, revives deleted clauses, and marks as core every clause that is needed to re-derive the empty clause by reverse unit propagation; replay() walks the core forward, re-derives each core clause by chain resolution, and feeds the resolution steps to a ResolutionProofIterator that computes interpolants on the fly. Proof minimization is carried by the Minimizer class, which collects the original core clauses, solves them with a fresh CaDiCaL instance, and computes the interpolant from the minimized proof. The Tracer API is what makes this possible without modifying the solver: it provides callbacks for clause addition and deletion, and Drup2Itp uses clause identifiers to keep its database synchronized with CaDiCaL's.

What would settle it

Take a sample of UNSAT formula pairs from the HWMCC benchmarks, compute Drup2Itp's interpolant, and check the Craig interpolant conditions: that the interpolant is implied by the A-side, contradicts the B-side, and uses only common variables; a single violation would falsify the implementation's correctness and, with it, the performance claim's foundation.

Watch

Extended reading notes

Core claim

The central discovery is an architecture in which an external class, Drup2Itp, plugs into CaDiCaL 2.0's Tracer API and maintains its own DRUP proof, clause database, unit-propagation engine, and conflict analysis. When the solver derives the empty clause, Drup2Itp trims the proof by marking the clauses that actually participate in the derivation of the empty clause, then replays the trimmed proof forward and reports resolution steps to an interpolation routine through a ResolutionProofIterator. The paper reports that when this machinery is integrated into Avy, the resulting configuration outperforms the existing Avy with Glucose in both runtime and number of solved instances on the HWMCC benchmarks, and that the optional Minimizer component further improves interpolant computation time and reduces interpolant size in incremental solving.

Load-bearing premise

The performance claim rests on a single comparison between Avy-with-CaDiCaL/Drup2Itp and Avy-with-Glucose on the HWMCC benchmarks, and on the unstated assumption that Drup2Itp's interpolants are correct, since no explicit correctness validation of the interpolants is reported.

Editorial extensions

If this is right

  • CaDiCaL becomes usable in any interpolation-based verification workflow, not just Avy, since Drup2Itp is solver-decoupled.
  • Proof minimization via Minimizer reduces both the replayed proof size and the resulting interpolant size in most incremental cases, which can speed up iterative model-checking loops.
  • The decoupling means future CaDiCaL releases can be supported without modifying solver internals, as long as the Tracer API remains stable.
  • The virtual-best score across CaDiCaL configurations exceeds any single configuration, suggesting that instance-specific configuration tuning could yield further gains.
  • The same trimming and replay machinery can be reused for unsat core extraction, which benefits abstraction-refinement and counterexample-guided refinement.

Reading between the lines

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

  • The reported gain may partly reflect CaDiCaL's raw solver strength rather than the DRUP interpolation method itself, since the comparison is against Glucose as a different solver; a controlled comparison would isolate the interpolation machinery.
  • The same Tracer-API design could be extended to DRAT and LRAT proofs with minimal new engineering, which would let interpolation coexist with proof-of-unsatisfiability certification.
  • Color-ordered propagation, which the paper mentions only as a heuristic for producing CNF-friendly interpolants, could be studied as a tunable parameter for interpolant quality in other model checkers.
  • The minimization step re-solves a core subset; on harder benchmarks where the core is not much smaller than the original, the overhead of an extra solve could outweigh the benefit, so the gain may be benchmark-dependent.
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

3 major / 5 minor

Summary. The paper presents Drup2Itp, an implementation of DRUP-based interpolant generation for the SAT solver CaDiCaL, built on CaDiCaL 2.0's Tracer API so that the SAT solver itself is not modified. The implementation is integrated into the bit-level model checker Avy, optionally with a proof-minimization step (Minimizer), and evaluated on the HWMCC'19 and HWMCC'20 benchmark sets against Avy with Glucose as the baseline. The paper reports aggregate runtime and solved-instance counts, and claims that the CaDiCaL/Drup2Itp configuration—especially with proof minimization—outperforms the Glucose-based vanilla Avy.

Significance. If the implementation is sound, the paper makes a useful engineering contribution: it brings a state-of-the-art SAT solver into interpolation-based model checking through a decoupled, maintainable proof-tracer interface, and it provides a public implementation that can be reused by the community. The use of the Tracer API and the independent proof database is a genuine architectural improvement over modifying the solver internals, and the evaluation over two HWMCC benchmark sets is a meaningful real-world test. However, the central performance claim rests on two load-bearing assumptions that are not substantiated in the manuscript: that CaDiCaL's emitted proofs can safely be treated as DRUP proofs, and that the interpolants handed to Avy are semantically correct. The experimental evidence is also thinner than the abstract suggests: the headline claim is only supported by the Minimizer configuration, and the reported differences in solved instances are small.

major comments (3)
  1. [Section 4, paragraph 1] The statement 'in the latest version available at the time of writing (2.1.2), CaDiCaL does not actually produce RAT clauses, so we can safely treat the emitted proof as a DRUP proof' is load-bearing for the entire paper. The correctness of the trim() and replay() procedures described in Section 3.1 depends on every logged clause having the RUP property: if any proof step is RAT but not RUP, the chain derivation constructed by Drup2Itp need not be a valid resolution derivation, and the interpolant computation is unsupported. No evidence is given for this claim, such as instrumentation showing that no RAT clauses occur, a version-specific check, or a proof-format validation on the benchmark instances. This must be addressed by either verifying the RUP property of every replayed step, disabling all RAT-producing techniques and arguing that the emitted proof is then DRUP, or adding explicit DRAT support.
  2. [Section 4.1 and Algorithms 2-3] The paper reports no direct validation that the interpolants produced by Drup2Itp satisfy the Craig conditions (A |= I and I |= ¬B) or even that they are well-formed formulas over the common variables. Since Table 1 only reports solved-instance counts and runtimes, an unsound interpolation path could produce spurious answers and faster solves without being detected. This is especially important because Avy relies on sequence interpolants for correctness. The authors should validate interpolants on a sample of the benchmark runs—for example, by checking A ∧ ¬I and I ∧ B with a SAT solver—or otherwise demonstrate that Avy's answers agree with known HWMCC statuses where available.
  3. [Section 4.1, Table 1] The abstract and Section 1 claim that integrating CaDiCaL with DRUP-based interpolants into Avy gives better performance than Avy with Glucose 'both in runtime and number of solved instances.' Table 1 does not support this claim for the plain CaDiCaL configuration: on HWMCC'19 it solves 203 instances versus Glucose's 205 and has a higher average runtime (1504.6 s versus 1447.5 s). The claim is only defensible for the Minimizer configuration (206 versus 205 on HWMCC'19, and 206 versus 201 on HWMCC'20). The paper should restrict its headline claim accordingly and provide per-instance comparison data or a statistical argument, since the total solved-instance differences are small and the average runtimes are influenced by many timeout-dominated values.
minor comments (5)
  1. [Section 1, paragraph 2] There is a typo in 'unsatisifiable instance'; it should be 'unsatisfiable instance.'
  2. [Section 4, paragraph 1] The phrase 'to ensure a a DRUP proof is emitted' contains a duplicated article and should read 'to ensure a DRUP proof is emitted.'
  3. [Figure 6 captions] Several figure captions read 'HMWCC' instead of 'HWMCC'; these should be corrected for consistency.
  4. [Reference [13]] The title of the cited paper by Gurfinkel and Vizel is rendered as 'Druping for interpolates'; the actual title is 'Druping for Interpolants.'
  5. [Figure 4 caption] The phrase 'under the diagonal of parity' is unclear; it should be 'below the diagonal' or 'below the diagonal of equality.'

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the paper reports an external benchmark comparison and builds on prior independent algorithms; the flagged limitations are soundness and selection risks, not circular steps.

full rationale

The central claim (Section 4.1, Table 1) is an empirical performance comparison of Avy with CaDiCaL/Drup2Itp against Avy with Glucose on the external HWMCC'19 and HWMCC'20 benchmark suites. Solved-instance counts and runtimes are not derived from the paper's inputs by construction; they are observations from executing the tools on independent benchmarks. The interpolation procedure is imported from prior work, [13] (Gurfinkel and Vizel, FMCAD 2014), and its correctness rests on the standard RUP property of DRUP proofs, supported by external results such as Lemma 1 from [2]. Self-citations to [13,17,23,24,25] point to the algorithm and model checker that the paper builds on; none is invoked to forbid alternatives or to establish the new implementation's performance claim, so they are not load-bearing circularity. The manuscript itself flags its main assumption in Section 4: 'By default, CaDiCaL emits a DRAT proof. However, in the latest version available at the time of writing (2.1.2), CaDiCaL does not actually produce RAT clauses, so we can safely treat the emitted proof as a DRUP proof.' This is an unverified soundness assumption and a correctness risk, but it is not circular: the performance conclusion is not defined in terms of that assumption. The paper also notes in Section 4.1 that the reported Minimizer configuration 'yields the best results for Avy with respect to the benchmark set we used,' which indicates configuration selection on the same test set; this is a statistical selection concern, not a derivation that reduces to its own inputs. No equation or parameter is fitted and then renamed as a prediction, and no self-citation chain forces the reported results. Therefore, no circular step is identified and the circularity score is 0.

Assumptions & free parameters 2 free parameters · 3 assumptions · 0 invented entities

The paper is an engineering implementation that relies on standard SAT solving, DRUP proofs, and interpolation theory. It does not introduce new logical entities or fitted physics-like parameters. The main dependencies are software assumptions (Tracer API faithfulness, DRAT-as-DRUP) and the empirical configuration choice.

free parameters (2)
  • Minimizer enabled/disabled configuration = Minimizer enabled with pre/in-processing enabled
    The best configuration is chosen empirically based on benchmark results (Section 4.1), and the paper notes disabling pre/in-processing in Minimizer yields smaller proofs but slightly worse overall runtime. This is a configuration choice fitted to the benchmark set.
  • Avy configuration = Same Avy switches across all SAT solver configurations
    The Avy settings are fixed, but the specific choice of these settings (e.g., PDR parameters, interpolation system) is not derived from first principles and affects the comparison.
assumptions (3)
  • domain assumption CaDiCaL's default DRAT proof can be treated as a DRUP proof because CaDiCaL 2.1.2 does not produce RAT clauses.
    Stated in Section 4. The correctness of the DRUP-based interpolation relies on this. The paper explicitly flags this as a caveat and asks users to disable RAT-producing features in future releases.
  • domain assumption The DRUP proof logged by Drup2Itp via the Tracer API is a faithful account of the clauses the solver actually uses.
    The correctness of trimming and replaying relies on the Tracer API providing complete and accurate notifications of clause additions and deletions (Section 3.1).
  • domain assumption The interpolant produced by the chosen interpolation system through ResolutionProofIterator is correct.
    The paper explicitly says interpolation procedures can be implemented via ResolutionProofIterator and does not go into details. The correctness of the model checking results depends on the interpolants satisfying the Craig interpolation conditions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Revisiting DRUP-based Interpolants with CaDiCaL 2.0." pith.science (2026). https://pith.science/paper/GTSECBIY

@misc{pith2026250102608,
  author       = {Pith},
  title        = {Pith review of: Revisiting DRUP-based Interpolants with CaDiCaL 2.0},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GTSECBIY}},
  note         = {Machine review of arXiv:2501.02608}
}
read the original abstract

We present our implementation of DRUP-based interpolants in CaDiCaL 2.0, and evaluate performance in the bit-level model checker Avy using the Hardware Model Checking Competition benchmarks. CaDiCaL is a state-of-the-art, open-source SAT solver known for its efficiency and flexibility. In its latest release, version 2.0, CaDiCaL introduces a new proof tracer API. This paper presents a tool that leverages this API to implement the DRUP-based algorithm for generating interpolants. By integrating this algorithm into CaDiCaL, we enable its use in model-checking workflows that require interpolants. Our experimental evaluation shows that integrating CaDiCaL with DRUP-based interpolants in Avy results in better performance (both runtime and number of solved instances) when compared to Avy with Glucose as the main SAT solver. Our implementation is publicly available and can be used by the formal methods community to further develop interpolation-based algorithms using the state-of-the-art SAT solver CaDiCaL. Since our implementation uses the Tracer API, it should be maintainable and applicable to future releases of CaDiCaL.

Figures

Figures reproduced from arXiv: 2501.02608 by the authors.

Figure 1
Figure 1. The Drup2Itp class [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Clause object. As in the original algorithm presented in [13], in order to support sequence interpolants clauses of the input formula are assigned different colors, with each original clause assigned a specific color. The Range class corresponds to the pair (κ↓, κ↑), hence, for original clauses, the range of a clause object (see [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Proof iterator In order to support interpolants, clauses in Drup2Itp are marked with colors (Definition 2). The color of clauses and variables determine the way in which interpolants are constructed and depend on the interpolation method of choice. This is beyond the scope of this paper and we refrain from discussing these de￾tails. Yet, different interpolation procedures can be implemented using different implement… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Comparing performance with and without Minimizer. sequence interpolants at every bound. Specifically, for each bound k, both vari￾ants unroll the model to depth k, solve a BMC(k) instance and compute a sequence interpolant. Consequently, at every bound k, both variants…
Figure 5
Figure 5. Figure 5: Proof size comparison while disabling pre-/in-processing during minimiza [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]
Figure 6
Figure 6. Figure 6: Proof size, interpolant size, and interpolant computation time comparison. [PITH_FULL_IMAGE:figures/full_fig_p017_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 18 canonical work pages

  1. [1]

    In: Boutilier, C

    Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009. pp. 399–404 (2009), http://ijcai.org/Proceedings/09/Papers/074.pdf

    work page 2009

  2. [2]

    Towards Understanding and Harnessing the Potential of Clause Learning

    Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. CoRR abs/1107.0044 (2011), http://arxiv. org/abs/1107.0044

    work page Pith review arXiv 2011

  3. [3]

    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003). https://doi.org/10.1016/ S0065-2458(03)58003-2 , https://doi.org/10.1016/S0065-2458(03)58003-2

    doi:10.1016/s0065-2458(03)58003-2 2003

  4. [4]

    In: Gurfinkel, A., Ganesh, V

    Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: Cadical 2.0. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CA V 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133–

    work page 2024

  5. [5]

    In: Jhala, R., Schmidt, D.A

    Bradley, A.R.: Sat-based model checking without unrolling. In: Jhala, R., Schmidt, D.A. (eds.) Verification, Model Checking, and Abstract Interpretation - 12th In- ternational Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6538, pp. 70–87. Springer (2011). https://doi.org/10.1007/978-3-64...

    doi:10.1007/978-3-642-18275-4_7 2011

  6. [6]

    In: Biere, A., Nahir, A., Vos, T.E.J

    Chockler, H., Ivrii, A., Matsliah, A.: Computing interpolants without proofs. In: Biere, A., Nahir, A., Vos, T.E.J. (eds.) Hardware and Software: Verifica- tion and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers. Lecture Notes in Com- puter Science, vol. 7857, pp. 72–85. Spri...

    work page doi:10.1007/978-3-642-39611-3_12 2012

  7. [7]

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

    work page arXiv 2003

  8. [8]

    In: de Moura, L

    Cruz-Filipe, L., Heule, M.J.H., Jr., W.A.H., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) Automated De- duction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 220–236. Springer (2017). ...

    doi:10.1007/978-3-319-63046-5_14 2017

Show all 30 references
  1. [9]

    In: Barthe, G., Hermenegildo, M.V

    D’Silva, V.V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M.V. (eds.) Verification, Model Check- ing, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceeding...

    2010 doi

  2. [10]

    In: Bjesse, P., Slobodov´ a, A

    E´ en, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Bjesse, P., Slobodov´ a, A. (eds.) International Confer- ence on Formal Methods in Computer-Aided Design, FMCAD ’11, Austin, TX, USA, October 30 - November 02, 2011. pp. 1...

    2011

  3. [11]

    In: Giunchiglia, E., Tacchella, A

    E´ en, N., S¨ orensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Confer- ence, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Pa- pers. Lecture Notes i...

    2003 doi

  4. [12]

    In: 2003 Design, Automation and Test in Europe Conference and Exhibition

    Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for cnf formulas. In: 2003 Design, Automation and Test in Europe Conference and Exhibition. pp. 886–891 (2003). https://doi.org/10.1109/DATE.2003.1253718

    2003 arXiv

  5. [13]

    In: Formal Methods in Computer- Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014

    Gurfinkel, A., Vizel, Y.: Druping for interpolates. In: Formal Methods in Computer- Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. pp. 99–106. IEEE (2014). https://doi.org/10.1109/FMCAD.2014.6987601, https:// doi.org/10.1109/FMCAD.2014.6987601

    2014

  6. [14]

    In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013

    Heule, M., Jr., W.A.H., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp. 181–188. IEEE (2013), https://ieeexplore.ieee.org/ document/6679408/

    2013

  7. [15]

    CoRR abs/1610.06229 (2016), http://arxiv.org/abs/1610.06229

    Heule, M.J.H.: The DRAT format and drat-trim checker. CoRR abs/1610.06229 (2016), http://arxiv.org/abs/1610.06229

    2016 arXiv

  8. [16]

    Kraj ´ ıcek, J.: Interpolation theorems, lower bounds for proof systems, and inde- pendence results for bounded arithmetic. J. Symb. Log. 62(2), 457–486 (1997). https://doi.org/10.2307/2275541, https://doi.org/10.2307/2275541

    1997 doi

  9. [17]

    In: Dillig, I., Tasiran, S

    Krishnan, H.G.V., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong in- duction. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st In- ternational Conference, CA V 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. Lecture Notes ...

    2019

  10. [18]

    In: Biere, A., Heule, M., van Maaren, H., Walsh, T

    Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Hand- book of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131–153. IOS Press (February 20...

    2009

  11. [19]

    In: Jr., W.A.H., Somenzi, F

    McMillan, K.L.: Interpolation and sat-based model checking. In: Jr., W.A.H., Somenzi, F. (eds.) Computer Aided Verification, 15th International Conference, CA V 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2725, pp. 1–13. Spring...

    2003 doi

  12. [20]

    In: Proceedings of the 15th International Conference on Computer Aided Verification (CA V)

    McMillan, K.L.: Interpolation and sat-based model checking. In: Proceedings of the 15th International Conference on Computer Aided Verification (CA V). pp. 1–13. Springer (2003)

    2003

  13. [21]

    In: Garavel, H., Hatcliff, J

    McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory a...

    2003

  14. [22]

    The Journal of Symbolic Logic 62(3), 981–998 (1997), http://www

    Pudl´ ak, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic 62(3), 981–998 (1997), http://www. jstor.org/stable/2275583 20 Basel Khouri and Yakir Vizel

    1997

  15. [23]

    In: Pro- ceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA

    Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Pro- ceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA. pp. 1–8. IEEE (2009). https://doi.org/10.1109/FMCAD.2009.535...

    2009

  16. [24]

    In: Biere, A., Bloem, R

    Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CA V 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Aus- tria, July 18-22, 2014. Proceeding...

    2014 doi

  17. [25]

    In: Kroening, D., Pasareanu, C.S

    Vizel, Y., Gurfinkel, A., Malik, S.: Fast interpolating BMC. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Confer- ence, CA V 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol...

    2015 doi

  18. [26]

    In: Sharygina, N., Veith, H

    Vizel, Y., Ryvchin, V., Nadel, A.: Efficient generation of small interpolants in CNF. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th Interna- tional Conference, CA V 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceed- ings. Lecture Notes in Compu...

    2013 doi

  19. [27]

    In: Sinz, C., Egly, U

    Wetzler, N., Heule, M., Jr., W.A.H.: Drat-trim: Efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) Theory and Applica- tions of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of L...

    2014

  20. [152]

    https://doi.org/10.1007/978-3-031-65627-9_7 , https: //doi.org/10.1007/978-3-031-65627-9_7

    Springer (2024). https://doi.org/10.1007/978-3-031-65627-9_7 , https: //doi.org/10.1007/978-3-031-65627-9_7

    2024 doi

  21. [385]

    https://doi.org/10.1007/978-3-030-25543-5_21 , https: //doi.org/10.1007/978-3-030-25543-5_21

    Springer (2019). https://doi.org/10.1007/978-3-030-25543-5_21 , https: //doi.org/10.1007/978-3-030-25543-5_21

    2019 doi

  22. [429]

    https://doi.org/10.1007/978-3-319-09284-3_31 , https: //doi.org/10.1007/978-3-319-09284-3_31

    Springer (2014). https://doi.org/10.1007/978-3-319-09284-3_31 , https: //doi.org/10.1007/978-3-319-09284-3_31

    2014 doi

Pith tools

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