Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties by Thibault Dardinier Apr 03
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs by Thibault Dardinier Mar 15
A Hoare Logic for Diverging Programs by Johannes Åman Pohjola, Magnus O. Myreen and Miki Tanaka Jan 20
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand by Thibault Dardinier May 30
Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations by Walter Guttmann Oct 12
Quantum Hoare Logic by Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying and Naijun Zhan Mar 24
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming by Simon Foster, Frank Zeyda, Yakoub Nemouchi, Pedro Ribeiro and Burkhart Wolff Feb 01
COMPLX: A Verification Framework for Concurrent Imperative Programs by Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong Nov 29
Separata: Isabelle tactics for Separation Algebra by Zhe Hou, David Sanan, Alwen Tiu, Rajeev Gore and Ranald Clouston Nov 16
Kleene Algebras with Domain by Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth and Tjark Weber Apr 12
Kleene Algebra with Tests and Demonic Refinement Algebras by Alasdair Armstrong, Victor B. F. Gomes and Georg Struth Jan 23
Semantics and Data Refinement of Invariant Based Programs by Viorel Preoteasa and Ralph-Johan Back May 28
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment by Norbert Schirmer Feb 29