Automatic generation of loop invariants
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2099.1/12693
Tutor / directorRubio, Alberto
Tipus de documentProjecte Final de Màster Oficial
Data2011-06
Condicions d'accésAccés obert
Llevat que s'hi indiqui el contrari, els
continguts d'aquesta obra estan subjectes a la llicència de Creative Commons
:
Reconeixement-NoComercial-SenseObraDerivada 3.0 Espanya
Abstract
CppInv works in two stages. Firstly, it parses a source code written in a subset of
C++ and abstracts all execution paths of the program building a control flow graph
associated to a transition system. Paths are expressed as arbitrary propositional
formulas over linear integer arithmetic including high level operators like integer
division and modulo. That makes easy the initial modeling. Later, formulas are
normalized and only paths between a set of locations that cover every cycle of the
control flow graph are regarded.
Secondly, CppInv generates linear invariants at the selected locations setting out
a constraint solving problem. We present a method to discover all linear invariant
of the considered form.
As a result, our tool can find linear invariants efficiently for a large set of interesting
programs. Moreover, CppInv is also able to generate some non-linear invariants
automatically. For instance, it is possible to prove the total correctness of a program
that multiplies two integers from the invariants returned by the tool.
MatèriesComputer programming, C++ (Computer program language), Programació (Ordinadors), C++ (Llenguatge de programació)
TitulacióMÀSTER UNIVERSITARI EN COMPUTACIÓ (Pla 2006)
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
daniel_larraz.pdf | 577,6Kb | Visualitza/Obre |