Bridging the Gap: Automatic Verified Abstraction of C

DOI10.1007/978-3-642-32347-8_8zbMATH Open1360.68751OpenAlexW81956812MaRDI QIDQ2914735FDOQ2914735

Authors D. Greenaway, June Andronick, Gerwin Klein

Publication date 20 September 2012

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-32347-8_8

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstraction and subsumption in modular verification of C programs
• Integrated and automated abstract interpretation, verification and testing of C/C++ modules
• scientific article; zbMATH DE number 1953018
• scientific article; zbMATH DE number 1696591
• Towards verification of C\(\#\) programs: a three-level approach
• Lifting CDCL to template-based abstract domains for program verification

Cited in

(11)

• Parameterized synthesis for fragments of first-order logic over data words
• Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
• Formalizing the Edmonds-Karp algorithm
• A concrete memory model for CompCert
• Highly automated formal proofs over memory usage of assembly code
• Cogent: uniqueness types and certifying compilation
• A framework for the verification of certifying computations
• A learning-based fact selector for Isabelle/HOL
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Trustworthy Graph Algorithms (Invited Talk)

Describes a project that uses

Uses Software

• Isabelle/HOL
• Frama-C
• VCC

This page was built for publication: Bridging the Gap: Automatic Verified Abstraction of C

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