Deductive Verification of Programs with Underspecified Semantics by Model Extraction

TL;DR

This paper introduces a method for verifying programs with underspecified semantics by extracting a formal distributed Active Object model from C code, enabling the use of standard tools for verification across all evaluation orders.

Contribution

It presents a novel automated approach that reduces underspecified program semantics to a formal model, facilitating verification with existing tools.

Findings

Successfully verified highly underspecified C code.

Automatically translated specifications into method contracts and invariants.

Ensured correctness across all evaluation orders.

Abstract

We present a novel and well automatable approach to formal verification of 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 distributed 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. For this we have implemented a theorem prover Crowbar based on the Behavioral Program Logic (BPL), 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 verified with existing tools for C.