Victor Rivera

Visiting Fellow


Formal Models for developing and verifying software, Software Engineering, Formal Verification.


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).

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

bars search times arrow-up