Bridging the Gap: Automatic Verified Abstraction of C
From MaRDI portal
Publication:2914735
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
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
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (11)
- A Concrete Memory Model for CompCert
- Cogent: uniqueness types and certifying compilation
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Formalizing the Edmonds-Karp Algorithm
- A framework for the verification of certifying computations
- Trustworthy Graph Algorithms (Invited Talk)
- A learning-based fact selector for Isabelle/HOL
- Highly Automated Formal Proofs over Memory Usage of Assembly Code
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- Parameterized synthesis for fragments of first-order logic over data words
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
Uses Software
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)
