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

TL;DR

This paper introduces a formal verification method for C programs with underspecified semantics by translating them into concurrent models, enabling automatic verification of all possible evaluation orders using existing tools.

Contribution

It presents a novel approach that reduces underspecified C semantics to concurrent non-determinism, allowing verification with standard tools without custom logic.

Findings

Successfully verified a highly underspecified C program case study.

Automatically extracted formal semantics and specifications from C code.

Ensured correctness for all evaluation orders using the Crowbar theorem prover.

Abstract

We present a novel and well automatable approach to formal verification of C programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain evaluations. First, we reduce this problem to non-determinism of concurrent systems, automatically extracting a distributed Active Object model from underspecified, sequential C code. This translation process provides a fully formal semantics for the considered C subset. In the extracted model every non-deterministic choice corresponds to one possible evaluation order. This step also automatically translates specifications in the ANSI/ISO C Specification Language (ACSL) into method contracts and object invariants for Active Objects. We then perform verification on the specified Active Objects model, using the Crowbar theorem prover, which verifies the extracted model with respect to the translated specification and ensures the original property of the C code for all possible evaluation orders. By using model extraction, we can use standard tools, without designing a new complex program logic to deal with underspecification. The case study used is highly underspecified and cannot be handled correctly by existing tools for C.