Computer science/Data management systems

Formalization of (Conflict-)Serializability and Strict Two-Phase Locking

by Dmitriy Traytel

A Verified Proof Checker for Metric First-Order Temporal Logic

by Andrei Herasimau, Jonathan Julian Huerta y Munive, Leonardo Lima, Martin Raszyk and Dmitriy Traytel

Verification of Query Optimization Algorithms

by Lukas Stevens and Bernhard Stöckl

Making Arbitrary Relational Calculus Queries Safe-Range

by Martin Raszyk and Dmitriy Traytel

First-Order Query Evaluation

by Martin Raszyk

A Verified Imperative Implementation of B-Trees

by Niels Mündler

Formalization of Multiway-Join Algorithms

by Thibault Dardinier