Skip to main content
SpringerLink
Log in

Template Polyhedra with a Twist

  • Conference paper
  • First Online:
Static Analysis (SAS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10422))

Included in the following conference series:

  • 1191 Accesses

Abstract

In this paper, we draw upon connections between bilinear programming and the process of computing (post) fixed points in abstract interpretation. It is well-known that the data flow constraints for numerical domains are expressed in terms of bilinear constraints. Algorithms such as policy and strategy iteration have been proposed for the special case of bilinear constraints that arise from template numerical domains. In particular, policy iteration improves upon a known post-fixed point by alternating between solving for an improved post-fixed point against finding certificates that are used to prove the new fixed point.

In this paper, we draw upon these connections to formulate a policy iteration scheme that changes the template on the fly in order to prove a target reachability property of interest. We show how the change to the template naturally fits inside a policy iteration scheme, and thus propose a policy iteration scheme that updates the template matrices associated with each program location. We demonstrate that the approach is effective over a set of benchmark instances, wherein starting from a simple predefined choice of templates, the approach is able to infer appropriate template directions to prove a property of interest. We also note some key theoretical questions regarding the convergence of the policy iteration scheme with template updates, that remain open at this time.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Adjé, A., Garoche, P.-L.: Automatic synthesis of piecewise linear quadratic invariants for programs. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 99–116. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46081-8_6

    Google Scholar 

  2. Adjé, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. Log. Methods Comput. Sci. 8(1), 1–32 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  3. Adjé, A., Gaubert, S., Goubault, E.: Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs. J. Math. Anal. Appl. 410(1), 227–240 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  4. Amato, G., Parton, M., Scozzari, F.: Deriving numerical abstract domains via principal component analysis. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 134–150. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15769-1_9

    Chapter  Google Scholar 

  5. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation, pp. 196–207. ACM Press (2003)

    Google Scholar 

  6. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002). doi:10.1007/3-540-36377-7_5

    Chapter  Google Scholar 

  7. Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guided refinement of template polyhedra. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 589–606. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54577-5_34

    Chapter  Google Scholar 

  8. Chen, X., Abraham, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Real Time Systems Symposium (RTSS), pp. 183–192. IEEE Press (2012)

    Google Scholar 

  9. Chen, X., Ábrahám, E.: Choice of directions for the approximation of reachable sets for hybrid systems. In: Moreno-Díaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2011. LNCS, vol. 6927, pp. 535–542. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27549-4_69

    Chapter  Google Scholar 

  10. Chvátal, V.: Linear Programming. Freeman, New York (1983)

    MATH  Google Scholar 

  11. Clariso, R., Cortadella, J.: The octahedron abstract domain. Sci. Comput. Program. 64(1), 115–139 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  12. Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_39

    Chapter  Google Scholar 

  13. Costan, A., Gaubert, S., Goubault, E., Martel, M., Putot, S.: A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 462–475. Springer, Heidelberg (2005). doi:10.1007/11513988_46

    Chapter  Google Scholar 

  14. Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30579-8_1

    Chapter  Google Scholar 

  15. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of ISOP 1976, pp. 106–130. Dunod, Paris (1976)

    Google Scholar 

  16. Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992). doi:10.1007/3-540-55844-6_142

    Chapter  Google Scholar 

  17. 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)

    Google Scholar 

  18. Delmas, D., Souyris, J.: Astrée: from research to industry. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 437–451. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74061-2_27

    Chapter  Google Scholar 

  19. Frehse, G., Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30

    Chapter  Google Scholar 

  20. Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 237–252. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71316-6_17

    Chapter  Google Scholar 

  21. Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 300–315. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71316-6_21

    Chapter  Google Scholar 

  22. Gawlitza, T.M., Seidl, H.: Solving systems of rational equations through strategy iteration. ACM Trans. Program. Lang. Syst. 33(3), 11:1–11:48 (2011)

    Article  Google Scholar 

  23. Ghaoui, L.E., Balakrishnan, V.: Synthesis of fixed-structure controllers via numerical optimization. In: Proceedings of the 33rd Conference on Decision and Control (CDC). IEEE (1994)

    Google Scholar 

  24. Goubault, E., Putot, S., Baufreton, P., Gassino, J.: Static analysis of the accuracy in control systems: principles and experiments. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 3–20. Springer, Heidelberg (2008). doi:10.1007/978-3-540-79707-4_3

    Chapter  Google Scholar 

  25. Guernic, C.L., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250–262 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  26. Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI. pp. 281–292. ACM (2008)

    Google Scholar 

  27. Helton, J., Merino, O.: Coordinate optimization for bi-convex matrix inequalities. In: IEEE Conference on Decision and Control (CDC), pp. 3609–3613 (1997)

    Google Scholar 

  28. Logozzo, F., Fähndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: Symposium on Applied Computing, SAC 2008, NY, USA, pp. 184–188. ACM, New York (2008)

    Google Scholar 

  29. Mathworks Inc.: PolySpace design verifier. http://www.mathworks.com/products/polyspace/. Accessed Apr 2017

  30. Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001). doi:10.1007/3-540-44978-7_10

    Chapter  Google Scholar 

  31. Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310–319. IEEE, IEEE CS Press, October 2001

    Google Scholar 

  32. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)

    Book  MATH  Google Scholar 

  33. Roux, P., Voronin, Y.-L., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 424–446. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53413-7_21

    Chapter  Google Scholar 

  34. Sankaranarayanan, S., Dang, T., Ivančić, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188–202. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_14

    Chapter  Google Scholar 

  35. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53–68. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27864-1_7

    Chapter  Google Scholar 

  36. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30579-8_2

    Chapter  Google Scholar 

  37. Sassi, M.A.B., Girard, A., Sankaranarayanan, S.: Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: IEEE Conference on Decision and Control (CDC), pp. 6348–6353. IEEE Press (2014)

    Google Scholar 

  38. Sassi, M.A.B., Sankaranarayanan, S., Chen, X., Ábraham, E.: Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis. IMA J. Math. Control Inf. 33, 723–756 (2016)

    Article  MathSciNet  Google Scholar 

  39. Venet, A., Brat, G.P.: Precise and efficient static array bound checking for large embedded C programs. In: PLDI, pp. 231–242. ACM (2004)

    Google Scholar 

  40. Weispfenning, V.: Quantifier elimination for real algebra–the quadratic case and beyond. Appl. Algebr. Error-Correct. Codes (AAECC) 8, 85–101 (1997)

    MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

The authors gratefully acknowledge the anonymous reviewers for their valuable comments and suggestions. This work was funded in part by NSF under award numbers SHF 1527075. All opinions expressed are those of the authors, and not necessarily of the NSF.

Author information

Authors and Affiliations

  1. University of Colorado, Boulder, CO, USA

    Sriram Sankaranarayanan

  2. Mediterranean Institute of Technology (MedTech), Tunis, Tunisia

    Mohamed Amin Ben Sassi

Authors
  1. Sriram Sankaranarayanan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohamed Amin Ben Sassi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sriram Sankaranarayanan .

Editor information

Editors and Affiliations

  1. Dipartimento di Matematica, University of Padova, Padua, Italy

    Francesco Ranzato

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Sankaranarayanan, S., Ben Sassi, M.A. (2017). Template Polyhedra with a Twist. In: Ranzato, F. (eds) Static Analysis. SAS 2017. Lecture Notes in Computer Science(), vol 10422. Springer, Cham. https://doi.org/10.1007/978-3-319-66706-5_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66706-5_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66705-8

  • Online ISBN: 978-3-319-66706-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation