×

CVC Lite

swMATH ID: 7581
Software Authors: Mclaughlin, Sean; Barrett, Clark; Ge, Yeting
Description: CVC Lite is no longer being maintained. Please visit the CVC3 web site for the current version of CVC. ————– Cooperating theorem provers: a case study combining HOL-Light and CVC Lite This paper is a case study in combining theorem provers. We define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite and translates the resulting proof object back to HOL-Light. As a result, we obtain a highly trusted proof-checker for CVC Lite, while also fundamentally expanding the capabilities of HOL-Light.
Homepage: http://www.cs.nyu.edu/acsys/cvc3/
Related Software: HOL Light; Chaff; CVC; SMT-LIB; z3; Isabelle/HOL; MiniSat; E Theorem Prover; SIMPLIFY; cvc3; ICS; MathSAT; SPASS; VAMPIRE; Yices; Metis_; Coq; Isabelle; veriT; HOL
Referenced in: 51 Publications
all top 5

Referenced by 111 Authors

5 Barrett, Clark W.
5 Böhme, Sascha
4 Blanchette, Jasmin Christian
4 Cimatti, Alessandro
4 Meier, Andreas
4 Sorge, Volker
4 Stump, Aaron
3 Armando, Alessandro
3 Bruttomesso, Roberto
3 Colton, Simon
3 de Moura, Leonardo
3 McCasland, Roy L.
3 Paulson, Lawrence Charles
3 Ranise, Silvio
3 Sebastiani, Roberto
3 Weber, Tjark
2 Barsotti, Damián
2 Bonacina, Maria Paola
2 Bozzano, Marco
2 Fontaine, Pascal
2 Junttila, Tommi A.
2 Kuncak, Viktor
2 Leino, K. Rustan M.
2 Moskal, Michał
2 Schulz, Stephan
2 van Rossum, Peter
1 Ábrahám, Erika
1 Amjad, Hasan
1 Armand, Michaël
1 Barbosa, Haniel
1 Becker, Bernd
1 Berezin, Sergey
1 Besson, Frédéric
1 Bjørner, Nikolaj S.
1 Blanco, Javier Oscar
1 Bockenek, Joshua A.
1 Castellini, Claudio
1 Chechik, Marsha
1 Clancy, Kevin
1 Cornilleau, Pierre-Emmanuel
1 Currie, David J.
1 Davis, Ernest
1 de Nivelle, Hans
1 Déharbe, David
1 Echenim, Mnacho
1 Faure, Germain
1 Feng, Xiushan
1 Fleury, Mathias
1 Fox, Anthony C. J.
1 Franzén, Anders
1 Fujita, Masahiro
1 Ge, Yeting
1 Giunchiglia, Enrico
1 Grégoire, Benjamin
1 Griggio, Alberto
1 Gu, Ming
1 Gulwani, Sumit
1 Gurfinkel, Arie
1 He, Kai-Duo
1 Herbstritt, Marc
1 Hsiao, Michael S.
1 Hu, Alan J.
1 Jones, Robert B.
1 Kaliszyk, Cezary
1 Kang, Eun-Young
1 Keller, Chantal
1 Krishnamoorthy, Saparya
1 Kröning, Daniel
1 Krstic, Sava A.
1 Kugler, Hillel
1 Kwan, Mark
1 Li, Li
1 Lingappan, Loganathan
1 Logozzo, Francesco
1 Maratea, Marco
1 McLaughlin, Sean
1 Merz, Stephan
1 Musuvathi, Madan
1 Musuvathi, Madanlal
1 Necula, George C.
1 Nguyen, Huu Hai
1 Nieto, Leonor Prensa
1 Oe, Duckki
1 Oliver, Corey
1 Ou, Xinming
1 Pichardie, David
1 Piskac, Ruzica
1 Rajan, Sreeranga P.
1 Ravindran, Binoy
1 Rinard, Martin C.
1 Schreiner, Wolfgang
1 Schulte, Wolfram
1 Sewell, Thomas D.
1 Shikanian, Igor
1 Shin, Ji-Ae
1 Song, Xiaoyu
1 Steffen, Martin
1 Strichman, Ofer
1 Tan, Liyang
1 Théry, Laurent
...and 11 more Authors

Referencing Publications by Year