David Nowak

ダヴィッド ノヴァック

CRIStAL, CNRS & University of Lille

Publications

(BibTeX file)

Peer-reviewed Journals

[1] David Nowak and Yu Zhang. Formal security proofs with minimal fuss: Implicit computational complexity at work. Information and Computation, 241:96--113, April 2015. [ http ]
[2] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal security proofs: the case of BBS. Science of Computer Programming, 77(10-11):1058--1074, September 2012. [ http ]
[3] Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. Mathematical Structures in Computer Science, 18(6):1169--1217, December 2008. [ http ]
[4] Stéphane Demri and David Nowak. Reasoning about transfinite sequences. International Journal of Foundations of Computer Science, 18(1):87--112, February 2007. [ http ]
[5] Stéphane Demri, Ranko Lazić, and David Nowak. On the freeze quantifier in Constraint LTL: decidability and complexity. Information and Computation, 205(1):2--24, January 2007. [ http ]
[6] David Nowak. Synchronous structures. Information and Computation, 204(8):1295--1324, August 2006. [ http ]

Peer-reviewed Conferences

[1] Narjes Jomaa, David Nowak, Gilles Grimaud, and Samuel Hym. Formal proof of dynamic memory isolation based on MMU. In Marcello Bonsangue and Yuxin Deng, editors, 10th International Symposium on Theoretical Aspects of Software Engineering (TASE 2016), July 17-19, 2016, Shanghai, China, pages 73--80, Shanghai, China, July 2016. IEEE Computer Society. [ http ]
[2] Dorel Lucanu, Vlad Rusu, Andrei Arusoaie, and David Nowak. Verifying reachability-logic properties on rewriting-logic specifications. In Narciso Martí-Oliet, Peter Csaba Ölveczky, and Carolyn Talcott, editors, Logic, Rewriting, and Concurrency: Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday, LRC 2015, Urbana, Illinois, USA, September 23-25, 2015, volume 9200 of Lecture Notes in Computer Science, pages 451--474, Urbana, Illinois, USA, September 2015. Springer. [ http ]
[3] Narjes Jomaa, David Nowak, Gilles Grimaud, and Julien Iguchi-Cartigny. Preuve formelle d'isolation mémoire dynamique à base de MMU. In Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), pages 297--300, Le Val d'Ajol, France, January 2015.
[4] Reynald Affeldt, David Nowak, and Yutaka Oiwa. Formal network packet processing with minimal fuss: Invertible syntax descriptions at work. In Koen Claessen and Nikhil Swamy, editors, Proceedings of the 6th ACM Workshop Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012, pages 27--36, Philadelphia, PA, USA, January 2012. ACM. [ http ]
[5] Sylvain Heraud and David Nowak. A formalization of polytime functions. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, volume 6898 of Lecture Notes in Computer Science, pages 119--134, Nijmegen, The Netherlands, August 2011. Springer. [ http ]
[6] David Nowak and Yu Zhang. A calculus for game-based security proofs. In Swee-Huay Heng and Kaoru Kurosawa, editors, Provable Security - 4th International Conference, ProvSec 2010, Malacca, Malaysia, October 13-15, 2010. Proceedings, volume 6402 of Lecture Notes in Computer Science, pages 35--52, Malacca, Malaysia, October 2010. Springer. [ http ]
[7] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. In Markus Roggenbach, editor, Automated Verification of Critical Systems 2009, volume 23 of Electronic Communications of the EASST, Swansea, UK, September 2009. EASST. [ http ]
[8] David Nowak and Kiyoshi Yamada. Towards a certified implementation of a cryptographically secure pseudorandom bit generator. In The 11th JSSST Workshop on Programming and Programming Languages (PPL 2009), pages 16--20, Takayama, Japan, March 2009. [ http ]
[9] David Nowak. On formal verification of arithmetic-based cryptographic primitives. In Pil Joong Lee and Jung Hee Cheon, editors, Information Security and Cryptology - ICISC 2008, 11th International Conference, Seoul, Korea, December 3-5, 2008, Proceedings, volume 5461 of Lecture Notes in Computer Science, pages 368--382, Seoul, Korea, December 2008. Springer. [ http ]
[10] David Nowak. A framework for game-based security proofs. In Sihan Qing, Hideki Imai, and Guilin Wang, editors, Information and Communications Security, 9th International Conference, ICICS 2007, Zhengzhou, China, December 12-15, 2007, Proceedings, volume 4861 of Lecture Notes in Computer Science, pages 319--333, Zhengzhou, China, December 2008. Springer. [ http ]
[11] Slawomir Lasota, David Nowak, and Yu Zhang. On completeness of logical relations for monadic types. In Mitsu Okada and Ichiro Satoh, editors, Advances in Computer Science - ASIAN 2006, Secure Software, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Proceedings, volume 4435 of Lecture Notes in Computer Science, pages 223--230, Tokyo, Japan, January 2008. Springer. [ http ]
[12] Stéphane Demri and David Nowak. Reasoning about transfinite sequences (extended abstract). In Doron A. Peled and Yih-Kuen Tsay, editors, Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005. Proceedings, volume 3707 of Lecture Notes in Computer Science, pages 248--262, Taipei, Taiwan, October 2005. Springer. [ http ]
[13] Stéphane Demri, Ranko Lazić, and David Nowak. On the freeze quantifier in Constraint LTL: decidability and complexity. In 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA, pages 113--121, Burlington, Vermont, USA, June 2005. IEEE Computer Society. [ http ]
[14] Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, and Yu Zhang. Complete lax logical relations for cryptographic lambda-calculi. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 400--414, Karpacz, Poland, September 2004. Springer. [ http ]
[15] Sébastien Bardin, Alain Finkel, and David Nowak. Toward symbolic verification of programs handling pointers. In Ramesh Bharadwaj, editor, Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Electronic Notes in Theoretical Computer Science, Barcelona, Spain, April 2004. Elsevier. To appear.
[16] Yu Zhang and David Nowak. Logical relations for dynamic name creation. In Matthias Baaz and Johann A. Makowsky, editors, Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Güdel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings, volume 2803 of Lecture Notes in Computer Science, pages 575--588, Vienna, Austria, August 2003. Springer. [ http ]
[17] Mickaël Kerbœuf, David Nowak, and Jean-Pierre Talpin. Formal proof of a polychronous protocol for loosely time-triggered architectures. In Jin Song Dong and Jim Woodcock, editors, Formal Methods and Software Engineering, 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, Proceedings, volume 2885 of Lecture Notes in Computer Science, pages 359--374, Singapore, November 2003. Springer. [ http ]
[18] Ranko Lazić and David Nowak. On a semantic definition of data independence. In Martin Hofmann, editor, Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings, volume 2701 of Lecture Notes in Computer Science, pages 226--240, Valencia, Spain, June 2003. Springer. [ http ]
[19] Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. In Julian C. Bradfield, editor, Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings, volume 2471 of Lecture Notes in Computer Science, pages 553--568, Edinburgh, Scotland, UK, September 2002. Springer. [ http ]
[20] Ranko Lazić and David Nowak. A unifying approach to data-independence. In Catuscia Palamidessi, editor, CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes in Computer Science, pages 581--595, Pennsylvania State University, Pennsylvania, USA, August 2000. Springer. [ http ]
[21] Mickaël Kerbœuf, David Nowak, and Jean-Pierre Talpin. Specification and verification of a steam-boiler with Signal-Coq. In Mark Aagaard and John Harrison, editors, Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, volume 1869 of Lecture Notes in Computer Science, pages 356--371, Portland, Oregon, USA, August 2000. Springer. [ http ]
[22] David Nowak, Jean-Pierre Talpin, and Paul Le Guernic. Synchronous structures. In Jos C. M. Baeten and Sjouke Mauw, editors, CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, volume 1664 of Lecture Notes in Computer Science, pages 494--509, Eindhoven, The Netherlands, August 1999. Springer. [ http ]
[23] Jean-Pierre Talpin and David Nowak. A synchronous semantics of higher-order processes for modeling reconfigurable reactive systems. In Vikraman Arvind and R. Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings, volume 1530 of Lecture Notes in Computer Science, pages 78--89, Chennai, India, December 1998. Springer. [ http ]
[24] David Nowak, Jean-René Beauvais, and Jean-Pierre Talpin. Co-inductive axiomatization of a synchronous language. In Jim Grundy and Malcolm C. Newey, editors, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98), volume 1479 of Lecture Notes in Computer Science, pages 387--399, Canberra, Australia, September 1998. Springer. [ http ]
[25] David Nowak, Jean-Pierre Talpin, Thierry Gautier, and Paul Le Guernic. An ML-like module system for the synchronous language Signal. In Christian Lengauer, Martin Griebl, and Sergei Gorlatch, editors, Euro-Par '97 Parallel Processing, Third International Euro-Par Conference, Passau, Germany, August 26-29, 1997, Proceedings, volume 1300 of Lecture Notes in Computer Science, pages 1244--1253, Passau, Germany, August 1997. Springer. [ http ]

Non Peer-reviewed Conferences

[1] David Nowak and Yu Zhang. A calculus for game-based security proofs (extended abstract). In Proceedings of the 2010 annual conference of the Japan Society for Industrial and Applied Mathematics (JSIAM), pages 57--58, Chiyoda, Tokyo, Japan, September 2010. [ http ]
[2] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. In Proceedings of the 2009 annual conference of the Japan Society for Industrial and Applied Mathematics (JSIAM), pages 53--54, Toyonaka, Osaka, Japan, September 2009. [ http ]
[3] David Nowak. A verification toolbox for cryptographic primitives (extended abstract). In Proceedings of the 2008 annual conference of the Japan Society for Industrial and Applied Mathematics (JSIAM), pages 181--182, Ichikawa, Chiba, Japan, September 2008. [ http ]

Others

[1] Andrei Arusoaie, David Nowak, Vlad Rusu, and Dorel Lucanu. Formal proof of soundness for an RL prover. Research Report RR-471, INRIA Lille - Nord Europe, Parc scientifique de la Haute-Borne, 40 avenue Halley, Bât A, Park Plaza, 59650 Villeneuve d'Ascq, December 2015. 27 pages. [ http ]
[2] Pierre Castéran, Jacques Garrigue, and David Nowak. NII Shonan school on Coq. NII Shonan Meeting Report 2014-9, National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-Ku, Tokyo, Japan, February 2015. 6 pages. [ .pdf ]
[3] Andrei Arusoaie, Dorel Lucanu, David Nowak, and Vlad Rusu. Verifying reachability-logic properties on rewriting-logic specifications (extended version). Technical Report 15-01, Faculty of Computer Science, University “Alexandru Ioan Cuza” of Iasi, Str. Berthelot 16, 6600-Iasi, Romania, February 2015. 24 pages. [ http ]
[4] Akitoshi Kawamura, Jean-Yves Marion, and David Nowak, editors. Implicit Computational Complexity and Applications: Resource Control, Security, Real-Number Computation, number 2013-13 in NII Shonan Meeting Report, 2-1-2 Hitotsubashi, Chiyoda-Ku, Tokyo, Japan, December 2013. 16 pages. [ .pdf ]
[5] Sylvain Heraud and David Nowak. A formalization of polytime functions. Research report 1102.5495, arXiv, February 2011. 13 pages. [ http ]
[6] David Nowak and Yu Zhang. A calculus for game-based security proofs. Research report 2010/230, Cryptology ePrint Archive, April 2010. 18 pages. [ http ]
[7] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. Research report 2009/322, Cryptology ePrint Archive, July 2009. 18 pages. [ http ]
[8] David Nowak. On formal verification of arithmetic-based cryptographic primitives. Research report 0904.1110, arXiv, April 2009. 13 pages. [ http ]
[9] David Nowak. A framework for game-based security proofs. Research report 2007/199, Cryptology ePrint Archive, May 2007. Revised in November 2007. 16 pages. [ http ]
[10] Slawomir Lasota, David Nowak, and Yu Zhang. On completeness of logical relations for monadic types. Research report cs.LO/0612106, arXiv, December 2006. 20 pages. [ http ]
[11] Stéphane Demri, Ranko Lazić, and David Nowak. On the freeze quantifier in Constraint LTL: decidability and complexity. Research report cs.LO/0609008, arXiv, September 2006. 29 pages. [ http ]
[12] Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. Research report cs.LO/0511006, arXiv, November 2005. Revised in March 2008. 83 pages. [ http ]
[13] Stéphane Demri and David Nowak. Reasoning about transfinite sequences. Research report cs.LO/0505073, arXiv, May 2005. Revised in August 2006. 38 pages. [ http ]
[14] Stéphane Demri, Ranko Lazić, and David Nowak. On the freeze quantifier in constraint LTL: Decidability and complexity. Research report LSV-05-03, Laboratoire Spécification et Vérification, ENS Cachan, April 2005. 13 pages. [ .pdf ]
[15] Alain Griffault, Frédéric Herbreteau, Gérald Point, Grégoire Sutre, Aymeric Vincent, Mihaela Sighireanu, Sébastien Bardin, Alain Finkel, and David Nowak. Intégration des outils persée. Deliverable, Livrable RC1 : Projet PERSÉE de l’ACI Sécurité Informatique, April 2005. 32 pages.
[16] Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, and Yu Zhang. Complete lax logical relations for cryptographic lambda-calculi. Research report LSV-04-4, Laboratoire Spécification et Vérification, École Normale Supérieure de Cachan, February 2004. 16 pages. [ .ps ]
[17] Sébastien Bardin, Alain Finkel, and David Nowak. Rapport final. Contract report, Contract P11L03/F01304/0 + 50.0241 between EDF and LSV, November 2003. 50 pages.
[18] Sébastien Bardin, Alain Finkel, and David Nowak. Note de synthèse à 10 mois. Contract report, Contract P11L03/F01304/0 + 50.0241 between EDF and LSV, August 2003. 21 pages.
[19] Sébastien Bardin, Alain Finkel, David Nowak, and Philippe Schnoebelen. Note de synthèse à 6 mois. Contract report, Contract P11L03/F01304/0 + 50.0241 between EDF and LSV, July 2003. 43 pages.
[20] Ranko Lazić and David Nowak. On a semantic definition of data independence. Research report CS-RR-392, Department of Computer Science, University of Warwick, December 2002. 20 pages. [ .ps.gz ]
[21] David Nowak, editor. Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS'01), number PRG-RR-01-07 in Programming Research Group research reports, Oxford, England, UK, April 2001. [ .ps.gz ]
[22] Ranko Lazić and David Nowak. A unifying approach to data-independence. Technical Report PRG-TR-4-00, Oxford University Computing Laboratory (OUCL), June 2000. 30 pages. [ .ps.gz ]
[23] Mickaël Kerbœuf, David Nowak, and Jean-Pierre Talpin. The steam boiler controller problem in Signal-Coq. Research report 3773, Institut National de Recherche en Informatique et Automatique (INRIA), October 1999. 59 pages. [ .html ]
[24] Mickaël Kerbœuf, David Nowak, and Jean-Pierre Talpin. The steam boiler controller problem in Signal-Coq. Internal Publication 1266, Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), October 1999. 59 pages. [ http ]
[25] David Nowak. Spécification et preuve de systèmes réactifs. PhD thesis, Université de Rennes 1, October 1999. 176 pages. [ .ps.gz ]
[26] David Nowak. The semantics of Tuplink. Research report RT0292, IBM Japan Ltd., Tokyo Research Laboratory, September 1998.
[27] David Nowak, Jean-Pierre Talpin, and Thierry Gautier. Un système de modules avancé pour Signal. Research report 3176, Institut National de Recherche en Informatique et Automatique (INRIA), June 1997. 34 pages. [ .html ]
[28] David Nowak, Jean-Pierre Talpin, and Thierry Gautier. Un système de modules avancé pour Signal. Internal Publication 1109, Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), June 1997. 34 pages. [ http ]

This web page has been partly generated by bibtex2html