Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. - Néstor Cataño; Marieke Huisman (FME, 2002)

CHASE: A Static Checker for JML's Assignable Clause. - Néstor Cataño; Marieke Huisman (VMCAI, 2003)

Slicing Event Spaces: Towards a Java Programs Checking Framework. - Néstor Cataño (FMICS, 2003)

Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS. - Néstor Cataño (TPHOLs, 2005)

Combining Symbolic Execution and Model Checking to Reduce Dynamic Program Analysis Overhead. - Néstor Cataño (Rev. Colomb. de Computación, 2005)

Formal methods for smart cards: an experience report. - Cees-Bart Breunesse; Néstor Cataño; Marieke Huisman; Bart Jacobs 001 (Sci. Comput. Program., 2005)

A Case Study in JML-Assisted Software Development. - Néstor Cataño; Fernando Barraza; Daniel García; Pablo Ortega; Camilo Rueda (SBMF, 2008)

Executing JML specifications of Java card applications: a case study. - Néstor Cataño; Tim Wahls (SAC, 2009)

Teaching Formal Methods for the Unconquered Territory. - Néstor Cataño; Camilo Rueda (TFM, 2009)

Matelas: A Predicate Calculus Common Formal Definition for Social Networking. - Néstor Cataño; Camilo Rueda (ASM, 2010)

A Machine-Checked Proof of A State-Space Construction Algorithm. - Néstor Cataño; Radu I. Siminiceanu (NASA Formal Methods, 2010)

Lightweight Verification of a Multi-Task Threaded Server: A Case Study With The Plural Tool. - Néstor Cataño; Ijaz Ahmed (FMICS, 2011)

The EventB2Dafny rodin plug-in. - Néstor Cataño; K. Rustan M. Leino; Víctor Rivera (TOPI@ICSE, 2012)

A linear concurrent constraint approach for the automatic verification of access permissions. - Carlos Olarte; Elaine Pimentel; Camilo Rueda; Néstor Cataño (PPDP, 2012)

Translating B machines to JML specifications. - Néstor Cataño; Tim Wahls; Camilo Rueda; Víctor Rivera; Danni Yu (SAC, 2012)

Poporo: A Formal Methods Tool for Fast-Checking of Social Network Privacy Policies. - Néstor Cataño; Sorren Hanvey; Camilo Rueda (TOOLS (50), 2012)

Automated Verification of Specifications with Typestates and Access Permissions. - Radu I. Siminiceanu; Ijaz Ahmed; Néstor Cataño (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

A Machine-Checked Proof for a Translation of Event-B Machines to JML. - Néstor Cataño; Camilo Rueda; Tim Wahls (CoRR, 2013)

Translating event-B to JML-specified Java programs. - Víctor Rivera; Néstor Cataño (SAC, 2014)

A case study on the lightweight verification of a multi-threaded task server. - Néstor Cataño; Ijaz Ahmed; Radu I. Siminiceanu; Jonathan Aldrich (Sci. Comput. Program., 2014)

Identifying Transitivity Threats in Social Networks. - Sorren Hanvey; Néstor Cataño (TELERISE@ICSE, 2015)

A Case Study on Code Generation of an ERP System from Event-B. - Néstor Cataño; Tim Wahls (QRS, 2015)

Undertaking the tokeneer challenge in event-b. - Victor Rivera; Sukriti Bhattacharya; Néstor Cataño (FormaliSE@ICSE, 2016)

Soundness Proof of EventB2Java. - Néstor Cataño; Shigeo Nishi (LADC, 2016)

EventB2Java: A Code Generator for Event-B. - Néstor Cataño; Victor Rivera (NFM, 2016)

An Empirical Study on Teaching Formal Methods to Millennials. - Néstor Cataño (SECM@ICSE, 2017)

Code generation for Event-B. - Victor Rivera; Néstor Cataño; Tim Wahls; Camilo Rueda (Int. J. Softw. Tools Technol. Transf., 2017)

Checking JML-encoded finite state machine properties. - Ijaz Ahmed; Néstor Cataño (ICACS, 2018)

Improving the Reliability of Mobility Applications. - Néstor Cataño (CoRR, 2018)

A Logical Framework for Verifying Privacy Breaches of Social Networks. - Néstor Cataño (CoRR, 2018)

Engaging Millennials into Learning Formal Methods. - Néstor Cataño (CoRR, 2018)

Teaching Formal Methods: Lessons Learnt from Using Event-B. - Néstor Cataño (FMTea, 2019)

A Methodological Approach to Verify Architecture Resiliency. - Joanna C. S. Santos; Selma Suloglu; Néstor Cataño; Mehdi Mirakhorli (ECSA (Tracks and Workshops), 2022)

Program Synthesis for Cyber-Resilience. - Néstor Cataño (IEEE Trans. Software Eng., 2023)

pyeb: A Python Implementation of Event-B Refinement Calculus. - Néstor Cataño (CoRR, 2025)