6 citations · 6 across the 2 of their papers we have counts for
3 papers
Multi-language Program Logics
Alexander Loitzl, Niklas Mück, Michael Sammler
Real-world programs are rarely written in a single language: For example, C programs call assembly routines, and high-level languages like OCaml link with low-level C libraries. Ye…
Iris in Lean
Markus de Medeiros, Sergei Stepanenko, Zongyuan Liu +9
The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-…
Formal Foundations for Translational Separation Logic Verifiers (extended version)
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy +2
Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3.…