DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2026.21

Foundational and Compositional Verification of Layered Concurrent Objects

Authors: Yicheng Ni and Yuting Wang

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract

Compositionality is essential for managing complexity in verification of concurrent programs, especially when proof certificates are needed. An effective verification scheme is to divide programs into abstraction layers and verify by composing refinements between layers. However, vanilla verified layers come with global states which severely limit their extensibility. This problem may be solved by dividing a layer into objects with encapsulated local states. Although the idea has been successfully realized in the sequential setting, it remains unclear if it also works in a concurrent setting where function calls across layers are no longer atomic steps and foundational proofs are needed. We propose an approach to foundational and compositional verification of concurrent objects organized into multiple layers. The central idea is to represent concurrent objects as open labeled transition systems with encapsulated threads and to adopt trace refinements as a uniform notion of functional correctness which supports both vertical composition (layered refinement) and horizontal composition (extension of layer interfaces). Due to the operational nature of transition systems, it is straightforward to adopt traditional simulation techniques to produce foundational proof certificates. We implement this framework in the Rocq theorem prover and demonstrate its capability in foundational and compositional verification by verifying non-trivial lock-free concurrent data structures.

Cite as

Yicheng Ni and Yuting Wang. Foundational and Compositional Verification of Layered Concurrent Objects. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 21:1-21:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ni_et_al:LIPIcs.ECOOP.2026.21,
  author =	{Ni, Yicheng and Wang, Yuting},
  title =	{{Foundational and Compositional Verification of Layered Concurrent Objects}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{21:1--21:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.21},
  URN =		{urn:nbn:de:0030-drops-261171},
  doi =		{10.4230/LIPIcs.ECOOP.2026.21},
  annote =	{Keywords: Concurrency, Compositional Verification}
}

Document

Artifact

DOI: 10.4230/DARTS.12.1.16

Foundational and Compositional Verification of Layered Concurrent Objects (Artifact)

Authors: Yicheng Ni and Yuting Wang

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract

This document provides artifact description for the ECOOP 2026 paper "Foundational and Compositional Verification of Layered Concurrent Objects".

Cite as

Yicheng Ni and Yuting Wang. Foundational and Compositional Verification of Layered Concurrent Objects (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{ni_et_al:DARTS.12.1.16,
  author =	{Ni, Yicheng and Wang, Yuting},
  title =	{{Foundational and Compositional Verification of Layered Concurrent Objects (Artifact)}},
  pages =	{16:1--16:11},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Ni, Yicheng and Wang, Yuting},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.16},
  URN =		{urn:nbn:de:0030-drops-261531},
  doi =		{10.4230/DARTS.12.1.16},
  annote =	{Keywords: Formal Verification, Concurrency, Formalization, Rocq}
}

Search Results

Documents authored by Ni, Yicheng

Foundational and Compositional Verification of Layered Concurrent Objects

Abstract

Cite as

Foundational and Compositional Verification of Layered Concurrent Objects (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message