• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Mechanical Verification of Mutually Recursive Procedures for Parsing Expressions using Separation Logic

Viorel Preoteasa, Mechanical Verification of Mutually Recursive Procedures for Parsing Expressions using Separation Logic. TUCS Technical Reports 771, Turku Centre for Computer Science, 2006.

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.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tPreoteasa06b,
  title = {Mechanical Verification of Mutually Recursive Procedures for Parsing Expressions using Separation Logic},
  author = {Preoteasa, Viorel},
  number = {771},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2006},
  keywords = {Pointer Programs. Separation Logic. Mutually Recursive Procedures.},
  ISBN = {952-12-1732-4},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication