.- Regular Papers.
.- Verifying Invariants by Deductive Model Checking.
.- Time-Bounded Resilience.
.- Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ.
.- Equivalence, and Property Internalization and Preservation for Equational Programs.
.- Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude.
.- Unified Opinion Dynamic Modeling as Concurrent Set Relations in Rewriting Logic.
.- Timed Strategies for Real-Time Rewrite Theories.
.- Specifying Fairness Constraints and Model Checking with Non-intensional Strategies.
.- Tool Papers.
.- The hrewrite Library: a Term Rewriting Engine for Automatic Code Assembly.
.- A Flexible Framework for Integrating Maude and SMT Solvers Using Python.
.- Education Papers.
.- Teaching an Advanced Maude-based Formal Methods Course in Oslo.