Computer science/Programming languages/Logics

Subject Classification

ACM: Theory of computation~Programming logic

AMS: Computer science / Theory of computing / Specification and verification (program logics, model checking, etc.)

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

Apr 17

2023

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

Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion

by Andrei Popescu

Feb 28

A Hoare Logic for Diverging Programs

by Johannes Åman Pohjola, Magnus O. Myreen and Miki Tanaka

Jan 20

2022

Unbounded Separation Logic

by Thibault Dardinier

Sep 05

A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand

by Thibault Dardinier

May 30

Formalization of a Framework for the Sound Automation of Magic Wands

by Thibault Dardinier

May 18

2021

Quantum and Classical Registers

by Dominique Unruh

Oct 28

Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations

by Walter Guttmann

Oct 12

2020

An Under-Approximate Relational Logic

by Toby Murray

Mar 12

2019

Differential Game Logic

by André Platzer

Jun 03

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

IMP2 – Simple Program Verification in Isabelle/HOL

by Peter Lammich and Simon Wimmer

Jan 15

2018

Hoare Logics for Time Bounds

by Maximilian P. L. Haslbeck and Tobias Nipkow

Feb 26

2017

Differential Dynamic Logic

by Rose Bohrer

Feb 13

2016

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

2015

Concurrent IMP

by Peter Gammie

Apr 13

2014

Formalization of Refinement Calculus for Reactive Systems

by Viorel Preoteasa

Oct 08

Kleene Algebra with Tests and Demonic Refinement Algebras

by Alasdair Armstrong, Victor B. F. Gomes and Georg Struth

Jan 23

2013

Automatic Data Refinement

by Peter Lammich

Oct 02

Ribbon Proofs

by John Wickerson

Jan 19

Kleene Algebra

by Alasdair Armstrong, Georg Struth and Tjark Weber

Jan 15

2012

A Separation Logic Framework for Imperative HOL

by Peter Lammich and Rene Meis

Nov 14

Separation Algebra

by Gerwin Klein, Rafal Kolanski and Andrew Boyton

May 11

2011

A Definitional Encoding of TLA* in Isabelle/HOL

by Gudmund Grov and Stephan Merz

Nov 19

Algebra of Monotonic Boolean Transformers

by Viorel Preoteasa

Sep 22

2010

Semantics and Data Refinement of Invariant Based Programs

by Viorel Preoteasa and Ralph-Johan Back

May 28

2008

A Bytecode Logic for JML and Types

by Lennart Beringer and Martin Hofmann

Dec 12

Secure information flow and program logics

by Lennart Beringer and Martin Hofmann

Nov 10

A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment

by Norbert Schirmer

Feb 29

2006

Abstract Hoare Logics

by Tobias Nipkow

Aug 08