Low-level reachability analysis based on formal logic

DOI10.1007/978-3-031-38828-6_2MaRDI QIDQ6535328zbMATH OpenFDO

Authors Nico Naus, Freek Verbeek, Marc Schoolderman, Binoy Ravindran

Publication date 12 December 2023

zbMATH Keywords

formal methodsreachability analysisformal verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• A Reachability Predicate for Analyzing Low-Level Software
• Hoare-style logic for unstructured programs
• Proving reachability-logic formulas incrementally
• Adversarial reachability for program-level security analysis
• One-path reachability logic

Cites work

• scientific article; zbMATH DE number 1032009 (Why is no real title available?)
• An axiomatic basis for computer programming
• Backward symbolic execution with loop folding
• Computer Aided Verification
• Formal Methods for Components and Objects
• Local reasoning about the presence of bugs: incorrectness separation logic
• On algebra of program correctness and incorrectness
• One-path reachability logic
• Reverse Hoare logic
• Symbolic model checking: \(10^{20}\) states and beyond
• Theorie der einfachen Ungleichungen.
• Verifying branch-free assembly code in Why3

Cited in

(1)

• Adversarial reachability for program-level security analysis

This page was built for publication: Low-level reachability analysis based on formal logic

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