Formal verification for C program

MaRDI QIDQ5424313zbMATH OpenFDO

Authors Junyan Qian, Baowen Xu

Publication date 5 November 2007

zbMATH Keywords

model checkingprogram verificationpredicate abstraction

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1953015
• Efficient verification of sequential and concurrent C programs
• Model checking: from hardware to software.
• Predicate abstraction for program verification
• Formal Methods at the Crossroads. From Panacea to Foundational Support

Cited in

(9)

• Formal verification of C systems code. Structured types, separation logic and theorem proving
• String abstraction for model checking of C programs
• Extracting Zing Models from C Source Code
• Counter-example guided program verification
• Bounded model checking of C programs using event automaton specifications
• An Iterative Framework for Simulation Conformance
• Automated compositional abstraction refinement for concurrent C programs: a two-level approach
• Verifying numerical programs via iterative abstract testing
• Integrated and automated abstract interpretation, verification and testing of C/C++ modules

Describes a project that uses

Uses Software

• CIL
• Bandera
• Java PathFinder
• PVS

This page was built for publication: Formal verification for C program

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