CVC4 swMATH ID: 9485 Software Authors: Barrett, C.; Conway, C. L.; Deters, M.; Hadarean, L.; Jovanović, D.; King, T.; Reynolds, A.; Tinelli, C. Description: 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). Homepage: http://cvc4.cs.nyu.edu/web/ Related Software: z3; SMT-LIB; VAMPIRE; MathSAT5; Isabelle/HOL; Yices; GitHub; cvc5; TPTP; Sledgehammer; Coq; veriT; SIMPLIFY; E Theorem Prover; Dafny; MiniSat; SPASS; Why3; Boolector; StarExec Cited in: 234 Documents Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). Zbl 07628183Kremer, Gereon; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare 2022 Induction for SMT solvers. Zbl 1432.68418Reynolds, Andrew; Kuncak, Viktor 2015 all top 5 Cited by 484 Authors 31 Barrett, Clark W. 29 Reynolds, Andrew 26 Tinelli, Cesare 12 Kovács, Laura Ildikó 11 Blanchette, Jasmin Christian 11 Zohar, Yoni 10 Kuncak, Viktor 9 Barbosa, Haniel 9 Niemetz, Aina 9 Preiner, Mathias 9 Voronkov, Andrei 8 Day, Joel D. 8 Nowotka, Dirk 7 Ganesh, Vijay 7 Manea, Florin 6 Bromberger, Martin 6 Kremer, Gereon 6 Kulczynski, Mitja 6 Nötzli, Andres 6 Weidenbach, Christoph 5 Ábrahám, Erika 5 Benzmüller, Christoph Ewald 5 De Angelis, Emanuele 5 Demri, Stéphane P. 5 Deters, Morgan 5 Fioravanti, Fabio 5 Fontaine, Pascal 5 Proietti, Maurizio 5 Reger, Giles 5 Sturm, Thomas 5 Tourret, Sophie 4 Bansal, Kshitij 4 Griggio, Alberto 4 Holík, Lukáš 4 Hozzová, Petra 4 Iosif, Radu 4 Mora, Federico 4 Pettorossi, Alberto 4 Rümmer, Philipp 4 Sheng, Ying 4 Vukmirović, Petar 3 Bardin, Sébastien 3 Bentkamp, Alexander 3 Berzish, Murphy 3 Bøgsted Poulsen, Danny 3 Chen, Yu-Fang 3 Cimatti, Alessandro 3 Cruanes, Simon 3 de Moura, Leonardo 3 Farzan, Azadeh 3 Fleury, Mathias 3 Kaliszyk, Cezary 3 Konnov, Igor Vladimirovich 3 Kröning, Daniel 3 Lotz, Kevin 3 Ozdemir, Alex 3 Peltier, Nicolas 3 Polgreen, Elizabeth 3 Robillard, Simon 3 Sharygina, Natasha 3 Steen, Alexander 3 Sutcliffe, Geoff 3 Urban, Josef 3 Viswanathan, Arjun 2 Abdulla, Parosh Aziz 2 Atig, Mohamed Faouzi 2 Biere, Armin 2 Bjørner, Nikolaj S. 2 Cai, Shaowei 2 Chakraborty, Supratik 2 Claessen, Koen 2 Corzilius, Florian 2 Czarnecki, Krzysztof 2 Diep, Bui Phi 2 Dill, David L. 2 Durán, Francisco 2 Echenim, Mnacho 2 Eisenhofer, Clemens 2 Eker, Steven 2 Escobar, Santiago 2 Farinier, Benjamin 2 Filliâtre, Jean-Christophe 2 Girol, Guillaume 2 Gleiss, Bernhard 2 Grieskamp, Wolfgang 2 Guilloud, Simon 2 Gupta, Ashutosh 2 Hajdú, Márton 2 Heinle, Albert 2 Irfan, Ahmed 2 Itzhaky, Shachar 2 Johansson, Moa 2 Jonáš, Martin 2 King, Tim 2 Koskinen, Eric 2 Lachnitt, Hanna 2 Larraz, Daniel 2 Lazić, Marijana 2 Li, Bohan 2 Lucanu, Dorel ...and 384 more Authors all top 5 Cited in 27 Serials 26 Journal of Automated Reasoning 9 Formal Methods in System Design 7 Journal of Logical and Algebraic Methods in Programming 3 Artificial Intelligence 3 Theoretical Computer Science 3 Formal Aspects of Computing 3 Theory of Computing Systems 3 ACM Transactions on Computational Logic 3 Logical Methods in Computer Science 2 Acta Informatica 2 Constraints 2 Fundamenta Informaticae 2 Theory and Practice of Logic Programming 1 Information Sciences 1 Annals of Pure and Applied Logic 1 Journal of Symbolic Computation 1 Information and Computation 1 AI Communications 1 Journal of Global Optimization 1 Cybernetics and Systems Analysis 1 Journal of Functional Programming 1 International Transactions in Operational Research 1 Mathematics in Computer Science 1 Scientific Annals of Computer Science 1 ACM Communications in Computer Algebra 1 Acta Universitatis Sapientiae. Informatica 1 Texts in Theoretical Computer Science. An EATCS Series all top 5 Cited in 18 Fields 231 Computer science (68-XX) 62 Mathematical logic and foundations (03-XX) 9 Operations research, mathematical programming (90-XX) 4 Combinatorics (05-XX) 3 Numerical analysis (65-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 1 History and biography (01-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) 1 Category theory; homological algebra (18-XX) 1 Group theory and generalizations (20-XX) 1 Real functions (26-XX) 1 Ordinary differential equations (34-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Geometry (51-XX) 1 Convex and discrete geometry (52-XX) 1 Biology and other natural sciences (92-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year