Publications
If you are using CVC3 for your research and you wish to cite it, please cite the first paper listed below.
Tool papers
-
Clark Barrett and Cesare Tinelli.
CVC3.
In Werner Damm and Holger Hermanns, editors, Proceedings of the
19th International Conference on Computer Aided Verification (CAV '07),
volume 4590 of
Lecture Notes in Computer Science, pages 298-302. Springer, July 2007.
Berlin, Germany.
[
Abstract |
BibTeX |
Paper
]
-
Clark Barrett and Sergey Berezin.
CVC Lite: A New Implementation of the Cooperating Validity Checker.
In Proceedings of the
16th International Conference on Computer Aided Verification (CAV '04),
volume 3114 of
Lecture Notes in Computer Science, pages 515-518. Springer, July 2004.
Boston, Massachusetts.
[
Abstract |
BibTeX |
Paper
]
-
Aaron Stump, Clark W. Barrett, and David L. Dill.
CVC: A Cooperating Validity Checker.
In Proceedings of the 14th International
Conference on Computer Aided Verification (CAV '02), volume 2404 of
Lecture Notes in Computer Science, pages 500-504. Springer, 2002.
Copenhagen, Denmark.
[
Abstract |
BibTeX |
Paper
]
Theoretical papers
-
Clark Barrett,
Robert Nieuwenhuis,
Albert Oliveras, and
Cesare Tinelli.
Splitting on Demand in SAT Modulo Theories.
In
Proceedings of the 13th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (LPAR'06),
Phnom Penh, Cambodia, 2006.
[
Abstract
|
Paper
|
BibTeX
]
-
Clark Barrett, Igor Shikanian, and Cesare Tinelli.
An Abstract Decision Procedure for Satisfiability in the Theory of
Recursive Data Types.
In Proceedings of the Fourth Workshop on Pragmatics of
Decision Procedures in Automated Reasoning (PDPAR '06), August 2006.
Seattle, Washington.
[
Abstract |
BibTeX |
Paper
]
-
Robert Nieuwenhuis,
Albert Oliveras, and
Cesare Tinelli.
Abstract DPLL and Abstract DPLL Modulo Theories.
In
Proceedings of the 11th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (LPAR'04),
Montevideo, Uruguay, 2005.
[
Abstract
|
Paper
|
BibTeX
]
-
Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel,
and David L. Dill.
A Practical Approach to Partial Functions in CVC Lite.
In Selected Papers from the Workshops
on Disproving and the Second International Workshop on Pragmatics of Decision
Procedures (PDPAR '04), volume 125(3) of Electronic Notes in
Theoretical Computer Science, pages 13-23. Elsevier, July 2005. Cork, Ireland.
[
Abstract |
BibTeX |
Paper
]
-
Harald Ganzinger,
George Hagen,
Robert Nieuwenhuis,
Albert Oliveras, and
Cesare Tinelli.
DPLL(T): Fast Decision Procedures.
In
Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), Boston, USA,
2004.
[
Abstract
|
Paper
|
BibTeX
]
-
Aaron Stump, David L. Dill, Clark W. Barrett and Jeremy Levitt.
A Decision Procedure for an Extensional Theory of Arrays.
In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS '01),
pages 29-37. IEEE Computer Society, June 2001. Boston, Massachusetts.
[
Abstract |
BibTeX |
Paper
]
-
Clark W. Barrett. Checking Validity of Quantifier-Free Formulas in
Combinations of First-Order Theories. PhD Thesis, Stanford University, 2003.
Stanford, California.
[
Abstract |
BibTeX |
Paper |
PPT
]
Selected Applications
-
Yeting Ge, Clark Barrett, and Cesare Tinelli.
Solving Quantified Verification Conditions using Satisfiability Modulo Theories.
In Proceedings of the 21st International Conference on Automated Deduction
(CADE '07), volume 4603 of
Lecture Notes in Artificial Intelligence, pages 167-182.
Springer-Verlag, July 2007.
Bremen, Germany.
[
Abstract |
BibTeX |
Paper
]
-
Nikhil Sethi and Clark Barrett.
CASCADE: C Assertion Checker and Deductive Engine.
In Proceedings of the
18th International Conference on Computer Aided Verification (CAV '06),
volume 4144 of
Lecture Notes in Computer Science, pages 166-169.
Springer-Verlag, August 2006.
Seattle, Washington.
[
Abstract |
BibTeX |
Paper
]
-
Clark Barrett, Yi Fang, Ben Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck.
TVOC: A Translation Validator for Optimizing Compilers.
In Proceedings
of the 17th International Conference on Computer Aided Verification (CAV
'05), volume 3576 of
Lecture Notes in Computer Science, pages
291-295. Springer-Verlag, July 2005.
Edinburgh, Scotland.
[
Abstract |
BibTeX |
Paper
]
-
Ying Hu, Clark Barrett, and Benjamin Goldberg.
Theory and Algorithms for the Generation and Validation of
Speculative Loop Optimizations.
In Proceedings of the Second IEEE International Conference on
Software Engineering and Formal Methods (SEFM '04), pages 281-289.
IEEE Computer Society, September 2004. Beijing, China.
[
Abstract |
BibTeX |
Paper
]
-
Sean McLaughlin, Clark Barrett, and Yeting Ge.
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite.
In
Proceedings of the Third Workshop on Pragmatics of Decision Procedures in
Automated Reasoning (PDPAR '05), volume 144(2) of Electronic Notes in
Theoretical Computer Science, pages 43-51. Elsevier, January 2006.
Edinburgh, Scotland.
[
Abstract |
BibTeX |
Paper
]
-
Clark Barrett, Benjamin Goldberg, and Lenore Zuck.
Run-Time Validation of Speculative Optimizations using CVC.
In Proceedings of the Third International
Workshop on Run-time Verification (RV '03), volume 89(2) of Electronic
Notes in Theoretical Computer Science. Elsevier, October 2003. Boulder, Colorado.
[
Abstract |
BibTeX |
Paper
]
Third-party Applications
-
Hasan Amjad and Richard Bornat.
Towards Automatic Stability Analysis for Rely-Guarantee Proofs.
In Proceedings of the Tenth International Conference on
Verification, Model Checking, and Abstract Interpretation
(VMCAI '09), volume 5403 of Lecture Notes in Computer Science, pages 14-28.
Springer, January 2009. Savannah, GA, USA.
[
Springer Link
]
-
Suzette Person, Matthew B. Dwyer, Sebastian Elbaum, and Corina S. Pǎsǎreanu.
Differential Symbolic Execution.
In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering
(SIGSOFT '08/FSE-16), pages 226-237.
ACM, November 2008. Atlanta, GA, USA.
[
ACM Link
]
-
Thomas A. Henzinger, Thibaud Hottelier, and Laura Kovács.
Valigator: A Verification Tool with Bound and Invariant Generation.
In Proceedings of the 15th International Conference on
Logic for Programming, Artificial Intelligence, and Reasoning
(LPAR '08), volume 5330 of Lecture Notes in Computer Science, pages 333-342.
Springer, November 2008. Doha, Qatar.
[
Springer Link
]
-
Nathaniel Nystrom, Vijay Saraswat, Jens Palsberg, and Christian Grothoff.
Constrained Types for Object-Oriented Languages.
In Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming
(OOPSLA '08), pages 457-474.
ACM, October 2008. Nashville, TN, USA.
[
ACM Link
]
-
Patrice Chalin, Perry R. James, and George Karabotsos.
JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML.
In Proceedings of the Second International Conference on
Verified Software: Theories, Tools, Experiments
(VSTTE '08), volume 5295 of Lecture Notes in Computer Science, pages 70-83.
Springer, October 2008. Toronto, Canada.
[
Springer Link
]
-
Xutao Du, Chunxiao Xing, and Lizhu Zhou.
Abstract Reachability Graph for Verifying Web Service Interfaces.
In High Confidence Software Reuse in Large Systems, Proceedings of the 10th International Conference on Software Reuse
(ICSR '08), volume 5030 of Lecture Notes in Computer Science, pages 262-265.
Springer, May 2008. Beijing, China.
[
Springer Link
]
-
Karen Zee, Viktor Kuncak, and Martin Rinard.
Verifying Linked Data Structure Implementations.
In IEEE International Symposium on Parallel and Distributed Processing (IPDPS '08), pages 1-5.
IEEE, April 2008. Miami, FL, USA.
[
IEEE Link
]
-
Paul B. Jackson, Bill J. Ellis, and Kathleen Sharp.
Using SMT Solvers to Verify High-Integrity Programs.
In Proceedings of the Second Workshop on Automated Formal Methods (AFM '07), pages 60-68.
ACM, November 2007. Atlanta, GA, USA.
[
ACM Link
]
-
Jean-Christophe Filliâtre and Claude Marché.
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification.
In Proceedings of the 19th International Conference on Computer Aided Verification
(CAV '07), volume 4590 of Lecture Notes in Computer Science, pages 173-177.
Springer, July 2007. Berlin, Germany.
[
Springer Link
]
