Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity

DOI10.1007/978-3-662-46669-8_14zbMath1335.68067arXiv1410.0306OpenAlexW1533529458MaRDI QIDQ2802440

Aleksandar Nanevski, Ilya Sergey, Anindya Banerjee

Publication date: 26 April 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1410.0306

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Connecting Higher-Order Separation Logic to a First-Order Outside World ⋮ A perspective on specifying and verifying concurrent modules ⋮ Higher-order linearisability ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Abstract Specifications for Concurrent Maps ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Coq

This page was built for publication: Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity