Ranan Fraer
Education:
Research interests:
The typical program verification system is a batch tool that accepts
as input a program annotated with Floyd-Hoare assertions, performs syntactic
and semantic analysis on it, and generates a list of verification conditions
that is subsequently submitted to a theorem prover. However, when a verification
condition cannot be proved, this may be due to an error in the program
or an inconsistency in the annotations. Unfortunately, it is very difficult
to relate a failing proof attempt to a particular piece of code or assertion.
My research deals with using debugging-like features in order to reestablish
the link between verification conditions and the source program. This way,
techniques like origin tracking and program slicing find new applications
in the context of program verification. More generally, I'm interested
in the interaction between various static analysis techniques based on
dependence graphs and program verification. The overall goal would be to
use Floyd-Hoare invariants not only in verification but also in debugging
and maintenance of programs.
I'm also an enthusiastic supporter of Jean-Raymond Abrial's B
method. There's a growing interest in B, as it has been already successfully
applied on several large-scale industrial projects in France and UK. Here
are some of my favourite Formal Methods links:
Oh,
I forgot. Work. Yes, I have some papers online:
Rocka Rolla !
Here are some links to my favourite bands: