4 papers
Domain Theory Meets Interaction Trees in Rocq
David Nowak, Vlad Rusu
We present a domain-theoretical formalization of interaction trees in the Rocq prover. Unlike existing formalizations, ours does not rely on Rocq's built-in coinduction. Hence, we…
Proceedings of the Sixth Working Formal Methods Symposium
Vlad Rusu
It is our pleasure to present the papers of the sixth Working Formal Methods Symposium (FROM 2022) held at the "Al. I. Cuza" university of Iasi, Romania on September 19-20, 2022. F…
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
Vlad Rusu, David Nowak
Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems…
Proceedings Second International Workshop on Algebraic Methods in Model-based Software Engineering
Francisco Durán, Vlad Rusu
Over the past years there has been quite a lot of activity in the algebraic community about using algebraic methods for providing support to model-driven software engineering. The…