2009

Towards A Formally Verified Network-on-Chip. [More information and source code here] Tom van den Broek and Julien Schmaltz. 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD’09), pp.184-187, Austin, TX, USA, November 15-18, IEEE Society, 2009 ©IEEE Computer Society

Model-based testing of electronic passports. Wojciech Mostowski, Erik Poll, Julien Schmaltz, Jan Tretmans, and Ronny Wichers Schreur. 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS’09), pp. 207-209, LNCS 5825, Eindhoven, The Netherlands, November 2-3, 2009 © Springer

Analysis of a clock synchronization protocol for wireless sensor networks. [more] Faranak Heidarian, Julien Schmaltz and Frits Vaandrager. Second World Congress on Formal Methods (FM’09), pp. 516-531, LNCS 5850, Eindhoven, The Netherlands, November Formal Methods, LNCS, Eindhoven, The Netherlands, November 2-6, 2009 © Springer

A formal approach to the verification of networks-on-chips. [web] Dominique Borrione, Amr Helmy, Laurence Pierre, and Julien Schmaltz. EURASIP Journal on Embedded Systems, vol. 2009, Article ID 548324 2009 © Hindawi Publishing Corporation

Formal Validation of Deadlock Prevention in Networks-on-Chip. Freek Verbeek and Julien Schmaltz. 8th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'09), S. Ray and D. Russinoff (eds), pp. 135-145, Boston, MA, USA, May 11-12 2009 © ACM

A Generic Implementation Model for the Formal Verification of Networks-on-Chips. Tom van den Broek and Julien Schmaltz. 8th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'09), S. Ray and D. Russinoff (eds), pp. 130-134, Boston, MA, USA, May 11-12 2009 © ACM

Chapter 6: Formal verification of communications in networks-on-chips. Dominique Borrione, Amr Helmy, Laurence Pierre, Julien Schmaltz. Networks-on-Chips: Theory and Practice, Fayez Gebali  and Haytham Elmigli (eds.), March 2009 © Taylor & Francis Group LLC - CRC Press

2008

On Conformance Testing for Timed Systems. [more] Julien Schmaltz and Jan Tretmans. 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’08), F. Cassez and C. Jard (eds), pp. 249-263, St Malo, France, September 15-17, LNCS 5215, Springer, 2008 © Springer

Executable Formal Specification and Validation of NoCs Communication Infrastructures. Dominique Borrione, Amr Helmy, Laurence Pierre, Julien Schmaltz. 21st Symposium on Integrated Circuits and System Design (SBCCI'08), pp. 176-181, Granada, Brazil, September 4-7, ACM, 2008 © ACM [more]

A functional formalization of on-chip communications. [more] Julien Schmaltz and Dominique Borrione. Formal Aspects of Computing, 20(3):241-258, May 2008 © Springer 

2007

Formal Specification and Validation of Minimal Routing Algorithms for the 2D Mesh. Julien Schmaltz. 7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'07),  Austin, TX, USA, November 15-16, 2007

A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware. [more] Julien Schmaltz. 7th International Conference on Formal Methods in Computer-Aided Design (FMCAD’07), pp. 223-230, Austin, TX, USA, November 11-14, IEEE Society, 2007 ©IEEE

A Generic Model for Verifying NoC Communication Architectures: A Case Study. Dominique Borrione, Amr Helmy, Laurence Pierre, Julien Schmaltz. 1st International Symposium on Networks on Chips (NOCS’07), pp. 127-136, Princeton, NJ, USA, May 7-9, IEEE Press Society 2007 © IEEE [more]

2006

A Formal Model of Lower System Layers. Julien Schmaltz. 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD’06), pp. 191-192, San Jose, CA, USA, November 12-16, IEEE Press Society 2006 © IEEE [more]

Towards a Formal Theory of Communication Architecture in the ACL2 Logic. Julien Schmaltz and Dominique Borrione. 6th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'06), pp 47-60, Seattle, WA, USA, August 15-16, ACM 2006 © ACM [more]

Formalizing on-chip communications in a functional style. Julien Schmaltz and Dominique Borrione. Workshop «Trustworthy Software» 2006 [web link]

Une formalisation fonctionnelle  des communications sur la puce. Julien Schmaltz. PhD Thesis. Université Joseph Fourier, Grenoble, France [pdf] [slides]

2005

A Generic Network on Chip Model. Julien Schmaltz and Dominique Borrione. 18th International Conference on Theorem Proving in Higher-Order Logics (TPHOLS’05), pp 310-325, Oxford, UK, August 22-25, LNCS 3603, Springer, 2005 © Springer [more]

2004

A Functional Approach to the Formal Specification of  Networks on Chip. Julien Schmaltz and Dominique Borrione. 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD’04), pp.52-66, Austin, TX, USA, November 15-17, LNCS 3312, Springer 2004 © Springer [more]

Theosim: Combining Symbolic Simulation and Theorem Proving for Hardware Verification. Ghiath Al Sammane, Julien Schmaltz, Diana Toma, Pierre Ostier, Dominique Borrione. 17 Symposium on Integrated Circuits and System Design (SBCCI'04), pp. 60-65, Porto de Galinhas, Pernambuco, Brazil, September 7-11 ACM 2004 © ACM [more]

Formal verification of on-chip networking. Ghiath Al Sammane, Julien Schmaltz, and Dominique Borrione. 1st International Conference on Information and Communication Technologies: from Theory to Practice (ICTTA’04), Damascus Syria, April 19-23, 2004

2003

Constrained Symbolic Simulation with Mathematica and ACL2. Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier, Dominique Borrione. 12th Advanced Research Conference on Correctn Hardware Design and Verification Methods (CHARME’03), pp. 150-157, L’Aquila, Italy, October 21-24, LNCS 2860, Springer, 2003 © Springer [more]

Combining mathematica and ACL2 for the symbolic execution of digital systems. Ghiath Al Sammane, Dominique Borrione, Pierre Ostier, Julien Schmaltz and Diana Toma. 4th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'03), Boulder, CA, USA, July 13-14, 2003

Validation of a parameterized bus architecture. Julien Schmaltz and Dominique Borrione, 4th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'03), Boulder, CA, USA, July 13-14, 2003

Formalization and Verification of the AMBA AHB Communication Architecture Using the ACL2 Theorem Prover. Julien Schmaltz and Dominique Borrione. 6th IEEE Workshop on Design and Diagnostics of Electronic Circtuits and Systems (DDECS'03), pp 93-100, Poznan, Poland, April 14-16, IEEE Computer Society 2003 © IEEE

2010

Inference and abstraction of the biometric passport. Fides Aarts, Julien Schmaltz, and Frits Vaandrager. Proceedings 4th International Symposium on Leveraging Applications of Formal Methods (ISoLA'10), pp. 673-686. LNCS 6415. Springer 2010.

A conformance testing relation for symbolic timed automata. Sabrina von Styp, Henrik Bohnenkamp, and Julien Schmaltz. 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), pp. 243-255,Vienna, Austria, LNCS 6246. Springer 2010

Proof Pearl: A formal proof of Duato’s condition for deadlock-free adaptive networks. [More information and source code available here] Freek Verbeek and Julien Schmaltz. 1st International Conference on Interactive Theorem Proving (ITP’10), pp. 67-82, part of FLoC’10, LNCS 6172, Kaufman and Paulson (Eds), July 11-14, Edinburgh, Scotland © Springer 2010

Formal Validation and Verification of Networks-Chips: Status and Perspective (Draft Paper). Julien Schmaltz, Freek Verbeek, and Tom van den Broek. Designing Correct Circuit (DCC’10), ETAPS 2010

Formal Specification of Networks-on-Chips: Deadlock and Evacuation. [more] Freek Verbeek and Julien Schmaltz. International Conference on Design Automation and Test Europe (DATE’10), Dresden, Germany © IEEE/ACM 2010

The axiomatization of overriding and update. [more] Jasper Berendsen, David Jansen, Julien Schmaltz and Frits Vaandrager. Journal of Applied Logic. Elsevier 2010

2011

Hunting deadlocks efficiently in microarchitectural models of communication fabrics. Freek Verbeek and Julien Schmaltz. Formal Methods in Computer-Aided Design (FMCAD'11). To Appear. © IEEE 2011

Easy formal specification and validation of unbounded networks-on-chips architectures. Freek Verbeek and Julien Schmaltz. ACM Transactions on Design Automation of Electronic Systems. To Appear. © ACM 2011

Analysis of a clock synchronization protocol for wireless sensor networks. Faranak Heydarian, Julien Schmaltz, and Frits Vaandrager. Theoretical Computer Science. To Appear © Elsevier 2011

On necessary and sufficient conditions for deadlock-free routing in wormhole networks. [more] Freek Verbeek and Julien Schmaltz. IEEE Transactions on Parallel and Distributed Systems. On-line (PrePrints)© IEEE 2011

Proof Pearl: A formal proof of Dally&Seitz necessary and sufficient condition for deadlock-free routing in interconnection networks. [More information and source code here.] Freek Verbeek and Julien Schmaltz. Journal of Automated Reasoning. On-line Springer 2011

A comment on "A necessary and sufficient condition for deadlock-free adaptive routing in wormhole networks".Freek Verbeek and Julien Schmaltz. IEEE Transactions on Parallel and Distributed Systems. On-line 22(10):1775--1776 © IEEE 2011

Automatic verification for deadlock in adaptive routing wormhole networks. Freek Verbeek and Julien Schmaltz. IEEE Symposium on Networks-on-Chips (NOCS'11). Pittsburgh, PA, USA, May 1-4 © IEEE 2011

Formal verification of a time-Triggered hardware interface. Source code here. Julien Schmaltz. CoRR Report ArXiv:1103.2246 on-line March 2011

An experience report on an industrial case-study about timed model-based testing with UPPAAL-TRON. [more] Carsten Rütz and Julien Schmaltz. 7th Workshop on Advances in Model Based Testing (A-MOST'11), Berlin, March 21st.  © IEEE 2011

A fast and verified algorithm for proving store-and-forward networks deadlock-free. [more] Freek Verbeek and Julien Schmaltz. Proc. 19th International Conference on Parallel, Distributed and Networked-Based Computing (PDP'11). February 9-11, Aya Napa, Cyprus © IEEE 2011