Freek Verbeek

My name is Freek Verbeek and I am a PHD student, affiliated with the Radboud University (Nijmegen) and the Open University. My project concerns Networks-On-Chips (NoCs) and particularly the validation of deadlock-related theorems in this field. I work at the Model-Based System Development section (MBSD), which is a part of the Computing Science Department of the Radboud University. My promotors are Frits Vaandrager and Marko van Eekelen, my supervisor is Julien Schmaltz.

Research Interests

• Formal verification: currently I use the ACL2 theorem prover to validate theorems and algorithms. My main interest lies in Theorem Provers. I have some experience with other theorem provers like Coq, Mizar and HOL.
  
• 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.
  
• Typed λ-calculi: the subject of my master thesis was a comparison between λ-calculi isomorph to classical logical systems instead of intuitionistic ones.

Contact

Deadlock detection in networks

Publications

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