Rewriting
Symbolic Computation in Maude: Some Tapas (Invited Paper)
Runtime Complexity Analysis of Logically Constrained Rewriting
Con uence and Commutation for Nominal Rewriting Systems with Atom Variables
Pattern eliminating transformations
Unification
Nominal Uni cation with Letrec and Environment-Variables
Terminating Non-Disjoint Combined Unification
Types
slepice: Towards a Verified Implementation of Type Theory in Type Theory
Resourceful Program Synthesis from Graded Linear Types
Verification
On Constrained Horn Clauses and Program Veri cation (Invited Paper)
Algorithm Selection for Dynamic Symbolic Execution: a Preliminary Study
Translation of Interactive Datalog Programs for Microcontrollers to Finite State Machines
Model Checking and Probabilistic Programming
Generating Functions for Probabilistic Programs
Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs
Program Analysis and Testing
Testing Your (Static Analysis) Truths
Slicing unconditional jumps with unnecessary control dependencies
Logics
A Formal Model for a Linear Time Correctness Condition of Proof Nets of Multiplicative Linear Logic
Synthesis of Modality De nitions and a Theorem Prover for Epistemic Intuitionistic Logic.