To access the full text documents, please follow this link: http://hdl.handle.net/2099.1/12693

Automatic generation of loop invariants
Larraz Hurtado, Daniel
Rubio, Alberto
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.
Àrees temàtiques de la UPC::Informàtica::Enginyeria del software
Computer programming
C++ (Computer program language)
CppInv
C++
SMT Formulas
Transition System
Programació (Ordinadors)
C++ (Llenguatge de programació)
Attribution-NonCommercial-NoDerivs 3.0 Spain
http://creativecommons.org/licenses/by-nc-nd/3.0/es/
info:eu-repo/semantics/masterThesis
Universitat Politècnica de Catalunya
         

Show full item record

Related documents

Other documents of the same author

Candeago, L.; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Larraz Hurtado, Daniel; Nimkar, Kaustubh; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
 

Coordination

 

Supporters