Abstract
In this paper, we present the logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions (CLU). CLU generalizes the logic of equality with uninterpreted functions (EUF) with constrained lambda expressions, ordering, and successor and predecessor functions. In addition to modeling pipelined processors that EUF has proved useful for, CLU can be used to model many infinite-state systems including those with infinite memories, finite and infinite queues including lossy channels, and networks of identical processes. Even with this richer expressive power, the validity of a CLU formula can be efficiently decided by translating it to a propositional formula, and then using Boolean methods to check validity. We give theoretical and empirical evidence for the efficiency of our decision procedure. We also describe verification techniques that we have used on a variety of systems, including an out-of-order execution unit and the load-store unit of an industrial microprocessor.
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
P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. In CAV’98, LNCS 1427, pages 305–318.
W. Ackermann. Solvable Cases of the Decision Problem. 1954.
C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In FMCAD’96, LNCS 1166, pages 187–201.
A. J. C. Bik and H. A. G. Wijshoff. Implementation of Fourier-Motzkin elimination. Technical Report 94-42, Dept. of Computer Science, Leiden University, 1994.
B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In SAS’ 97, pages 172–186.
A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In CAV 2000, LNCS 1855, pages 403–418.
R. E. Bryant, S. German, and M. N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. ACM Transactions on Computational Logic, 2(1):93–134, January 2001.
R. E. Bryant and M. N. Velev. Boolean satisfiability with transitivity constraints. In CAV 2000, LNCS 1855, pages 85–98.
T. Bultan, R. Gerber, and W. Pugh. Symbolic model checking of infinite state systems using Presburger arithmetic. In CAV’ 97, LNCS 1254, pages 400–411.
J. R. Burch and D. L. Dill. Automated verification of pipelined microprocessor control. In CAV’ 94, LNCS 818, pages 68–80.
M. J. Fischer and M. O. Rabin. Super-exponential complexity of Presburger arithmetic. Proc. SIAM-AMS, 7:27–41, 1974.
Steven German. Personal communication.
M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. 1993.
R. Jhala and K. McMillan. Microarchitecture verification by compositional model checking. In CAV 2001, LNCS 2102, pages 396–410.
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In CAV’ 97, LNCS 1254, pages 424–435.
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Design Automation Conference (DAC’01), pages 530–535, June 2001.
S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In CADE’ 92, LNAI 607, pages 748–752.
A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small-domain instantiations. In CAV’ 99, LNCS 1633, pages 455–469.
V. Pratt. Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology, 1977. Cambridge, Mass.
O. Strichman, S. A. Seshia, and R. E. Bryant. Deciding separation formulas with SAT. In Proc. Computer-Aided Verification (CAV’02), July 2002. This volume.
UCLID. Available at http://www.cs.cmu.edu/~uclid.
M. N. Velev and R. E. Bryant. Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. In Design Automation Conference (DAC’ 01), pages 226–231, June 2001.
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
Bryant, R.E., Lahiri, S.K., Seshia, S.A. (2002). Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. 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_7
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_7
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