Activities

DM-Check: Verifying invariants of concurrent systems by deductive model checking

Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, José Meseguer and Julia Sapiña

PROLE 2026Conference presentation

Generating Invariants by Deductive Model Checking

Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, José Meseguer and Julia Sapiña

WRLA 2026Università di Torino · Torino, Italy

Folding Narrowing for the Analysis of Mutual Exclusion Protocols

PPDP 2025Università della Calabria · Rende, Italy

Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints

IMT Lucca–ELP MeetingValencia, Spain

Research stay as a PhD student

Japan Advanced Institute of Science and Technology (JAIST)Nomi, Japan · supervised by Prof. Kazuhiro Ogata

Research stay as a PhD student

Japan Advanced Institute of Science and Technology (JAIST)Nomi, Japan · supervised by Prof. Kazuhiro Ogata

Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints

FTSCS 2023Cascais, Portugal

Canonical Narrowing for Variant-Based Conditional Rewrite Theories

PROLE 2023Universidad de Castilla-La Mancha · Ciudad Real, Spain

Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method

JNIC 2023Sede Afundación · Vigo, Spain

Summer School Assistant

13th International School on Rewriting (ISR 2022)Tbilisi State University · Tbilisi, Georgia

An Efficient Canonical Narrowing Implementation for Protocol Analysis

PROLE 2022Universidad de Santiago de Compostela · Spain

An Efficient Canonical Narrowing Implementation for Protocol Analysis

WRLA 2022Technical University of Munich · Germany

Volunteer Collaborator

PROLE 2021 / CEDI 2021Universidad de Málaga · Spain

Summer School Assistant

12th International School on Rewriting (ISR 2021)Universidad Complutense de Madrid · Spain