Abstract
In this paper we discuss reachability analysis for infinite-state systems in which states can be represented by a vector of integers. We propose a new algorithm for verifying reachability properties based on canonical representations of solutions to systems of linear inequations over integers instead of decision procedures for integer or real arithmetic. Experimental results demonstrate that problems in protocol verification which are beyond the reach of other existing systems can be solved completely automatically.
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. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1–2): 109–127, January 2000.
F. Ajili and E. Contejean. Avoiding slack variables in the solving of linear Diophantine equations and inequations. Theoretical Computer Science, 173(1):183–208, 1997.
B. Bérard and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmetic. In J. C. M. Baeten and S. Mauw, editors, CONCUR’99: Concurrency Theory, 10th International Conference, volume 1664 of Lecture Notes in Computer Science, pages 178–193. Springer Verlag, 1999.
T. Bultan. Action Language: a specification language for model checking reactive systems. In ICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, pages 335–344, Limerick, Ireland, 2000. ACM.
T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747–789, 1999.
E. Contejean and H. Devie. An efficient incremental algorithm for solving of systems of linear diophantine equations. Information and Computation, 113(1):143–172, 1994.
G. Delzanno. Automatic verification of parametrized cache coherence protocols. In A. E. Emerson and A. P. Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, volume 1855 of Lecture Notes in Computer Science, pages 53–68. Springer Verlag, 2000.
G. Delzanno and A. Podelski. Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer, 3(3):250–270, 2001.
J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In 14th Annual IEEE Symposium on Logic in Computer Science (LICS’99), pages352–359, Trento, Italy, 1999. IEEE Computer Society.
N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, 1997.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hy-tech: a model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1–2): 110–122, 1997.
D. Hilbert. Über die Theorie der algebraischen Formen. Mathematische Annalen, 36:473–534, 1890.
O. Kupferman and M. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291–314, 2001.
W. Pugh. Counting solutions to Presburger formulas: how and why. ACM SIGPLAN Notices, 29(6):121–134, June 1994. Proceedings of the ACM SIGPLAN’94 Conference on Programming Languages Design and Implementation (PLDI).
T. Rybina and A. Voronkov. A logical reconstruction of reachability. submitted, 2002.
A. Schrijver. Theory of Linear and Integer Programming. John Wiley and Sons, 1998.
A. P. Tomás and M. Filgueiras. An algorithm for solving systems of linear diophantine equations in naturals. In E. Costa and A. Cardoso, editors, Progress in Artificial Intelligence, 8th Portugese Conference on Artificial Intelligence, EPIA’ 97, volume 1323 of Lecture Notes in Artificial Intelligence, pages 73–84, Coimbra, Portugal, 1997. Springer Verlag.
A. Voronkov. An incremental algorithm for finding the basis of solutions to systems of linear Diophantine equations and inequations. unpublished, January 2002.
T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. A library for composite symbolic representations. In T. Margaria, editor, Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference, TACAS 2001, volume 1384 of Lecture Notes in Computer Science, pages 52–66, Genova, Italy, 2001. Springer Verlag.
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
Rybina, T., Voronkov, A. (2002). Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking. 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_32
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_32
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