Low-Level Reachability Analysis Based on Formal Logic

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review


Reachability is an important problem in program analysis. Automatically being able to show that – and how – a certain state is reachable, can be used to detect bugs and vulnerabilities. Various research has focused on formalizing a program logic that connects preconditions to post-conditions in the context of reachability analysis, e.g., must+, Lisbon Triples, and Outcome Logic. Outcome Logic and its variants can be seen as an adaptation of Hoare Logic and Incorrectness Logic. In this paper, we aim to study 1.) how such a formal reachability logic can be used for automated precondition generation, and 2.) how it can be used to reason over low-level assembly code. Automated precondition generation for reachability logic enables us to find inputs that provably trigger an assertion (i.e., a post-condition). Motivation for focusing on low-level code is that low-level code accurately describes actual program behavior, can be targeted in cases where source code is unavailable, and allows reasoning over low-level properties like return pointer integrity. An implementation has been developed, and the entire system is proven to be sound and complete (the latter only in the absence of unresolved indirections) in the Isabelle/HOL theorem prover. Initial results are obtained on litmus tests and case studies. The results expose limitations: traversal may not terminate, and more scalability would require a compositional approach. However, the results show as well that precondition generation based on low-level reachability logic allows exposing bugs in low-level code.

Original languageEnglish
Title of host publicationTests and Proofs
Subtitle of host publication17th International Conference, TAP 2023, Leicester, UK, July 18–19, 2023, Proceedings
EditorsVirgile Prevosto, Cristina Seceleanu
PublisherSpringer, Cham
Number of pages19
ISBN (Electronic)9783031388286
ISBN (Print)9783031388279
Publication statusPublished - Jul 2023
Event17th International Conference, Tests and Proofs 2023 - Leicester, United Kingdom
Duration: 18 Jul 202319 Jul 2023

Publication series

SeriesLecture Notes in Computer Science


Conference17th International Conference, Tests and Proofs 2023
Abbreviated titleTAP 2023
Country/TerritoryUnited Kingdom
Internet address


  • Formal Methods
  • Formal verification
  • Reachability analysis


Dive into the research topics of 'Low-Level Reachability Analysis Based on Formal Logic'. Together they form a unique fingerprint.

Cite this