@techreport{
    tPreoteasa06,
    author = "Preoteasa, Viorel",
    isbn = "952-12-1732-4",
    title = "Mechanical Verification of Mutually Recursive Procedures for Parsing Expressions using Separation Logic",
    abstract = "This paper adds support for mutually recursive procedures on top of a predicate transformer semantics of imperative programs with pointers implemented in PVS theorem prover. We define and prove correct a collection of mutually recursive procedures which constructs the parsing tree of an expression generated by a context free grammar. We use separation logic to specify and verify these procedures; the parsing tree is represented in memory using pointers and the specification predicates are defined using separation logic.",
    year = "2006",
    number = "771",
    lab = "Software Construction",
    month = "May",
    flags = "copy",
    address = "Turku, Finland",
    pdf = "TR771.pdf",
    institution = "{TUCS} - Turku Centre for Computer Science"
}