-
The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics
Authors:
Eduard Kamburjan,
Nathan Wasser
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…
▽ More
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.
△ Less
Submitted 9 August, 2022;
originally announced August 2022.
-
Teaching for large-scale Reproducibility Verification
Authors:
Lars Vilhuber,
Hyuk Harry Son,
Meredith Welch,
David N. Wasser,
Michael Darisse
Abstract:
We describe a unique environment in which undergraduate students from various STEM and social science disciplines are trained in data provenance and reproducible methods, and then apply that knowledge to real, conditionally accepted manuscripts and associated replication packages. We describe in detail the recruitment, training, and regular activities. While the activity is not part of a regular c…
▽ More
We describe a unique environment in which undergraduate students from various STEM and social science disciplines are trained in data provenance and reproducible methods, and then apply that knowledge to real, conditionally accepted manuscripts and associated replication packages. We describe in detail the recruitment, training, and regular activities. While the activity is not part of a regular curriculum, the skills and knowledge taught through explicit training of reproducible methods and principles, and reinforced through repeated application in a real-life workflow, contribute to the education of these undergraduate students, and prepare them for post-graduation jobs and further studies.
△ Less
Submitted 31 March, 2022;
originally announced April 2022.
-
Deductive Verification of Programs with Underspecified Semantics by Model Extraction
Authors:
Eduard Kamburjan,
Nathan Wasser
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…
▽ More
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.
△ Less
Submitted 11 February, 2022; v1 submitted 5 October, 2021;
originally announced October 2021.
-
Treating for-Loops as First-Class Citizens in Proofs
Authors:
Nathan Wasser,
Dominic Steinhöfel
Abstract:
Indexed loop scopes have been shown to be a helpful tool in creating sound loop invariant rules in dynamic logic for programming languages with abrupt completion, such as Java. These rules do not require program transformation of the loop body, as other approaches to dealing with abrupt completion do. However, indexed loop scopes were designed specifically to provide a loop invariant rule for whil…
▽ More
Indexed loop scopes have been shown to be a helpful tool in creating sound loop invariant rules in dynamic logic for programming languages with abrupt completion, such as Java. These rules do not require program transformation of the loop body, as other approaches to dealing with abrupt completion do. However, indexed loop scopes were designed specifically to provide a loop invariant rule for while loops and work rather opaquely. Here we propose replacing indexed loop scopes with a more transparent solution, which also lets us extend this idea from while loops to for loops. We further present sound loop unrolling rules for while, do and for loops, which require neither program transformation of the loop body, nor the use of nested modalities. This approach allows for loops to be treated as first-class citizens in proofs -- rather than the usual approach of transforming for loops into while loops -- which makes semi-automated proofs more transparent and easier to follow for the user, whose interactions may be required in order to close the proofs.
△ Less
Submitted 3 February, 2020;
originally announced February 2020.
-
Technical Report: Using Loop Scopes with for-Loops
Authors:
Nathan Wasser,
Dominic Steinhöfel
Abstract:
Loop scopes have been shown to be a helpful tool in creating sound loop invariant rules which do not require program transformation of the loop body. Here we extend this idea from while-loops to for-loops and also present sound loop unrolling rules for while- and for-loops, which require neither program transformation of the loop body, nor the use of nested modalities. This approach allows for-loo…
▽ More
Loop scopes have been shown to be a helpful tool in creating sound loop invariant rules which do not require program transformation of the loop body. Here we extend this idea from while-loops to for-loops and also present sound loop unrolling rules for while- and for-loops, which require neither program transformation of the loop body, nor the use of nested modalities. This approach allows for-loops to be treated as first-class citizens -- rather than the usual approach of transforming for-loops into while-loops -- which makes semi-automated proofs easier to follow for the user, who may need to provide help in order to finish the proof.
△ Less
Submitted 24 January, 2019; v1 submitted 21 January, 2019;
originally announced January 2019.
