Abstract
Linear-relations analysis of transition systems discovers linear invariant relationships among the variables of the system. These relationships help establish important safety and liveness properties. Efficient techniques for the analysis of systems using polyhedra have been explored, leading to the development of successful tools like HyTech. However, existing techniques rely on the use of approximations such as widening and extrapolation in order to ensure termination. In an earlier paper, we demonstrated the use of Farkas Lemma to provide a translation from the linear-relations analysis problem into a system of constraints on the unknown coefficients of a candidate invariant. However, since the constraints in question are non-linear, a naive application of the method does not scale. In this paper, we show that by some efficient simplifications and approximations to the quantifier elimination procedure, not only does the method scale to higher dimensions, but also enjoys performance advantages for some larger examples.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337–354. Springer, Heidelberg (2003)
Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002)
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: Fast accelereation of symbolic transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)
Besson, F., Jensen, T., Talpin, J.-P.: Polyhedral analysis of synchronous languages. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 51–69. Springer, Heidelberg (1999)
Collins, G.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–433. Springer, Heidelberg (2003)
Cousot, P., Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Principles of Programming Languages, pp. 238–252 (1977)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: ACM Principles of Programming, January 1978, pp. 84–97 (1978)
Fukuda, K., Prodon, A.: Double description method revisited. In Combinatorics and Computer Science. In: Deza, M., Manoussakis, I., Euler, R. (eds.) CCS 1995. LNCS, vol. 1120, pp. 91–111. Springer, Heidelberg (1996)
Halbwachs, N., Merchat, D., Parent-Vigouroux, C.: Cartesian factoring of polyhedra for linear relation analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 355–365. Springer, Heidelberg (2003)
Halbwachs, N., Proy, Y., 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.: HyTech: The Cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 265–293. Springer, Heidelberg (1995)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Petri net analysis using invariant generation. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 682–701. Springer, Heidelberg (2004)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)
Tarski, A.: A decision method for elementary algebra and geometry, p. 5. Univ. of California Press, Berkeley (1951)
Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation 5(1-2), 3–27 (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sankaranarayanan, S., Sipma, H.B., Manna, Z. (2004). Constraint-Based Linear-Relations Analysis. In: Giacobazzi, R. (eds) Static Analysis. SAS 2004. Lecture Notes in Computer Science, vol 3148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27864-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-27864-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22791-5
Online ISBN: 978-3-540-27864-1
eBook Packages: Springer Book Archive