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 57 articles , 1 standard article )

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

1 2 3 next

  1. Bromberger, Martin; Weidenbach, Christoph: New techniques for linear arithmetic: cubes and equalities (2017)
  2. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  3. Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh: Symbolic trajectory evaluation for word-level verification: theory and implementation (2017)
  4. Chen, Li; Lyu, Yinrun; Wang, Chong; Wu, Jingzheng; Zhang, Changyou; Min-Allah, Nasro; Alhiyafi, Jamal; Wang, Yongji: Solving linear optimization over arithmetic constraint formula (2017)
  5. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  6. Demri, Stéphane; Galmiche, Didier; Larchey-Wendling, Dominique; Méry, Daniel: Separation logic with one quantified variable (2017)
  7. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  8. Johansson, Moa: Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (2017)
  9. Jovanović, Dejan: Solving nonlinear integer arithmetic with MCSAT (2017)
  10. Kovács, Laura; Robillard, Simon; Voronkov, Andrei: Coming to terms with quantified reasoning (2017)
  11. Nguy^en, Phúc C.; Tobin-Hochstadt, Sam; Van Horn, David: Higher order symbolic execution for contract verification and refutation (2017)
  12. Niemetz, Aina; Preiner, Mathias; Biere, Armin: Propagation based local search for bit-precise reasoning (2017)
  13. Nightingale, Peter; Akgün, Özgür; Gent, Ian P.; Jefferson, Christopher; Miguel, Ian; Spracklen, Patrick: Automatically improving constraint models in Savile row (2017)
  14. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
  15. Reynolds, Andrew; Iosif, Radu; Serban, Cristina: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic (2017)
  16. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  17. Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas: \ssfSC$^2$: satisfiability checking meets symbolic computation. (Project paper) (2016)
  18. Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare: A new decision procedure for finite sets and cardinality constraints in SMT (2016)
  19. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  20. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)

1 2 3 next