@inproceedings{
    inpPr06,
    editor = "Misra, J. and Nipkow, T. and Sekerinski, E.",
    author = "Preoteasa, Viorel",
    publisher = "Springer",
    title = "Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada",
    year = "2006",
    lab = "Software Construction",
    month = "Aug",
    volume = "4085",
    flags = "copy",
    address = "Berlin / Heidelberg",
    abstract = "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 prover. The theory, including the proofs, is implemented in the theorem prover PVS.",
    pdf = "inpPr06.pdf",
    pages = "508 - 523"
}