CVC4

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. CVC4 is the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. A joint project of NYU and U Iowa, CVC4 aims to support the features of CVC3 and SMT-LIBv2 while optimizing the design of the core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances. CVC4 is intended to be an open and extensible SMT engine, and it can be used as a stand-alone tool or as a library, with essentially no limit on its use for research or commercial purposes (see license).


References in zbMATH (referenced in 124 articles , 1 standard article )

Showing results 1 to 20 of 124.
Sorted by year (citations)

1 2 3 ... 5 6 7 next

  1. Bavendiek, Kai; Schupp, Sibylle: A process calculus for privacy-preserving protocols in location-based service systems (2022)
  2. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  3. Backeman, Peter; Rümmer, Philipp; Zeljić, Aleksandar: Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (2021)
  4. Bozga, Marius; Iosif, Radu; Sifakis, Joseph: Checking deadlock-freedom of parametric component-based systems (2021)
  5. Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca: Universal invariant checking of parametric systems with quantifier-free SMT reasoning (2021)
  6. Claessen, Koen; Lillieström, Ann: Handling transitive relations in first-order automated reasoning (2021)
  7. Filliâtre, Jean-Christophe: Simpler proofs with decentralized invariants (2021)
  8. Garreta, Albert; Gray, Robert D.: On equations and first-order theory of one-relator monoids (2021)
  9. Hajdu, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei: Inductive benchmarks for automated reasoning (2021)
  10. Kruff, Niclas; Lüders, Christoph; Radulescu, Ovidiu; Sturm, Thomas; Walcher, Sebastian: Algorithmic reduction of biological networks with multiple time scales (2021)
  11. Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark Barrett: Pono: A Flexible and Extensible SMT-Based Model Checker (2021) not zbMATH
  12. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare: On solving quantified bit-vector constraints using invertibility conditions (2021)
  13. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare: Towards satisfiability modulo parametric bit-vectors (2021)
  14. Bansal, Kshitij; Koskinen, Eric; Tripp, Omer: Synthesizing precise and useful commutativity conditions (2020)
  15. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  16. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  17. De Angelis, Emanuele; Fioravanti, Fabio; Proietti, Maurizio: Transformational verification of Quicksort (2020)
  18. Durán, Francisco; Eker, Steven; Escobar, Santiago; Martí-Oliet, Narciso; Meseguer, José; Rubio, Rubén; Talcott, Carolyn: Programming and symbolic computation in Maude (2020)
  19. Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
  20. Jonáš, Martin; Strejček, Jan: Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions (2020)

1 2 3 ... 5 6 7 next