Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove consistent Hoare total correctness rules for pointer manipulating statements according to the predicate transformer semantics. We prove the frame rule in the context of a programming language with recursive procedures with value and result parameters and local variables, where program variables and addresses can store values of any type of the theorem proven The theory, including the proofs, is implemented in the theorem prover PVS. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Preoteasa, V. (2006). Mechanical verification of recursive procedures manipulating pointers using separation logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4085 LNCS, pp. 508–523). Springer Verlag. https://doi.org/10.1007/11813040_34
Mendeley helps you to discover research relevant for your work.