Doomed program points

DOI10.1007/S10703-010-0102-0MaRDI QIDQ633286zbMATH OpenOpenAlexFDO

Authors Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies

Publication date 31 March 2011

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-010-0102-0

zbMATH Keywords

reliabilityprogram falsificationstatic checking

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Toward general diagnosis of static errors
• Static checker of semantic run-time errors
• scientific article; zbMATH DE number 1863891
• scientific article; zbMATH DE number 1670777
• Abstract Error Projection

Cites work

• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1982210 (Why is no real title available?)
• scientific article; zbMATH DE number 868107 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• A fast algorithm for finding dominators in a flowgraph
• Avoiding exponential explosion: generating compact verification conditions
• Compositional may-must program analysis: unleashing the power of alternation
• Computer Aided Verification
• Computer Science Logic
• Efficient weakest preconditions
• On the Notion of Vacuous Truth
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of Array, Record, and Pointer Operations in Pascal

Cited in

(1)

• Preemptive type checking

Describes a project that uses

Uses Software

• CBMC
• Boogie
• VCC
• ESC/Java
• Caduceus
• Spec#
• Why3
• KRAKATOA
• BLAST

This page was built for publication: Doomed program points

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