- On a simple problem due to Yves Bertot.- Verifying Neural Networks with PyRAT.- Contextual Equality Saturation.- A Programming Language for Feasible Solutions.- Specifying and Verifying Future Conditions.- AURA: Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty.- Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis.- Bounded-Exhaustive Subspace Diversification for SMT Solver Testing.

- Abstracting Concolic Execution for Soft Contract Verification.- Enhancing Neural Network Robustness via Synthesis of Repair Programs.- Relating Distances and Abstractions: An Abstract Interpretation Perspective.- Ductape: Optimizing Dynamically Typed Programs Using Ahead-of-Time Compilation and Data-Flow Analysis.- Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types.- Formal Analysis of Networked PLC Controllers Interacting with Physical Environments.- Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell.- Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters.