My name is Freek Verbeek and I am an assistent professor, affiliated
Open University of The Netherlands, working at the Radboud University in Nijmegen. I work at the Digital
Security section (DS),
which is a part of the Computing Science Department of the Radboud
University. My promotors were Frits
Vaandrager and Marko van
supervisor was Julien
Schmaltz. I have finished my PhD
which concerns Networks-On-Chips (NoCs) and particularly the validation of
deadlock-related theorems in this field.
- Formal verification: in the EUROMILS project I have used Isabelle/HOL to prove security properties such as noninterference over PikeOS,
an industrial separation kernel. I have used the ACL2 theorem
prover to validate theorems and algorithms in hardware design, most
notably on NoCs. I also teach a course on model-checking and
Networks: in particular I am interested in deadlock prevention in
networks. Also, I have studied livelock and starvation prevention
mechanisms. Other related research interests are dynamic networks and
message dependent routing functions.
- Cache Coherent Architectures: recently, I have become
interested in cross-layer verification. Modelling both a cache
coherence protocol and the undelrying communication fabric, to perform
monolithic analysis. This enables me to find exotic and unexpected
deadlocks that emerge even when the communication fabric and the
protocol are deadlock-free when considered in isolation.
λ-calculi: the subject of my master thesis was a comparison between
λ-calculi isomorph to classical logical systems instead of
You can reach me by e-mail: fvb `at' ou.nl or visit me at the Radboud Universiteit:
Deadlock detection in communication networks
DCI2 is a tool for finding deadlocks in communication networks. See here
for downloads and tutorials.
As for the cross-layer
verification tool ADVOCAT
, please see here
for more information.
We are also developing graphical deadlock detection tools for xMAS. See here here
for screen shots and downloads. Please note that this very much under
development, and documentation is still very sparse. Information on the
examples that are proven deadlock-free can be found in my thesis
and are available on request.
- Alhussien, Abdulaziz, et al. Fully Reliable Dynamic Routing Logic for a Fault-Tolerant NoC Architecture. Journal of Integrated Circuits and Systems 8.1 (2013): 43-53 (link).
- F. Verbeek and J. Schmaltz. A Decision Procedure for Deadlock-Free Routing in Wormhole Networks. IEEE Transactions on
Parallel and Distributed Systems (TPDS), july 2013 (link).
- F. Verbeek and J. Schmaltz. Verification of Building Blocks for Asynchronous Circuits. Proceedings of the ACL2 Workshop, may 2013 (link).
- F. Verbeek and J. Schmaltz. Formal Deadlock Verification for Click Circuits. IEEE 19th International Symposium on Asynchronous Circuits and Systems (ASYNC), may 2013 (link).
- F. Verbeek. Formal Verification of On-Chip Communication Fabrics. PhD thesis, march 2013 (link)
- A. Alhussien and N. Bagherzadeh and F. Verbeek, F. and B.
van Gastel, B. and J. Schmaltz. A
formally verified deadlock-free routing function in a fault-tolerant
NoC architecture. Proceedings of the 25th Symposium on
Integrated Circuits and Systems Design (SBCCI'12), august 2012 (link).
- F. Verbeek and J. Schmaltz. Towards the Formal Verification of Cache
Coherency at the Architectural Level. ACM Transactions on
Design Automation of Electronic Systems (TODAES). Accepted for
- F. Verbeek and J. Schmaltz. Formal
veriﬁcation of a deadlock detection algorithm. Proceedings
of the Workshop on the ACL2 Theorem Prover and its Applications
(ACL2'11), november 2011 (link).
- F. Verbeek and J. Schmaltz. Hunting deadlocks efficiently in
microarchitectural models of communication fabrics. Proceedings
of Formal Methods in Computer Aided Design (FMCAD'11), november 2011 (link).
- F. Verbeek and J. Schmaltz. Easy Formal Speciﬁcation and Validation of
Unbounded Networks-on-Chips Architectures. ACM Transactions on
Design Automation of Electronic Systems (TODAES), january 2012 (link).
- F. Verbeek and J. Schmaltz. Automatic veriﬁcation for deadlock in
networks-on-chips with adaptive routing and wormhole switching. Proceedings
of Networks-on-Chips Symposium (NOCS'11), may 2011 (link).
- F. Verbeek and J. Schmaltz. A Fast and Veriﬁed Algorithm for Proving
Store-and-Forward Networks Deadlock-Free.
Proceedings of The 19th Euromicro International Conference
on Parallel, Distributed and Network-Based Computing (PDP'11), february
- F. Verbeek and J. Schmaltz. On Necessary and Sufficient Conditions for
Deadlock-Free Routing in Wormhole Networks. IEEE Transactions on
Parallel and Distributed Systems (TPDS), february 2011 (link).
- F. Verbeek and J. Schmaltz. A Comment on “A Necessary and Sufficient
Condition for Deadlock-Free Adaptive Routing in Wormhole Networks”.
IEEE Transactions on Parallel and Distributed Systems (TPDS), january
- F. Verbeek and J. Schmaltz. Proof Pearl: A formal proof of Duato's
condition for deadlock-free adaptive networks. Proceedings of
Interactive Theorem Proving (ITP), july 2010 (link).
- J. Schmaltz, F. Verbeek and T. van der Broek. Formal Validation and Verification of
Networks-Chips: Status and Perspective (Draft Paper).
Proceedings of Designing Correct Circuits (DCC), march 2010 (link).
- F. Verbeek and J. Schmaltz. Proof
Pearl: A formal proof of Dally&Seitz necessary and sufficient
condition for deadlock-free routing in interconnection networks.
Journal of Automated Reasoning (JAR) (link).
- F. Verbeek and J. Schmaltz. Formal Specification of Networks-on-Chips:
Deadlock and Evacuation. Proceedings of DATE, march
- F. Verbeek and J. Schmaltz. Formal Validation of Deadlock Prevention
in Networks-On-Chips. Proceedings of the Eight International
Workshop on the ACL2 Theorem Prover and its Applications, may 2009 (link).
- ICT.OPEN 2012. A poster on cross-layer deadlock detection in communication fabrics.
- NOCS 2010. A poster on the
deadlock detection algorithms for packet- and wormhole networks.
- SIREN 2009.
A poster on the GeNoC Verification method and the theorems which can be
proven with it.