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

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

1 2 3 next

  1. Chakraborty, Supratik; Gupta, Ashutosh; Jain, Rahul: Matching multiplications in bit-vector formulas (2017)
  2. 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)
  3. 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)
  4. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  5. Demri, Stéphane; Galmiche, Didier; Larchey-Wendling, Dominique; Méry, Daniel: Separation logic with one quantified variable (2017)
  6. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  7. Jovanović, Dejan: Solving nonlinear integer arithmetic with MCSAT (2017)
  8. Nguy^en, Phúc C.; Tobin-Hochstadt, Sam; Van Horn, David: Higher order symbolic execution for contract verification and refutation (2017)
  9. Nightingale, Peter; Akgün, Özgür; Gent, Ian P.; Jefferson, Christopher; Miguel, Ian; Spracklen, Patrick: Automatically improving constraint models in Savile row (2017)
  10. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
  11. Reynolds, Andrew; Iosif, Radu; Serban, Cristina: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic (2017)
  12. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  13. Á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)
  14. Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare: A new decision procedure for finite sets and cardinality constraints in SMT (2016)
  15. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  16. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  17. Bromberger, Martin; Weidenbach, Christoph: Fast cube tests for LIA constraint solving (2016)
  18. Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei: Adding decision procedures to SMT solvers using axioms with triggers (2016)
  19. Hupel, Lars; Kuncak, Viktor: Translating scala programs to isabelle/HOL. System description (2016)
  20. Inala, Jeevana Priya; Singh, Rohit; Solar-Lezama, Armando: Synthesis of domain specific CNF encoders for bit-vector solvers (2016)

1 2 3 next