Néstor Cataño

PhD University Paris 7 and INRIA, France, 2004


Néstor Cataño currently works as an Assistant Professor in the department of Mathematics and Engineering of The University of Madeira, Portugal, where he teaches courses on Software Engineering, Programming Languages, and Human Computer. In spring 2010, he worked as a visiting professor at the Institute of Software Research (ISR) and the Human Computer Interaction Institute (HCII) of Carnegie Mellon University (CMU) in Pittsburgh. He participates of CMU-Portugal.

Néstor Cataño’s major interests in research are in Formal Methods (e.g. for critical systems, social networks). In particular, he is interested in formal specification and verification of programs using Java and JML (Java Modeling Language). He currently works in a predicate calculus definition for social networking and in the use of refinement calculus in B to develop a social-network core application implementing common privacy and security social network policies.

He also works in the design and implementation of the B2JML tool, a tool that translates B machines into JML abstract class specifications. He currently works in a translation of JML with generics into the input language of the Yices SMT solver. He has being using PVS for the modeling and correctness proof of algorithms during the last 10 years.

Néstor Cataño’s is an enthusiastic and experienced user of formal methods tools such as JML, AtelierB, and PVS. He is recently using The Plural Tool to specify and verify a Multi-Task Thread Server application (see a case study with Plural).

Néstor Cataño holds a Master Degree and a PhD from The University of Paris 7. During his PhD he was hosted at the Lemme research group at INRIA Sophia-Antipolis. After finishing his PhD, he worked as a Research Associate at The University of York.



The University of Madeira

Campus Universitário da Penteada, 9000-390

Funchal, Madeira, Portugal

ncatano at uma dot pt