Néstor Cataño

Associate Professor in Computer Science

Innopolis University
Software Engineering Lab
Master MSIT/SE with CMU
1 Universitetskaya, 420500
Innopolis, Tatarstan, Russia
Office 410
n.catano at innopolis.ru

I am a Computer Scientist, a Formal Methods Researcher and a Lecturer in Software Engineering and Formal Methods. I earned a Master degree and a PhD degree in Computer Science from The University Paris 7, and INRIA Sophia Antipolis, in France. I am currently an Associate Professor in Computer Science and Software Engineering at Innopolis University in Kazan, Tatarstan, Russian Federation. Previously, I was a Lecturer at University of Madeira, in Portugal, and Universities Andes, EAFIT, and Javeriana in Colombia. I was an invited professor to CMU in Pittsburgh in 2011 and in 2015.

I am the proud main designer and co-implementer of the EventB2Java Java code generator for Event-B. EventB2Java is implemented as a Rodin plug-in. I also designed and implemented sibling tools EventB2Jml and B2Jml . These tools are implemented in Java as plug-ins of Eclipse and ABToools, respectively. In 2011, I received research funding from the SEIF research program of Microsoft Research to port Event-B refinement proof obligations into Dafny and Boogie. As a result of this work, I designed and implemented the EventB2Dafny tool (check all my software tools). In a previous life, I designed and implemented the Chase tool, a static checker of JML’s modifiable clause that checks Java programs for side effects. I have been the project coordinator of several European national Research Projects on Formal Methods, Concurrency, and Software Engineering.

I co-authored a chapter entitled "On the Use of Formal Methods to Enforce Privacy-Aware Social Networking" of the book "Social Network Engineering for Secure Web Data Services" that you can find here.

Former PhD Students