Nestor Catano

I am a software engineer and a computer scientist; my main research area is the use of formal methods for software engineering. I specialise in program specification and verification using JML and design-by-contract, and in a formal method called Event-B. My main research goal is to use formal methods techniques and to develop software tools that improve the quality of software systems. My main tool contributions are the design and implementation of the EventB2Java and EventB2JML code generators; the design and implementation of the EventB2Dafny Proof Obligation generator, and the design and implementation of the Chase syntactic checker of JML's assignable clause. My research work with EventB2Dafny was funded by Microsoft Research through the SEIF program in 2011.

I earned a Master Degree and a PhD in Computer Science from The University Paris 7. I am currently attending the MICS Master in CyberSecurity at UC Berkeley.

I am the proud designer of the EventB2Java Java code generator for Event-B, a Rodin plugin that generates implementation of Event-B models. If you are interested in installing and using EventB2Java, drop me an email to nescatano at hotmail dot com and I will send you the address of EventB2Java update site.

My proposal for a workshop on Formal Methods for Blockchains was accepted and will take place as part of the Formal Methods world congress https://sites.google.com/view/fmbc/

My research publications can be reached from the DBLP repository or Google Scholar.

Past Research Projects

• EventB2Dafny: Extending Boogie to Support the Analysis of B Machines, research funded through the SEIF program of Microsoft Research.

• AEminium: Freeing Programmers from the Shackles of Sequentiality, funded by CMU-Portugal

• WeSP: Web Security and Privacy, funded by CMU-Portugal

• Favas: A Formal Verification Platform for Real-time Systems, funded by FCT, Portugal.