Generating invariants for non-linear loops by linear algebraic methods

详细信息    查看全文

• 作者：Rachid Rebiha ; Arnaldo Vieira Moura ; Nadir Matringe
• 关键词：Formal methods ; Invariant generation ; Linear algebra
• 刊名：Formal Aspects of Computing
• 出版年：2015
• 出版时间：November 2015
• 年：2015
• 卷：27
• 期：5-6
• 页码：805-829
• 全文大小：897 KB
• 参考文献：AV97.Arnaudiesa JM, Valibouze A (1997) Lagrange resolvents. J Pure Appl Algebra 117?18: 23-0
  BBGL00.Bensalem S, Bozga M, Ghirvu J-C, Lakhnech L (2000) A transformation approach for generating non-linear invariants. Stat Anal Sympos 5: 101-14
  BLS96.Bensalem S, Lakhnech Y, Saidi H (1996) Powerful techniques for the automatic generation of invariants. In: Alur R, Henzinger TA (eds) Proceedings of the 8th international conference on computer aided verification CAV, vol 1102, pp 323-35
  Buc96.Buchberger B (1996) Symbolic computation: computer algebra and logic. In: Frontiers of combining systems. Proceedings of the 1st international workshop, Munich, pp 193-20
  CC77.Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symposium of the principles of programming languages, pp 238-52. ACM Press, New York
  CC92.Cousot P, Cousot R (1992) Abstract interpretation and application to logic programs. J Logic Program 13(2-): 103-79MATH MathSciNet CrossRef
  Col75.Collins GE (1975) Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: LNCS. Springer, New York
  Cou05.Cousot P (2005) Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Conference on VMCAI, pp 1-4, Paris, LNCS, vol 3385, 17-9 January 2005
  CXYZ07.Chen Y, Xia B, Yang L, Zhan N (2007) Generating polynomial invariants with discoverer and QEPCAD. In: Formal methods and hybrid, real-time systems, pp 67-2
  Dij76.Dijkstra EW (1976) A discipline of programming. Prentince-Hall, LondonMATH
  Fau99.Faugere J-C (1999) A new efficient algorithm for computing Grobner bases (f4). J Pure Appl Algebra 139(1-): 61-8MATH MathSciNet CrossRef
  Flo67.Floyd RW (1967) Assigning meanings to programs. In: Proceedings of the 19th symposium on applied mathematics, pp 19-7
  GT06.Gulwani S, Tiwari A (2006) Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft P (ed) European symposium on programming, ESOP 2006, LNCS, vol 3924, pp 279-93
  GT08.Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Proceedings of the 14th international conference on computer aided verification (CAV)
  Hoa69.Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10): 576-80MATH CrossRef
  JKP06.Jebelean T, Kovacs L, Popov N (2006) Experimental program verification in the theorema system. Int J Softw Tools Technol Transf (STTT) (in press)
  Kap04.Kapur D (2004) Automatically generating loop invariants using quantifier elimination. In: Proceedings of the IMACS international conference on applications of computer algebra
  KJ06.Kovacs L, Jebelean T (2006) Finding polynomial invariants for imperative loops in the theorema system. In: Proceedings of the verify-6 workshop, pp 52-7, 15-6 August 2006
  Kov08.Kovacs L (2008) Reasoning algebraically about p-solvable loops. In: TACAS 2008, Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems, LNCS, vol 4963, pp 249-64.
  Lan02.Lang S (2002) Algebra. Springer, New YorkMATH CrossRef
  MOS02.Müller-Olm M, Seidl H (2002) Polynomial constants are decidable. In: Static analysis symposium, LNCS, pp 4-9
  MP95.Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, New YorkCrossRef
  PC08.Platzer A, Clarke EM (2008) Clarke Computing differential invariants of hybrid systems as fixedpoints. In: Proceedings of the computer-aided verification, CAV 2008, Princeton, LNCS. Springer, New York
  PJ04.Prajna S, Jadbabaie A (2004) Safety verification of hybrid systems using barrier certificates
  RCK07a.Rodríguez-Carbonell E, Kapur D (2007) Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci Comput Program 64(1): 54-5MATH CrossRef
  RCK07b.Rodríguez-Carbonell E, Kapur D (2007) Generating all polynomial invariants in simple loops. J Symb Comput 42(4): 443-76MATH CrossRef
  RM09.Rebiha R, Moura AV (2009) Automated malware invariant generation. In: 6th international conference on forensic computer science, ICoFSC2009 and ICCYBER2009 (best paper award)
  RM11a.Rebiha R, Moura AV (2011) Algebraic formal methods for invariant generation. In: Ph.D. Dissertation, Faculty of Informatics USI, University of Lugano, Switzerland, pp 1-09
  RM11b.Rebiha R, Moura AV (2011) Algebraic formal methods for invariant generation. In: Ph.D. Dissertation, Insitute of Computing UNICAMP, University of Campinas, Sao Paulo, pp 1-14
  RM11c.Rebiha R, Moura AV (2011) Semantic malware resistance using inductive invariants. Int J Forensic Comput Sci (IJoFCS0) (best paper award, 5)
  RMM08a.Rebiha R, Matringe N, Moura AV (2008) Endomorphism for non-trivial semi-alge
• 作者单位：Rachid Rebiha (1)
  Arnaldo Vieira Moura (1)
  Nadir Matringe (2)
  
  1. Institute of Computing, University of Campinas, Campinas, Brazil
  2. LMA, University of Poitiers, Poitiers, France
  
• 刊物类别：Computer Science
• 刊物主题：Math Applications in Computer Science
  Theory of Computation
  Computational Mathematics and Numerical Analysis
  
• 出版者：Springer London
• ISSN：1433-299X

文摘

We present new computational methods that can automate the discovery and the strengthening of non-linear interrelationships among the variables of programs containing non-linear loops, that is, that give rise to multivariate polynomial and fractional relationships. Our methods have complexities lower than the mathematical foundations of the previous approaches, which used Gr?bner basis computations, quantifier eliminations or cylindrical algebraic decompositions. We show that the preconditions for discrete transitions can be viewed as morphisms over a vector space of degree bounded by polynomials. These morphisms can, thus, be suitably represented by matrices. We also introduce fractional and polynomial consecution, as more general forms for approximating consecution. The new relaxed consecution conditions are also encoded as morphisms represented by matrices. By so doing, we can reduce the non-linear loop invariant generation problem to the computation of eigenspaces of specific morphisms. Moreover, as one of the main results, we provide very general sufficient conditions allowing for the existence and computation of whole loop invariant ideals. As far as it is our knowledge, it is the first invariant generation methods that can handle multivariate fractional loops. Keywords Formal methods Invariant generation Linear algebra