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; MathSAT5; Yices; VAMPIRE; Isabelle/HOL; SIMPLIFY; TPTP; Sledgehammer; veriT; Coq; SPASS; E Theorem Prover; StarExec; Why3; Dafny; MiniSat; Boolector; GitHub; iProver Cited in: 158 Publications 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 344 Authors 23 Reynolds, Andrew 22 Barrett, Clark W. 18 Tinelli, Cesare 7 Blanchette, Jasmin Christian 7 Kovács, Laura Ildikó 7 Niemetz, Aina 7 Preiner, Mathias 7 Zohar, Yoni 6 Bromberger, Martin 6 Ganesh, Vijay 6 Kuncak, Viktor 6 Voronkov, Andrei 6 Weidenbach, Christoph 5 Ábrahám, Erika 5 Barbosa, Haniel 5 Day, Joel D. 5 Demri, Stéphane P. 5 Deters, Morgan 5 Fontaine, Pascal 5 Kremer, Gereon 5 Sturm, Thomas 4 Bansal, Kshitij 4 Benzmüller, Christoph Ewald 4 Manea, Florin 4 Mora, Federico 4 Nowotka, Dirk 3 Berzish, Murphy 3 De Angelis, Emanuele 3 de Moura, Leonardo 3 Fioravanti, Fabio 3 Griggio, Alberto 3 Iosif, Radu 3 Kaliszyk, Cezary 3 Kulczynski, Mitja 3 Nötzli, Andres 3 Peltier, Nicolas 3 Proietti, Maurizio 3 Robillard, Simon 3 Urban, Josef 2 Bardin, Sébastien 2 Biere, Armin 2 Chakraborty, Supratik 2 Cimatti, Alessandro 2 Claessen, Koen 2 Corzilius, Florian 2 Cruanes, Simon 2 Czarnecki, Krzysztof 2 Durán, Francisco 2 Echenim, Mnacho 2 Eker, Steven 2 Escobar, Santiago 2 Filliâtre, Jean-Christophe 2 Fleury, Mathias 2 Gleiss, Bernhard 2 Gupta, Ashutosh 2 Heinle, Albert 2 Hozzová, Petra 2 Irfan, Ahmed 2 Johansson, Moa 2 Jonáš, Martin 2 King, Tim 2 Koskinen, Eric 2 Kröning, Daniel 2 Larraz, Daniel 2 Mann, Makai 2 Marché, Claude 2 Martí-Oliet, Narciso 2 Ozdemir, Alex 2 Pettorossi, Alberto 2 Polgreen, Elizabeth 2 Reger, Giles 2 Rosen, Dan 2 Rümmer, Philipp 2 Serban, Cristina 2 Seshia, Sanjit Arunkumar 2 Sharygina, Natasha 2 Sheng, Ying 2 Smallbone, Nicholas 2 Steen, Alexander 2 Strejček, Jan 2 Sutcliffe, Geoff 2 Talcott, Carolyn L. 2 Tourret, Sophie 2 Tripp, Omer 2 Viswanathan, Arjun 2 Zeljić, Aleksandar 2 Zulkoski, Edward 1 Abbasi, Rosa 1 Abbott, John A. 1 Abdulla, Parosh Aziz 1 Ahrendt, Wolfgang 1 Akgün, Özgür 1 Alberti, Francesco 1 Alhiyafi, Jamal 1 Atig, Mohamed Faouzi 1 Backeman, Peter 1 Bagnara, Abramo 1 Bagnara, Roberto 1 Bao, Yuyan 1 Baranowski, Marek ...and 244 more Authors all top 5 Cited in 25 Serials 18 Journal of Automated Reasoning 7 Formal Methods in System Design 5 Journal of Logical and Algebraic Methods in Programming 3 Theoretical Computer Science 2 Artificial Intelligence 2 Formal Aspects of Computing 2 Logical Methods in Computer Science 1 Acta Informatica 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 Constraints 1 Theory of Computing Systems 1 Fundamenta Informaticae 1 Theory and Practice of Logic Programming 1 ACM Transactions on Computational Logic 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 13 Fields 157 Computer science (68-XX) 40 Mathematical logic and foundations (03-XX) 5 Operations research, mathematical programming (90-XX) 3 Numerical analysis (65-XX) 2 Combinatorics (05-XX) 1 History and biography (01-XX) 1 Commutative algebra (13-XX) 1 Category theory; homological algebra (18-XX) 1 Real functions (26-XX) 1 Ordinary differential equations (34-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Convex and discrete geometry (52-XX) 1 Biology and other natural sciences (92-XX) Citations by Year