Provably Correct Flow Graph Extraction for Boolean Programs
Boolean programs are an established model for software analysis that is
expressive enough to represent features in common programming languages
and is amenable to model checking [BR00]. Boolean
flow graphs are a graphical model of Boolean programs that is suitable
for capturing the structure and behaviour of such programs [Sol11]. In
particular, such models are suitable for the verification of temporal
properties, and will be used to extend an existing method and tool set
for compositional verification of software [HG10].
Tasks:
- Define formally Boolean programs
- the formal syntax as presented in Stefan Schoon's PhD Thesis [Sch02] (pages 185-190)
- the small-step operational semantics (a standard exercise)
- Define formally Boolean flow graphs: structure and behaviour
- as in [Sol11]
- follows the philosophy described in [HAG08]
- Define formally a translation from Boolean programs to Boolean flow graphs
- Prove correctness of the translation:
- show that the extracted flow graph is bisimilar to the original program (a standard exercise)
- Implement the translation in OCaml
- Perform a program verification exercise (with support from Siavash):
- write a Boolean program
- specify an important program property in LTL
- extract a Boolean flow graph from the program
- convert the flow graph to a pushdown system
- use Moped to model check the pushdown system against the LTL specification
Last modified: 24 August 2011