Formal specification of networks-on-chips: deadlock and evacuation. - Freek Verbeek; Julien Schmaltz (DATE, 2010)

A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. - Freek Verbeek; Julien Schmaltz (ITP, 2010)

Hunting deadlocks efficiently in microarchitectural models of communication fabrics. - Freek Verbeek; Julien Schmaltz (FMCAD, 2011)

Automatic verification for deadlock in networks-on-chips with adaptive routing and wormhole switching. - Freek Verbeek; Julien Schmaltz (NOCS, 2011)

A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free. - Freek Verbeek; Julien Schmaltz (PDP, 2011)

Formal verification of a deadlock detection algorithm - Freek Verbeek; Julien Schmaltz (ACL2, 2011)

A Comment on "A Necessary and Sufficient Condition for Deadlock-Free Adaptive Routing in Wormhole Networks". - Freek Verbeek; Julien Schmaltz (IEEE Trans. Parallel Distributed Syst., 2011)

On Necessary and Sufficient Conditions for Deadlock-Free Routing in Wormhole Networks. - Freek Verbeek; Julien Schmaltz (IEEE Trans. Parallel Distributed Syst., 2011)

Automatic generation of deadlock detection algorithms for a family of microarchitecture description languages of communication fabrics. - Freek Verbeek; Julien Schmaltz (HLDVT, 2012)

A formally verified deadlock-free routing function in a fault-tolerant NoC architecture. - Abdulaziz Alhussien; Nader Bagherzadeh; Freek Verbeek; Bernard van Gastel; Julien Schmaltz (SBCCI, 2012)

Proof Pearl: A Formal Proof of Dally and Seitz' Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks. - Freek Verbeek; Julien Schmaltz (J. Autom. Reason., 2012)

Easy Formal Specification and Validation of Unbounded Networks-on-Chips Architectures. - Freek Verbeek; Julien Schmaltz (ACM Trans. Design Autom. Electr. Syst., 2012)

Towards the formal verification of cache coherency at the architectural level. - Freek Verbeek; Julien Schmaltz (ACM Trans. Design Autom. Electr. Syst., 2012)

Formal Deadlock Verification for Click Circuits. - Freek Verbeek; Sebastiaan J. C. Joosten; Julien Schmaltz (ASYNC, 2013)

Verification of Building Blocks for Asynchronous Circuits - Freek Verbeek; Julien Schmaltz (ACL2, 2013)

On Two Models of Noninterference: Rushby and Greve, Wilding, and Vanfleet. - Adrian Garcia Ramirez; Julien Schmaltz; Freek Verbeek; Bruno Langenstein; Holger Blasum (SAFECOMP, 2014)

Inference of channel types in micro-architectural models of on-chip communication networks. - Bernard van Gastel; Freek Verbeek; Julien Schmaltz (VLSI-SoC, 2014)

Formal Specification of a Generic Separation Kernel. - Freek Verbeek; Sergey Tverdyshev; Oto Havle; Holger Blasum; Bruno Langenstein; Werner Stephan 001; Yakoub Nemouchi; Abderrahmane Feliachi; Burkhart Wolff; Julien Schmaltz (Arch. Formal Proofs, 2014)

Recreational Formal Methods: Designing Vacuum Cleaning Trajectories. - Frits W. Vaandrager; Freek Verbeek (Bull. EATCS, 2014)

A Decision Procedure for Deadlock-Free Routing in Wormhole Networks. - Freek Verbeek; Julien Schmaltz (IEEE Trans. Parallel Distributed Syst., 2014)

Formal API Specification of the PikeOS Separation Kernel. - Freek Verbeek; Oto Havle; Julien Schmaltz; Sergey Tverdyshev; Holger Blasum; Bruno Langenstein; Werner Stephan 001; Burkhart Wolff; Yakoub Nemouchi (NFM, 2015)

ADVOCAT: Automated deadlock verification for on-chip cache coherence and interconnects. - Freek Verbeek; Pooria M. Yaghini; Ashkan Eghbal; Nader Bagherzadeh (DATE, 2016)

CoBRA: Low cost compensation of TSV failures in 3D-NoC. - Ronak Salamat; Masoumeh Ebrahimi; Nader Bagherzadeh; Freek Verbeek (DFT, 2016)

Estimating worst-case latency of on-chip interconnects with formal simulation. - Freek Verbeek; Nike van Vugt (FMCAD, 2017)

Deadlock Verification of Cache Coherence Protocols and Communication Fabrics. - Freek Verbeek; Pooria M. Yaghini; Ashkan Eghbal; Nader Bagherzadeh (IEEE Trans. Computers, 2017)

A Compositional Approach for Verifying Protocols Running on On-Chip Networks. - Freek Verbeek; Pooria M. Yaghini; Ashkan Eghbal; Nader Bagherzadeh (IEEE Trans. Computers, 2018)

Formally verified big step semantics out of x86-64 binaries. - Ian Roessle; Freek Verbeek; Binoy Ravindran (CPP, 2019)

Establishing a refinement relation between binaries and abstract code. - Freek Verbeek; Joshua A. Bockenek; Abhijith Bharadwaj; Binoy Ravindran; Ian Roessle (MEMOCODE, 2019)

Formal Verification of Memory Preservation of x86-64 Binaries. - Joshua A. Bockenek; Freek Verbeek; Peter Lammich; Binoy Ravindran (SAFECOMP, 2019)

A benchmark for C program verification. - 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 (CoRR, 2019)

Sound C Code Decompilation for a Subset of x86-64 Binaries. - Freek Verbeek; Pierre Olivier; Binoy Ravindran (SEFM, 2020)

Highly Automated Formal Proofs over Memory Usage of Assembly Code. - Freek Verbeek; Joshua A. Bockenek; Binoy Ravindran (TACAS (2), 2020)

Verification of Functional Correctness of Code Diversification Techniques. - Jae-Won Jang; Freek Verbeek; Binoy Ravindran (NFM, 2021)

X86 instruction semantics and basic block symbolic execution. - Freek Verbeek; Abhijith Bharadwaj; Joshua A. Bockenek; Ian Roessle; Timmy Weerwag; Binoy Ravindran (Arch. Formal Proofs, 2021)

DSV: Disassembly Soundness Validation Without Assuming a Ground Truth. - Xiaoxin An; Freek Verbeek; Binoy Ravindran (NFM, 2022)

Formally verified lifting of C-compiled x86-64 binaries. - Freek Verbeek; Joshua A. Bockenek; Zhoulai Fu; Binoy Ravindran (PLDI, 2022)

A Formal Semantics for P-Code. - Nico Naus; Freek Verbeek; Dale Walker; Binoy Ravindran (VSTTE, 2022)

Reachability Logic for Low-Level Programs. - Nico Naus; Freek Verbeek; Marc Schoolderman; Binoy Ravindran (CoRR, 2022)

BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of X86-64 Binaries. - Daniel Engel; Freek Verbeek; Binoy Ravindran (TAP, 2023)

Low-Level Reachability Analysis Based on Formal Logic. - Nico Naus; Freek Verbeek; Marc Schoolderman; Binoy Ravindran (TAP, 2023)

BIRD: A Binary Intermediate Representation for formally verified Decompilation of x86-64 binaries. - Daniel Engel; Freek Verbeek; Binoy Ravindran (Zenodo, 2023)

Poster: Formally Verified Binary Lifting to P-Code. - Nico Naus; Freek Verbeek; Sagar Atla; Binoy Ravindran (CCS, 2024)

Verifiably Correct Lifting of Position-Independent x86-64 Binaries to Symbolized Assembly. - Freek Verbeek; Nico Naus; Binoy Ravindran (CCS, 2024)

Exceptional Interprocedural Control Flow Graphs for x86-64 Binaries. - Joshua A. Bockenek; Freek Verbeek; Binoy Ravindran (DIMVA, 2024)

On the Decidability of Disassembling Binaries. - Daniel Engel; Freek Verbeek; Binoy Ravindran (TASE, 2024)

HMTRace: Hardware-Assisted Memory-Tagging based Dynamic Data Race Detection. - Jaidev Shastri; Xiaoguang Wang 003; Basavesh Ammanaghatta Shivakumar; Freek Verbeek; Binoy Ravindran (CoRR, 2024)

libLISA: Instruction Discovery and Analysis on x86-64. - Jos Craaijo; Freek Verbeek; Binoy Ravindran (Proc. ACM Program. Lang., 2024)

Artifact for the DIMVA 2024 paper "Exceptional Interprocedural Control Flow Graphs for x86-64 Binaries". - Joshua A. Bockenek; Freek Verbeek; Binoy Ravindran (Zenodo, 2024)

Report from the 14th International Workshop on Automating Test Case Design, Selection, and Evaluation (A-TEST 2023). - João Pascoal Faria; Freek Verbeek; Anna Rita Fasolino (ACM SIGSOFT Softw. Eng. Notes, 2024)

Reproduction package (Docker container) for the OOPSLA 2024 article "libLISA: Instruction Discovery and Analysis on x86-64". - Jos Craaijo; Freek Verbeek; Binoy Ravindran (Zenodo, 2024)

Formally Verified Binary-Level Pointer Analysis. - Freek Verbeek; Ali Shokri 003; Daniel Engel; Binoy Ravindran (ICSE, 2025)

On Extending Incorrectness Logic with Backwards Reasoning. - Freek Verbeek; Md Syadus Sefat; Zhoulai Fu; Binoy Ravindran (Proc. ACM Program. Lang., 2025)

Augmented Weak Distance for Fast and Accurate Bounds Checking. - Zhoulai Fu; Freek Verbeek; Binoy Ravindran (CoRR, 2025)

BeePL: Correct-by-compilation kernel extensions. - Swarn Priya; Frédéric Besson; Connor Sughrue; Tim Steenvoorden; Jamie Fulford; Freek Verbeek; Binoy Ravindran (CoRR, 2025)