Research
Formal Models for developing and verifying software, Software Engineering, Formal Verification.
Biography
I am a computer science researcher on Formal Methods for Developing and Verifying Software. I am interested mainly in developing tools to make the use of formal methodologies easier. Some of the works I’ve been involved are the formal definition and implementation of the EventB2Java tool. A tool that enables users to start the development of software in Event-B (a stepwise refinement approach) where users can model the system and prove it consistently, to then transition to JML-annotated Java code (a Design-by-Contract approach) where users can continue the development of the software. I am currently working on the design and its corresponding implementation of two calculi: (i) AutoAlias, to automatically infer aliasing in OO programs, and (ii) AutoFrame, to automatically infer frame conditions, frame locations that OO programs are allowed to change (a.k.a the Framing problem). I am also working on using mathematical reasoning to prove properties on legal documents (e.g. Legislation).