Freek Verbeek

My name is Freek Verbeek and I am an assistant professor at VirginiaTech. I work at the Systems Software Research Group of prof. Binoy Ravindran (link). My interest is in formal verification, and especially the application of formal methods to realistic case-studies. I have finished my PhD which concerns Networks-On-Chips (NoCs) and particularly the validation of deadlock-related theorems in this field. Currently, I am working on bottom-up binary verification: is it possible to formally prove properties over binaries, without having source code?

We are hiring PhD students and postdocs!

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

Publications

• F. Verbeek et al. Sound C Code Decompilation for a Subset of x86-64 Binaries. SEFM 2020: 247-264. Best-paper award
• F. Verbeek et al. Highly Automated Formal Proofs over Memory Usage of Assembly Code.i TACAS (2) 2020: 98-117
• F. Verbeek et al. Establishing a refinement relation between binaries and abstract code. Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design. ACM, 2019.
• Joshua A. Bockenek et al. Formal Verification of Memory Preservation of x86-64 Binaries. International Conference on Computer Safety, Reliability, and Security (SAFECOMP'19). Springer, Cham, 2019.
• F.Verbeek et al. Symbolic Execution of x86 assembly in Isabelle/HOL. Workshop on Instruction Set Architecture Specification (SpISA'19)
• Ian Roessle, Freek Verbeek, and Binoy Ravindran. Formally verified big step semantics out of x86-64 binaries. Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, 2019.
• F. Verbeek and Nikè van Vugt. Estimating worst-case latency of on-chip interconnects with formal simulation. Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design. FMCAD Inc, 2017.
• F. Verbeek et al. A Compositional Approach for Verifying Protocols Running on On-Chip Networks. IEEE Transactions on Computers 67.7 (2017): 905-919.
• F. Verbeek et al. Deadlock verification of cache coherence protocols and communication fabrics. IEEE Transactions on Computers 66.2 (2016): 272-284.
• F. Verbeek et al. ADVOCAT: Automated deadlock verification for on-chip cache coherence and interconnects. Proceedings of the 2016 Conference on Design, Automation & Test in Europe (DATE'16). 2016
• Ramirez, Adrian Garcia, et al. On two models of noninterference: Rushby and Greve, Wilding, and Vanfleet. International Conference on Computer Safety, Reliability, and Security (SAFECOMP). Springer, Cham, 2014.
• F. Verbeek et al. Formal API specification of the PikeOS separation kernel. NASA Formal Methods Symposium. Springer, Cham, 2015. (see also archive of formal proofs)
• F. Verbeek et al. Implicit assumptions in a model for separation kernels. 2nd VeriSure Workshop (Vienna, Austria, July 23, 2014; part of FLoC). 2014.
• 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, Sebastiaan Joosten 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).