The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics

DOI10.4204/eptcs.365.1arXiv2208.04630MaRDI QIDQ6122639

Nathan Wasser, Eduard Kamburjan

Publication date: 1 March 2024

Published in: Electronic Proceedings in Theoretical Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Unnamed Item
• Compositional reasoning about active objects with shared futures
• An overview of the K semantic framework
• Behavioral program logic
• An operational and axiomatic semantics for non-determinism and sequence points in C
• Semi-automated reasoning about non-determinism in C expressions

This page was built for publication: The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics