Abstract
In this paper we present algorithms for efficient image computation for systems represented as arithmetic constraints. We use automata as a symbolic representation for such systems. We show that, for a common class of systems, given a set of states and a transition, the time required for image computation is bounded by the product of the sizes of the automata encoding the input set and the transition. We also show that the size of the result has the same bound. We obtain these results using a linear time projection operation for automata encoding linear arithmetic constraints. We also experimentally show the benefits of using these algorithms by comparing our implementation with LASH and BRAIN.
This work is supported in part by NSF grant CCR-9970976 and NSF CAREER award CCR-9984822.
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
The Liège Automata-based Symbolic Handler (LASH), Available at http://www.montefiore.ulg.ac.be/~boigelot/research/lash/
Bartzis, C., Bultan, T.: Efficient symbolic representations for arithmetic constraints in verification. International Journal of Foundations of Computer Science (to appear)
Bartzis, C., Bultan, T.: Automata-based representations for arithmetic constraints in automated verification. In: Proceedings of the Seventh International Conference on Implementation and Application of Automata (2002)
Bartzis, C., Bultan, T.: Construction of efficient BDDs for bounded arithmetic constraints. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003)
Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 30–43. Springer, Heidelberg (1996)
Bryant, R.: Graph-based algorithms for boolean function manipulation. In: Proceedings of the 27th ACM/IEEE Design Automation Conference (1990)
Bultan, T., Yavuz-Kahveci, T.: Action language verifier. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (2001)
Bultan, T., Gerber, R., Pugh, W.: 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)
Delzanno, G., Bultan, T.: Constraint-based verification of client-server protocols. In: Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming (2001)
Delzanno, G., Podelski, A.: Constraint-based deductive model checking. Journal of Software Tools and Technology Transfer 3(3), 250–270 (2001)
Dor, N., Rodeh, M., Sagiv, M.: Cleanness checking of string manipulations in C programs via integer analysis. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 194–212. Springer, Heidelberg (2001)
Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2), 157–185 (1997)
Henzinger, T.A., Ho, P., Wong-Toi, H.: Hytech: a model checker for hybrid systems. Software Tools for Technology Transfer 1, 110–122 (1997)
Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus (2001)
McMillan, K.L.: Symbolic model checking. Kluwer Academic Publishers, Massachusetts (1993)
Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis (1992)
Rybina, T., Voronkov, A.: Using canonical representations of solutions to speed up infinite-state model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification, pp. 400–411 (2002)
Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints. In: Proceedings of the Static Analysis Symposium (1995)
Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Graf, S., Schwartzbach, M. (eds.) Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, pp. 1–19. Springer, Heidelberg (2000)
Yavuz-Kahveci, T., Bultan, T.: Specification, verification, and synthesis of concurrency control components. In: Proceedings of the International Symposium on Software Testing and Analysis, July 2002, pp. 169–179 (2002)
Yavuz-Kahveci, T., Tuncer, M., Bultan, T.: Composite symbolic library. In: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 2031, pp. 335–344. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bartzis, C., Bultan, T. (2003). Efficient Image Computation in Infinite State Model Checking. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive