Freek Verbeek

Publication Activity (10 Years)

Years Active: 2010-2024
Publications (10 Years): 23

Top Topics

Formal Specification

Top Venues

Arch. Formal Proofs

IEEE Trans. Computers

Publications

João Pascoal Faria, Freek Verbeek, Anna Rita Fasolino
Report from the 14th International Workshop on Automating Test Case Design, Selection, and Evaluation (A-TEST 2023). ACM SIGSOFT Softw. Eng. Notes 49 (2) (2024)
Daniel Engel, Freek Verbeek, Binoy Ravindran
On the Decidability of Disassembling Binaries. TASE (2024)
Joshua A. Bockenek, Freek Verbeek, Binoy Ravindran
Exceptional Interprocedural Control Flow Graphs for x86-64 Binaries. DIMVA (2024)
Jaidev Shastri, Xiaoguang Wang, Basavesh Ammanaghatta Shivakumar, Freek Verbeek, Binoy Ravindran
HMTRace: Hardware-Assisted Memory-Tagging based Dynamic Data Race Detection. CoRR (2024)
Nico Naus, Freek Verbeek, Marc Schoolderman, Binoy Ravindran
Low-Level Reachability Analysis Based on Formal Logic. TAP (2023)
Daniel Engel, Freek Verbeek, Binoy Ravindran
BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of X86-64 Binaries. TAP (2023)
Xiaoxin An, Freek Verbeek, Binoy Ravindran
DSV: Disassembly Soundness Validation Without Assuming a Ground Truth. NFM (2022)
Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, Binoy Ravindran
Formally verified lifting of C-compiled x86-64 binaries. PLDI (2022)
Nico Naus, Freek Verbeek, Dale Walker, Binoy Ravindran
A Formal Semantics for P-Code. VSTTE (2022)
Nico Naus, Freek Verbeek, Marc Schoolderman, Binoy Ravindran
Reachability Logic for Low-Level Programs. CoRR (2022)
Freek Verbeek, Abhijith Bharadwaj, Joshua A. Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran
X86 instruction semantics and basic block symbolic execution. Arch. Formal Proofs 2021 (2021)
Jae-Won Jang, Freek Verbeek, Binoy Ravindran
Verification of Functional Correctness of Code Diversification Techniques. NFM (2021)
Freek Verbeek, Joshua A. Bockenek, Binoy Ravindran
Highly Automated Formal Proofs over Memory Usage of Assembly Code. TACAS (2) (2020)
Freek Verbeek, Pierre Olivier, Binoy Ravindran
Sound C Code Decompilation for a Subset of x86-64 Binaries. SEFM (2020)
Joshua A. Bockenek, Freek Verbeek, Peter Lammich, Binoy Ravindran
Formal Verification of Memory Preservation of x86-64 Binaries. SAFECOMP (2019)
Ian Roessle, Freek Verbeek, Binoy Ravindran
Formally verified big step semantics out of x86-64 binaries. CPP (2019)
Marko C. J. D. van Eekelen, Daniil Frumin, Herman Geuvers, Léon Gondelman, Robbert Krebbers, Marc Schoolderman, Sjaak Smetsers, Freek Verbeek, Benoît Viguier, Freek Wiedijk
A benchmark for C program verification. CoRR (2019)
Freek Verbeek, Joshua A. Bockenek, Abhijith Bharadwaj, Binoy Ravindran, Ian Roessle
Establishing a refinement relation between binaries and abstract code. MEMOCODE (2019)
Freek Verbeek, Pooria M. Yaghini, Ashkan Eghbal, Nader Bagherzadeh
A Compositional Approach for Verifying Protocols Running on On-Chip Networks. IEEE Trans. Computers 67 (7) (2018)
Freek Verbeek, Pooria M. Yaghini, Ashkan Eghbal, Nader Bagherzadeh
Deadlock Verification of Cache Coherence Protocols and Communication Fabrics. IEEE Trans. Computers 66 (2) (2017)
Freek Verbeek, Nike van Vugt
Estimating worst-case latency of on-chip interconnects with formal simulation. FMCAD (2017)
Freek Verbeek, Pooria M. Yaghini, Ashkan Eghbal, Nader Bagherzadeh
ADVOCAT: Automated deadlock verification for on-chip cache coherence and interconnects. DATE (2016)
Ronak Salamat, Masoumeh Ebrahimi, Nader Bagherzadeh, Freek Verbeek
CoBRA: Low cost compensation of TSV failures in 3D-NoC. DFT (2016)
Freek Verbeek, Oto Havle, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Bruno Langenstein, Werner Stephan, Burkhart Wolff, Yakoub Nemouchi
Formal API Specification of the PikeOS Separation Kernel. NFM (2015)
Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff, Julien Schmaltz
Formal Specification of a Generic Separation Kernel. Arch. Formal Proofs 2014 (2014)
Freek Verbeek, Julien Schmaltz
A Decision Procedure for Deadlock-Free Routing in Wormhole Networks. IEEE Trans. Parallel Distributed Syst. 25 (8) (2014)
Bernard van Gastel, Freek Verbeek, Julien Schmaltz
Inference of channel types in micro-architectural models of on-chip communication networks. VLSI-SoC (2014)
Adrian Garcia Ramirez, Julien Schmaltz, Freek Verbeek, Bruno Langenstein, Holger Blasum
On Two Models of Noninterference: Rushby and Greve, Wilding, and Vanfleet. SAFECOMP (2014)
Frits W. Vaandrager, Freek Verbeek
Recreational Formal Methods: Designing Vacuum Cleaning Trajectories. Bull. EATCS 113 (2014)
Freek Verbeek, Sebastiaan J. C. Joosten, Julien Schmaltz
Formal Deadlock Verification for Click Circuits. ASYNC (2013)
Freek Verbeek, Julien Schmaltz
Verification of Building Blocks for Asynchronous Circuits ACL2 (2013)
Freek Verbeek, Julien Schmaltz
Automatic generation of deadlock detection algorithms for a family of microarchitecture description languages of communication fabrics. HLDVT (2012)
Abdulaziz Alhussien, Nader Bagherzadeh, Freek Verbeek, Bernard van Gastel, Julien Schmaltz
A formally verified deadlock-free routing function in a fault-tolerant NoC architecture. SBCCI (2012)
Freek Verbeek, Julien Schmaltz
Easy Formal Specification and Validation of Unbounded Networks-on-Chips Architectures. ACM Trans. Design Autom. Electr. Syst. 17 (1) (2012)
Freek Verbeek, Julien Schmaltz
Towards the formal verification of cache coherency at the architectural level. ACM Trans. Design Autom. Electr. Syst. 17 (3) (2012)
Freek Verbeek, Julien Schmaltz
Proof Pearl: A Formal Proof of Dally and Seitz' Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks. J. Autom. Reason. 48 (4) (2012)
Freek Verbeek, Julien Schmaltz
Formal verification of a deadlock detection algorithm ACL2 (2011)
Freek Verbeek, Julien Schmaltz
A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free. PDP (2011)
Freek Verbeek, Julien Schmaltz
Hunting deadlocks efficiently in microarchitectural models of communication fabrics. FMCAD (2011)
Freek Verbeek, Julien Schmaltz
Automatic verification for deadlock in networks-on-chips with adaptive routing and wormhole switching. NOCS (2011)
Freek Verbeek, Julien Schmaltz
A Comment on "A Necessary and Sufficient Condition for Deadlock-Free Adaptive Routing in Wormhole Networks". IEEE Trans. Parallel Distributed Syst. 22 (10) (2011)
Freek Verbeek, Julien Schmaltz
On Necessary and Sufficient Conditions for Deadlock-Free Routing in Wormhole Networks. IEEE Trans. Parallel Distributed Syst. 22 (12) (2011)
Freek Verbeek, Julien Schmaltz
Formal specification of networks-on-chips: deadlock and evacuation. DATE (2010)
Freek Verbeek, Julien Schmaltz
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. ITP (2010)