Publications

Here is a list of my publications in chronological order and organised under the categories: Journals, Edited proceedings Books and Book Chapters, Workshop and Conferences, Tutorials.

Journals

  1. Formal Specification of a Generic Separation Kernel. Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff, Julien Schmaltz. Archive of Formal Proofs 2014
  2. A decision procedure for deadlock-free routing in wormhole networks. F. Verbeek and J. Schmaltz. IEEE Transactions on Parallel and Distributed Systems 25(8):1935--1944, August 2014 IEEE
  3. Fully Reliable Dynamic Routing Logic for a Fault-Tolerant NoC Architecture A. Alhussein, F. Verbeek, B. van Gastel, N. Bagherzadeh, and J. Schmaltz. Journal of Integrated Circuits and Systems 8(1):43--53 2013
  4. Towards the formal verification of cache coherency at the architectural level. F. Verbeek and J. Schmaltz. ACM Transactions on Design Automation of Electronic Systems 17(3):1 2012 ACM
  5. Proof Pearl: A formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection network. F. Verbeek and J. Schmaltz. Journal of Automated Reasoning 48(4):419--439 2012 Springer
  6. Easy Formal Specification and Validation of Unbounded Networks-on-Chips Architectures. F. Verbeek and J. Schmaltz. ACM Transactions on Design Automation of Electronic Systems 17(1):1 2012 ACM
  7. Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks F. Heydarian, J. Schmaltz, and F. Vaandrager. Theoretical Computer Science 413(1):87--105 2012 Elsevier
  8. On necessary and sufficient conditions for deadlock-free routing in wormhole networks. F. Verbeek and J. Schmaltz. IEEE Transactions on Parallel and Distributed Systems 22(12):2022--2032, December 2011 IEEE
  9. A Comment on "A Necessary and Sufficient Condition for Deadlock-Free Adaptive Routing in Wormhole Networks". F. Verbeek and J. Schmaltz. IEEE Transactions on Parallel and Distributed Systems 22(10):1775--1776, October, 2011 IEEE
  10. The axiomatization of overriding and update. J. Berendsen, D. Jansen J. Schmaltz and F.W. Vaandrager. Journal of Applied Logic 8(1):141--150, March, 2010 Elsevier
  11. A formal approach to the verification of networks-on-chips D. Borrione, A. Helmy, L. Pierre, and J. Schmaltz. Journal on Embedded Systems (2009):548324 2009 Hindawi
  12. A Functional Formalization of On Chip Communications. J. Schmaltz and D. Borrione. Formal Aspects of Computing 20(3):241--258, May, 2008 Springer

Edited proceedings, Books, and Book Chapters

  1. Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2'14) F. Verbeek and J. Schmaltz. Vol 152 Electronic Proceedings in Theoretical Computer Science (EPTCS) 2014
  2. Proceedings of the 10th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2'11) D.S. Hardin and J. Schmaltz. Vol 70 Electronic Proceedings in Theoretical Computer Science (EPTCS) 2011
  3. Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP'11) M.J.C.D. van Eekelen, H. Geuvers, J. Schmaltz, and F. Wiedijk. LNCS 6898, Springer 2011
  4. Chapter 6: Formal verification of communications in networks-on-chips D. Borrione, A. Helmy, L. Pierre, and J. Schmaltz. Networks-on-Chip: Theory and Practice, F. Gebali and H. Elmigli (Eds.), Taylor & Francis Group LLC -- CRC Press 2009

Workshops and Conferences

  1. Modelling Information Routing with Noninterference. R. Koolean and J. Schmaltz. International Workshop on MILS: Architecture and Assurance for Secure Systems. Prague, Co-locatad with HiPEAC Conference, January 19, 2016 [web site]
  2. Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics. S. Wouda, S.J.C Joosten, J. Schmaltz. 13th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE'15) , Austin, USA, September , 2015 [web site]
  3. Formal API Specification of the PikeOS Separation Kernel F. Verbeek, J.Schmaltz, S. Tverdyshev, H. Blasum, O. Havle, B. Langenstein, W. Stephan, Y. Nemouchi, and B. Wolff. NASA Formal Methods Symposium, Pasadena, CA, USA 2015
  4. Automatic Extraction of Micro-Architectural Models of Communication Fabrics from Register Transfer Level Designs. S.J.C. Joosten and J. Schmaltz. Design and Test Europe (DATE'15), Grenoble, France, March 9--13, IEEE 2015 [web site]
  5. Formal Methods for MILS: Formalisations of the GWV Firewall R. Koolen and J. Schmaltz. International Workshop on MILS: Architecture and Assurance for Secure Systems. Amsterdam, Co-locatad with HiPEAC Conference, January 20, 2015 [web site]
  6. WickedXmas: Designing and Verifying on-chip Communication Fabrics. S.J.C. Joosten, F. Verbeek, and J. Schmaltz. International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS'14) Lausanne, Switzerland, October 20, 2014 (pdf link)
  7. Inference of channel types in micro-architectural models of on-chip communication networks. B. van Gastel, F. Verbeek, and J. Schmaltz. 22nd IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SOC'14), Playa del Carmen, Mexico, October 6-8, IEEE 2014
  8. On two models of noninterference: Rushby and Greve, Wilding, and Vanfleet. Adrian Garcia Ramirez, Julien Schmaltz, Freek Verbeek, Bruno Langenstein, and Holger Blasum. SAFECOMP 2014, LNCS 8666, Firenze, Italia, September 10-12 2014 [web site]
  9. Scalable liveness verification for communication fabrics. Sebastiaan J.C. Joosten. Design And Test Europe (DATE'14), Dresden, Germany IEEE 2014 [web site]
  10. Implicit Assumptions in a Model for Separation Kernels. F. Verbeek, J.Schmaltz, S. Tverdyshev, H. Blasum, and O. Havle. VERISURE Workshop, part of FLoC, July 23rd, Vienna, Austria 2014
  11. Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract). H. Blasum, O. Havle, B. Langenstein, Y. Nemouchi, J. Schmaltz, W. Stephan, S. Tverdyshev, F. Verbeek, and B. Wolff. Isabelle Workshop, part of FLoC, July 13, Vienna, Austria, 2014
  12. Generation of Inductive Invariants from Register Transfer Level Designs of Communication Fabrics. S.J.C. Joosten and J. Schmaltz. 11th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE'13) , Portland, USA, October 18-20, 2013
  13. A Formalisation of xMAS. B. van Gastel and J. Schmaltz. 11th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'13) , EPTCS Vol. 114, pp. 111--126, Laramie, WY, USA, May 30--31, 2013
  14. Verification of Building Blocks for Asynchronous Circuits. F. Verbeek and J. Schmaltz. 11th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'13) , EPTCS Vol. 114, pp. 70--84, Laramie, WY, USA, May 30--31, 2013
  15. A Macro for Reusing Abstract Functions and Theorems. S. J.C. Joosten, B. van Gastel and J. Schmaltz. 11th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'13), EPTCS Vol. 114, pp. 29--41, Laramie, WY, USA, May 30--31, 2013
  16. Formal Deadlock Verification for Click Circuits. F. Verbeek, S. Joosten and J. Schmaltz. 19th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'13), Santa Monica, CA, USA, May 19--22, IEEE 2013
  17. Automatic Generation of Deadlock Detection Algorithms for a Family of Microarchitecture Description Languages. Verbeek and Schmaltz (doi link) 17th IEEE International High Level Design Validation and Test Workshop (HLDVT'12) November IEEE 2012
  18. A formally verified deadlock-free routing function in a fault-tolerant NoC architecture. A. Alhussien, F. Verbeek, N. Bagherzadeh, J. Schmaltz and B. van Gastel. 25th Symposium on Integrated Circuits and System Design (SBCCI'12) Brasilia, Brazil, September IEEE/ACM 2012
  19. Formal verification of a deadlock detection algorithm. F. Verbeek and J. Schmaltz. 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'11) , pp. 103--112, EPTCS 70, Austin, Texas, USA, November 3--4 2011
  20. Hunting Deadlocks Efficiently in Micro-Architectural Models of Communication Fabrics. Verbeek and Schmaltz (pdf link) Formal Methods in Computer-Aided Design (FMCAD'11) pp. 223--231, Austin, TX, October 30 -- November 2, IEEE 2011
  21. Automatic verification for deadlock in adaptive routing wormhole networks. F. Verbeek and J. Schmaltz. International Symposium on Networks on Chip (NOCS'11) , pp. 25--32, Pittsburgh, PA, USA May 1-4 IEEE 2011
  22. An Experience Report on an Industrial Case-Study about Timed Model-Based Testing with UPPAAL-TRON. C. Ruetz and J. Schmaltz. 7th Workshop on Advances in Model Based Testing (A-MOST'11), March 21st, Berlin, IEEE 2011
  23. A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free. F. Verbeek and J. Schmaltz. Euromicro Conference on Pararell and Distributing Processing (PDP'11) pp. 3--10, Ayia Napa, Cyprus, February 9--11 IEEE 2011
  24. A conformance testing relation for symbolic timed automata. S. von Styp, H. Bohnenkamp, and J. Schmaltz. 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), pp. 673-686, Vienna, Austria, LNCS 6246, Springer 2010
  25. Inference and abstraction of the biometric passport. F. Aarts, J. Schmaltz, and F. Vaandrager. International Symposium on Leveraging Applications of Formal Methods (ISoLA'10), pp. 673-686, LNCS 6415, Springer 2010
  26. Proof Pearl: A formal proof a necessary and sufficient condition for deadlock-free adaptive networks. F. Verbeek and J. Schmaltz. 1st International Conference on Interactive Theorem Proving (ITP'10), pp. 67-82, LNCS 6172, part of FLoC'10, Edinburgh, Scotland, Springer 2010
  27. Formal specification of networks-on-chips: deadlock and evacuation. F. Verbeek and J. Schmaltz, Design Automation and Test in Europe (DATE'10) , pp. 1701--1706, Dresden, March 8--12, Germany, IEEE Computer Society 2010
  28. Formal Validation and Verification of Networks-on-Chips: Status and Perspective. J. Schmaltz, F. Verbeek, and T. van den Broek. Designing Correct Circuits (DCC'2010) , part of ETAPS 2010
  29. Towards a Fully Verified Network-on-Chip T. van den Broek and J. Schmaltz. Formal Methods in Computer-Aided Design (FMCAD'09), pp. 184--187, Austin, TX, October, IEEE Computer Society 2009
  30. Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks. F. Heydarian, J. Schmaltz, and F. Vaandrager. Formal Methods (FM'09) , pp. 516--531, LNCS 5850, Eindhoven, November 2--6, The Netherlands, Springer 2009
  31. Model-based testing of electronic passports. W. Mostowski, E. Poll, J. Schmaltz, J. Tretmans, and R. Wichers Schreur 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'09), pp. 207--209, LNCS 5825, November 2--3, Eindhoven, The Netherlands Springer 2009
  32. Formal validation of deadlock prevention in networks-on-chips. F. Verbeek and J. Schmaltz. 8th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'09), Boston, MA, May 11-12, USA, ACM 2009
  33. T. van den Broek and J. Schmaltz. A generic implementation model for the formal verification of networks-on-chips. 8th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'09) , Boston, MA, May 11-12, USA, ACM 2009
  34. On Conformance Testing for Timed Systems. J. Schmaltz and J. Tretmans. 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08) , pp. 249--263, St Malo, France, September 15--17, LNCS 5215, Springer 2008
  35. Executable Formal Specification and Validation of NoC Communication Infrastructures. D. Borrione, A. Helmy, L. Pierre and J. Schmaltz. 21st Symposium on Integrated Circuits and System Design (SBCCI'08) , pp. 176--181, Gramado, Brazil, September 1--4, ACM 2008
  36. Formal Specification and Validation of Minimal Routing Algorithms for the 2D Mesh. J. Schmaltz. 7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'07) , pp. 40--49, Austin, Texas, November 15-16, USA, ACM 2007
  37. A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware J. Schmaltz. Formal Methods in Computer-Aided Design (FMCAD'07) , pp. 223--230, Austin, TX, USA, 11-14 November, IEEE 2007
  38. A Generic Model for Formally Verifying NoC Communication Architectures: A Case Study D. Borrione, A. Helmy, L. Pierre and J. Schmaltz. 1st International Symposium on Networks on Chip (NoCs'07) , pp 127-137, Princeton, New Jersey, May 7-9, USA, IEEE 2007
  39. A Formal Model of Lower System Layer J. Schmaltz. Formal Methods in Computer-Aided Design (FMCAD'06), pp 191-192, San Jose, CA, USA, 12-16 November, IEEE 2006
  40. Towards a Formal Theory of Communication Architectures in the ACL2 Logic. J. Schmaltz and D. Borrione. 6th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'06) , FloC'06, pp 47-56, Seattle, WA, USA, August 15-16, ACM 2006
  41. Formalizing On Chip Communications in a Functional Style. J. Schmaltz and D. Borrione Workshop "Trustworthy Software" , May 18-19, Saarbruecken, Intl. Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2006
  42. A Generic Network on Chip Model. J. Schmaltz and D. Borrione. Theorem Proving in Higher Order Logics (TPHOLS'05) , LNCS 3603, pp 310-325, Oxford, UK, August 22-25, Springer 2005
  43. A Functional Specification and Validation Model for Networks on Chip in the ACL2 Logic J. Schmaltz and D. Borrione. 5th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'04), Austin, TX, USA November 18-19, 2004
  44. A Functional Approach to the Formal Specification of Networks on Chip. J. Schmaltz and D. Borrione. Formal Methods in Computer-Aided Design (FMCAD'04), LNCS 3312, pp 52-66, Austin, Texas, USA, November 14-17, Springer 2004
  45. Theosim: Combining Symbolic Simulation and Theorem Proving for Hardware Verification. G. Al Sammane, J. Schmaltz, D. Toma, P. Ostier and D. Borrione. 17th Symposium on Integrated Circuits and System Design (SBCCI'04), pp 60--65, Porto de Galinhas, Pernambuco, Brazil, September 7-11, ACM 2004
  46. Formal Verification of On-Chip Networking. G. Al Sammane, J. Schmaltz and D. Borrione. 1st International Conference on Information \& Communication Technologies : from Theory to Applications (ICTTA'04) , Damascus, Syria, April 19-23, 2004
  47. Constrained Symbolic Simulation with Mathematica and ACL2. G. Al Sammane, D. Toma, J. Schmaltz, P. Ostier and D. Borrione. 12th Advanced Research Conference on Correct Hardware Design and Verification Methods (CHARME'03), LNCS 2860, L'aquila, Italy, October 21-24, Springer 2003
  48. Validation of a Parameterized Bus Architecture. J. Schmaltz and D. Borrione. 4th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'03) , Boulder, Colorado, USA July 13-14, 2003
  49. Combining Mathematica for the Symbolic Simulation of Digital Systems. G. Al Sammane, D. Borrione, P. Ostier, J. Schmaltz and D. Toma. 4th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'03) , Boulder, Colorado, USA July 13-14, 2003
  50. Formalization and Verification of the AMBA AHB Communication Architecture Using the ACL2 Theorem Prover J. Schmaltz and D. Borrione. IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems (DDECS'03) , pp 93-100, Poznan, Poland, April 14-16, IEEE 2003

Tutorials

  1. Advanced Design, Analysis, and Verification of NoC Architectures. 23rd International Conference on Parallel Architectures and Compilation Techniques (PACT'14), August 24th, Edmonton, Canada 2014 [web site]
  2. Automatic Deadlock Verification in Wormhole Networks-on-Chips. International Symposium on Networks on Chip (NOCS'13), April 21, Tempe, Arizona, USA 2013