Computer science/Programming languages/Logics
Subject Classification
ACM: Theory of computation~Programming logic
2025
2024
AutoCorres2
by Matthew Brecknell, David Greenaway, Johannes Hölzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch and Simon Wimmer
2023
Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties
by Thibault Dardinier
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs
by Thibault Dardinier
2022
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
by Thibault Dardinier
2021
Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations
by Walter Guttmann
2020
2019
Quantum Hoare Logic
by Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying and Naijun Zhan
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
by Simon Foster, Frank Zeyda, Yakoub Nemouchi, Pedro Ribeiro and Burkhart Wolff
2018
2017
2016
COMPLX: A Verification Framework for Concurrent Imperative Programs
by Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong
Separata: Isabelle tactics for Separation Algebra
by Zhe Hou, David Sanan, Alwen Tiu, Rajeev Gore and Ranald Clouston
Kleene Algebras with Domain
by Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth and Tjark Weber
2015
2014
Kleene Algebra with Tests and Demonic Refinement Algebras
by Alasdair Armstrong, Victor B. F. Gomes and Georg Struth
2013
2012
2011
2010
2008
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
by Norbert Schirmer