Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts

This conference talk explores a novel approach to validating the correctness of concurrent programs through a witness format that uses ghost statements. Learn how researchers from multiple European universities address the challenge of exchanging information between different static analyzers that use varying semantics for concurrent program analysis. The presentation explains how the proposed format embeds claims about program correctness into modified programs with ghosts, allowing for consistent validation across both interleaving and thread-modular semantics. Discover the evaluation results showing that 75% of ghost witnesses generated for SV-COMP benchmark programs were successfully confirmed by a model checker, demonstrating the format's effectiveness in bridging the semantic divide between different analysis approaches. Presented at the VMCAI conference in January 2025 and sponsored by ACM SIGPLAN, this 32-minute talk provides valuable insights for researchers and practitioners working on program verification and static analysis.