• Non-linear loop invariant gene...

Treffer: Non-linear loop invariant generation using gröbner bases

Title:
Non-linear loop invariant generation using gröbner bases
Authors:
SANKARANARAYANAN, Sriram, SIPMA, Henny B, MANNA, Zohar
Source:
Proceedings of the 2004 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004)ACM SIGPLAN notices. 39(1):318-329
Publisher Information:
Broadway, NY: ACM, 2004.
Publication Year:
2004
Physical Description:
print, 30 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Analyse programme, Program analysis, Análisis programa, Base Gröbner, Gröbner basis, Boucle programme, Program loop, Bucle programa, Calcul symbolique, Symbolic computation, Cálculo simbólico, Complétude, Completeness, Completitud, Programmation logique avec contrainte, Constraint logic programming, Programación lógica con restricción, Vérification programme, Program verification, Verificación programa, Contrainte ensembliste, Set constraint, Algorithms, Constraint Programming, Gröbner Bases, Ideals, Invariant Generation, Languages, Symbolic Computation, Theory, Verification. Program Analysis, Verification
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Department of Computer Science, Stanford University, Stanford, CA 94305, United States
ISSN:
1523-2867
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=15499435
Rights:
Copyright 2004 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.15499435
Database:
PASCAL Archive

Weitere Informationen

We present a new technique for the generation of non-linear (algebraic) invariants of a program. Our technique uses the theory of ideals over polynomial rings to reduce the non-linear invariant generation problem to a numerical constraint solving problem. So far, the literature on invariant generation has been focussed on the construction of linear invariants for linear programs. Consequently, there has been little progress toward non-linear invariant generation. In this paper, we demonstrate a technique that encodes the conditions for a given template assertion being an invariant into a set of constraints, such that all the solutions to these constraints correspond to non-linear (algebraic) loop invariants of the program. We discuss some trade-offs between the completeness of the technique and the tractability of the constraint-solving problem generated. The application of the technique is demonstrated on a few examples.