Victor Rivera

简介

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 condi