From the 1 of 4 linked papers with an AI index.
4 papers
Automated Template-free Synthesis of Instruction-Centric Leakage Contracts for Black-Box CPUs
Elvira Moreno, Tiziano Marinaro, Ryan Williams +4
The paper introduces malcos, a template‑free tool that automatically derives instruction‑centric leakage contracts for black‑box CPUs, enabling precise modeling of microarchitectur…
Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic
Hamed Nemati, Mads Dam
Shared-memory concurrency is notoriously difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments…
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Andreas Lindner, Karl Palmskog, Scott Constable +3
Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when…
Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA
Karl Palmskog, Andreas Lindner, Scott Constable +2
Many types of formal verification establish properties about abstract high-level program representations, leaving a large gap to programs at runtime. Although gaps can sometimes be…