Abstract
Decision procedures for decidable logics and logical theories have proven to be useful tools in verification. This paper describes the CVC (“Cooperating Validity Checker”) decision procedure. CVC implements a framework for combining subsidiary decision procedures for certain logical theories into a decision procedure for the theories’ union. Subsidiary decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently implemented. Other notable features of CVC are the incorporation of the high-performance Chaff solver for propositional reasoning, and the ability to produce independently checkable proofs for valid formulas.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In M. Srivas and A. Camilleri, editors, Formal Methods In Computer-Aided Design, volume 1166 of LNCS, pages 187–201. Springer-Verlag, 1996.
C. Barrett, D. Dill, and A. Stump. A Framework for Cooperating Decision Procedures. In David McAllester, editor, 17th International Conference on Computer Aided Deduction, volume 1831 of LNAI, pages 79–97. Springer-Verlag, 2000.
C. Barrett, D. Dill, and A. Stump. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In 14th International Conference on Computer-Aided Verification, 2002.
J. Filliâtre, S. Owre, H. Rueß, and N. Shankar. ICS: integrated canonizer and solver. In G. Berry, H. Comon, and A. Finkel, editors, 13th International Conference on Computer-Aided Verification, 2001.
R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993.
M. Moskewicz, C. Madigan, Y. Zhaod, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In 39th Design Automation Conference, 2001.
G. Nelson and D. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–57, 1979.
S. Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume607 of LNAI, pages 748–752. Springer-Verlag, 1992.
J. Skakkebæk, R. Jones, and D. Dill. Formal verification of out-of-order execution using incremental flushing. In 10th International Conference on Computer Aided Verification, 1998.
A. Stump, C. Barrett, D. Dill, and J. Levitt. A Decision Procedure for an Extensional Theory of Arrays. In 16th IEEE Symposium on Logic in Computer Science, pages 29–37. IEEE Computer Society, 2001.
A. Stump and D. Dill. Faster Proof Checking in the Edinburgh Logical Framework. In 18th International Conference on Automated Deduction, 2002.
A. Stump and D. Dill. Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. In 3rd International Workhsop on Logical Frameworks and Meta-Languages, 2002. (acceptance pending).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stump, A., Barrett, C.W., Dill, D.L. (2002). CVC: A Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_40
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive