Bridging the Gap: Automatic Verified Abstraction of C

DOI10.1007/978-3-642-32347-8_8zbMath1360.68751OpenAlexW81956812MaRDI QIDQ2914735

June Andronick, David Greenaway, 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)

Related Items (11)

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

Uses Software

• Isabelle/HOL
• Frama-C
• VCC

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