Proving properties of programs using automatically generated models.

Description
Title: Proving properties of programs using automatically generated models.
Authors: Binard, Franck J. L.
Date: 2002
Abstract: This thesis describes a method for automatically generating theories in a first order logic with arithmetic for the purpose of proving properties about the programs. We build the logic and define the syntactic model generation algorithm. The models can be used to prove a substantial class of properties that are true of the programs they are generated from. Here, a model is a set of formulas of the logic that are interpreted as mathematical function definitions. These functions describe the computation steps of the algorithm.
URL: http://hdl.handle.net/10393/6098
http://dx.doi.org/10.20381/ruor-11094
CollectionTh├Ęses, 1910 - 2010 // Theses, 1910 - 2010
Files
MQ76565.PDF3.82 MBAdobe PDFOpen