Ranan Fraer
Welcome to my page, a collection of things I'm quite sure are interesting only to me. In case you wonder how my thesis is going ... Although its completion might require an unpredictable amount of time, the results up to date have been astonishing, to say the least !
Education:
If you're interested in employing me, or just need a good laugh, you can
read my CV (english or
french version).
Research interests:
The typical program verification sytem 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.
Personally, I'm 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. Not surprisingly, B tools are
already marketed by two competing software houses. So, if you're in need of a formal
method, do yourself a favour and take a look at B !
Anyway, 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: