Low-level reachability analysis based on formal logic

DOI10.1007/978-3-031-38828-6_2zbMATH Open1541.6811MaRDI QIDQ6535328FDOQ6535328

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

Publication date: 12 December 2023

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

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)

Cites Work

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

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)