DocumentCode
3143828
Title
Combining Logic and Algebraic Techniques for Program Verification in Theorema
Author
Kovacs, Levente ; Popov, Nikolaj ; Jebelean, Tudor
Author_Institution
Johannes Kepler Univ., Linz
fYear
2006
fDate
15-19 Nov. 2006
Firstpage
67
Lastpage
74
Abstract
We study and implement concrete methods for the verification of both imperative as well as functional programs in the frame of the Theorema system. The distinctive features of our approach consist in the automatic generation of loop invariants (by using combinatorial and algebraic techniques), and the generation of verification conditions as first-order logical formulae which do not refer to a specific model of computation.
Keywords
functional programming; process algebra; program verification; Theorema system; algebraic techniques; first-order logical formulae; functional programs; logic techniques; loop invariants; program verification; Algebra; Combinatorial mathematics; Computational modeling; Concrete; Difference equations; Functional programming; Logic devices; Logic functions; Polynomials; Problem-solving;
fLanguage
English
Publisher
ieee
Conference_Titel
Leveraging Applications of Formal Methods, Verification and Validation, 2006. ISoLA 2006. Second International Symposium on
Conference_Location
Paphos
Print_ISBN
978-0-7695-3071-0
Type
conf
DOI
10.1109/ISoLA.2006.46
Filename
4463696
Link To Document