Chris Poskitt will review the literature relevant to his research topic,
"Verification of Graph Programs". After a brief refresher on Hoare
logic and the graph programming language GP, a number of for-
malisms for specifying graph properties will be reviewed, including
nested graph conditions, and the powerful monadic second-order
logic. Finally, the latest work done to apply these formalisms to the
verification of graph programs will be reviewed, and areas for future
work will briefly be exposed.
Jason Reich will discuss research pertaining to the "Formal Verifi-
cation of Functional Language Implementations". The seminar will
cover the rationale for proving compiler correctness, a selection of
formal verification methodologies and the tools and languages as-
sociated with these methodologies. Existing projects investigating
compiler correctness will be examined and their approaches evalu-
ated against project goals.
Hello! I am a Ph.D. research student in the Department of Computer Science at The University of York, where I am a member of the PLASMA research group.
Under the supervision of Dr. Detlef Plump, my research will focus on the formal verification of graph programs (our original proposal provides some more information).
My reading list is available online, and should provide a good indication of my research interests.