Proving properties of programs using automatically generated models.

dc.contributor.advisor	Felty, Amy,
dc.contributor.author	Binard, Franck J. L.
dc.date.accessioned	2009-03-23T13:00:59Z
dc.date.available	2009-03-23T13:00:59Z
dc.date.created	2002
dc.date.issued	2002
dc.degree.level	Masters
dc.degree.name	M.C.S.
dc.description.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.
dc.format.extent	162 p.
dc.identifier.citation	Source: Masters Abstracts International, Volume: 41-05, page: 1460.
dc.identifier.isbn	9780612765658
dc.identifier.uri	http://hdl.handle.net/10393/6098
dc.identifier.uri	http://dx.doi.org/10.20381/ruor-11094
dc.publisher	University of Ottawa (Canada)
dc.subject.classification	Computer Science.
dc.title	Proving properties of programs using automatically generated models.
dc.type	Thesis

Files

Now showing 1 - 1 of 1