9 citations · 11 across the 10 of their papers we have counts for
10 papers
Adding Compilation Metadata To Binaries To Make Disassembly Decidable
Daniel Engel, Freek Verbeek, Pranav Kumar +1
The binary executable format is the standard method for distributing and executing software. Yet, it is also as opaque a representation of software as can be. If the binary format…
BeePL: Correct-by-compilation kernel extensions
Swarn Priya, Frédéric Besson, Connor Sughrue +4
eBPF is a technology that allows developers to safely extend kernel functionality without modifying kernel source code or developing loadable kernel modules. Since the kernel gover…
Augmented Weak Distance for Fast and Accurate Bounds Checking
Zhoulai Fu, Freek Verbeek, Binoy Ravindran
This work advances floating-point program verification by introducing Augmented Weak-Distance (AWD), a principled extension of the Weak-Distance (WD) framework. WD is a recent appr…
Formally Verified Binary-level Pointer Analysis
Freek Verbeek, Ali Shokri, Daniel Engel +1
Binary-level pointer analysis can be of use in symbolic execution, testing, verification, and decompilation of software binaries. In various such contexts, it is crucial that the r…
HMTRace: Hardware-Assisted Memory-Tagging based Dynamic Data Race Detection
Jaidev Shastri, Xiaoguang Wang, Basavesh Ammanaghatta Shivakumar +2
Data race, a category of insidious software concurrency bugs, is often challenging and resource-intensive to detect and debug. Existing dynamic race detection tools incur significa…
Reachability Logic for Low-Level Programs
Nico Naus, Freek Verbeek, Marc Schoolderman +1
Automatic exploit generation is a relatively new area of research. Work in this area aims to automate the manual and labor intensive task of finding exploits in software. In this p…
A benchmark for C program verification
Marko van Eekelen, Daniil Frumin, Herman Geuvers +7
We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verificati…
Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications
Freek Verbeek, Julien Schmaltz
This volume contains the proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2'14, a two-day workshop held in Vienna, Austria, on…
Verification of Building Blocks for Asynchronous Circuits
Freek Verbeek, Julien Schmaltz
Scalable formal verification constitutes an important challenge for the design of asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an…
Formal verification of a deadlock detection algorithm
Freek Verbeek, Julien Schmaltz
Deadlock detection is a challenging issue in the analysis and design of on-chip networks. We have designed an algorithm to detect deadlocks automatically in on-chip networks with w…