Freek Verbeek

My name is Freek Verbeek and I am an assistent professor, affiliated with the 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 Eekelen, my 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.

Research Interests

  • 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 model-based testing.
  • NoCs/Interconnection 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.
  • Typed λ-calculi: the subject of my master thesis was a comparison between λ-calculi isomorph to classical logical systems instead of intuitionistic ones.

Contact

You can reach me by e-mail: fvb `at' ou.nl or visit me at the Radboud Universiteit:
Mercator I
Room 3.07

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.

Publications

  • 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 publication.
  • F. Verbeek and J. Schmaltz. Formal verification 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 Specification 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 verification 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 Verified 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 2011 (link).
  • 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 2011 (link).
  • 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 2010 (link).
  • 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).

Posters

  • 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.