Semi-automated reasoning about non-determinism in C expressions

DOI10.1007/978-3-030-17184-1_3MaRDI QIDQ6091297zbMATH OpenOpenAlexFDO

Authors Dan Frumin, Léon Gondelman, Robbert Krebbers

Publication date 24 November 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17184-1_3

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• An operational and axiomatic semantics for non-determinism and sequence points in C
• VST-Floyd: a separation logic tool to verify correctness of C programs
• The problems of C program verification
• Towards verification of C programs. C-light language and its formal semantics
• Effective generation of verification conditions for non-deterministic unstructured programs

Cited in

(1)

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

This page was built for publication: Semi-automated reasoning about non-determinism in C expressions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6091297)