Title :
Combining Logic and Algebraic Techniques for Program Verification in Theorema
Author :
Kovacs, Levente ; Popov, Nikolaj ; Jebelean, Tudor
Author_Institution :
Johannes Kepler Univ., Linz
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;
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
DOI :
10.1109/ISoLA.2006.46
