David Nowak

ダヴィッド ノヴァック

CRIStAL, CNRS & University of Lille

Publications

Peer-reviewed Journals

[1] Narjes Jomaa, David Nowak, Gilles Grimaud, and Samuel Hym. Formal proof of dynamic memory isolation based on MMU. Sci. Comput. Program., July 2017. In press. [ http ]
[2] David Nowak and Yu Zhang. Formal security proofs with minimal fuss: Implicit computational complexity at work. Inf. Comput., 241:96--113, 2015. [ http ]
[3] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal security proofs: The case of BBS. Sci. Comput. Program., 77(10-11):1058--1074, 2012. [ http ]
[4] Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. Mathematical Structures in Computer Science, 18(6):1169--1217, 2008. [ http ]
[5] Stéphane Demri and David Nowak. Reasoning about transfinite sequences. Int. J. Found. Comput. Sci., 18(1):87--112, 2007. [ http ]
[6] Stéphane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput., 205(1):2--24, 2007. [ http ]
[7] David Nowak. Synchronous structures. Inf. Comput., 204(8):1295--1324, 2006. [ http ]

Peer-reviewed Conferences

[1] Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak. Formal proof of polynomial-time complexity with quasi-interpretations. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 146--157. ACM, 2018. [ http ]
[2] Andrei Arusoaie, David Nowak, Vlad Rusu, and Dorel Lucanu. A certified procedure for RL verification. In Juan Guerrero, editor, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), September 21-24, 2017, Timisoara, Romania, Timisoara, Romania, September 2017. IEEE. To appear. [ http ]
[3] Narjes Jomaa, David Nowak, Gilles Grimaud, and Samuel Hym. Formal proof of dynamic memory isolation based on MMU. In 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016, Shanghai, China, July 17-19, 2016, pages 73--80. IEEE Computer Society, 2016. [ http ]
[4] 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 L. Talcott, editors, Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, volume 9200 of Lecture Notes in Computer Science, pages 451--474. Springer, 2015. [ http ]
[5] Narjes Jomaa, David Nowak, Gilles Grimaud, and Julien Iguchi-Cartigny. Preuve formelle d'isolation mémoire dynamique à base de MMU. In Vingt-sixièmes Journées Francophones des Langages Applicatifs, JFLA 2015, Le Val d'Ajol, France, January 7-10, 2015. Proceedings, pages 297--300, Le Val d'Ajol, France, January 2015. [ http ]
[6] 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 sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012, pages 27--36. ACM, 2012. [ http ]
[7] 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. Springer, 2011. [ http ]
[8] 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. Springer, 2010. [ http ]
[9] 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 ]
[10] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. ECEASST, 23, 2009. [ http ]
[11] 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, Revised Selected Papers, volume 5461 of Lecture Notes in Computer Science, pages 368--382. Springer, 2008. [ http ]
[12] 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. Springer, 2007. [ http ]
[13] 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 and Related Issues, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Revised Selected Papers, volume 4435 of Lecture Notes in Computer Science, pages 223--230. Springer, 2006. [ http ]
[14] Stéphane Demri, Ranko Lazic, 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. IEEE Computer Society, 2005. [ http ]
[15] Stéphane Demri and David Nowak. Reasoning about transfinite sequences. 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. Springer, 2005. [ http ]
[16] Sébastien Bardin, Alain Finkel, and David Nowak. Toward symbolic verification of programs handling pointers. In Ramesh Bharadwaj, editor, 3rd International Workshop on Automated Verification of Infinite-State Systems, AVIS'04, Barcelona, Spain, April 3-4, 2004. Proceedings, Electronic Notes in Theoretical Computer Science, Barcelona, Spain, April 2004. Elsevier. To appear.
[17] 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. Springer, 2004. [ http ]
[18] Ranko Lazic 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. Springer, 2003. [ http ]
[19] Mickaël Kerboeuf, 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. Springer, 2003. [ http ]
[20] 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. Springer, 2003. [ http ]
[21] 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. Springer, 2002. [ http ]
[22] Mickaël Kerboeuf, 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. Springer, 2000. [ http ]
[23] Ranko Lazic 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. Springer, 2000. [ http ]
[24] 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. Springer, 1999. [ http ]
[25] David Nowak, Jean-René Beauvais, and Jean-Pierre Talpin. Co-inductive axiomatization of a synchronous language. In Jim Grundy and Malcolm C. Newey, editors, Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, volume 1479 of Lecture Notes in Computer Science, pages 387--399. Springer, 1998. [ http ]
[26] Jean-Pierre Talpin and David Nowak. A synchronous semantics of higher-order processes for modeling reconfigurable reactive systems. In Vikraman Arvind and Ramaswamy 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. Springer, 1998. [ http ]
[27] 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. Springer, 1997. [ 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. CoRR, abs/1102.5495, 2011. [ http ]
[6] David Nowak and Yu Zhang. A calculus for game-based security proofs. IACR Cryptology ePrint Archive, 2010:230, 2010. [ http ]
[7] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. IACR Cryptology ePrint Archive, 2009:322, 2009. [ http ]
[8] David Nowak. On formal verification of arithmetic-based cryptographic primitives. CoRR, abs/0904.1110, 2009. [ http ]
[9] David Nowak. A framework for game-based security proofs. IACR Cryptology ePrint Archive, 2007:199, 2007. [ http ]
[10] Slawomir Lasota, David Nowak, and Yu Zhang. On completeness of logical relations for monadic types. CoRR, abs/cs/0612106, 2006. [ http ]
[11] Stéphane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: decidability and complexity. CoRR, abs/cs/0609008, 2006. [ http ]
[12] 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 ]
[13] 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.
[14] Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. CoRR, abs/cs/0511006, 2005. [ http ]
[15] Stéphane Demri and David Nowak. Reasoning about transfinite sequences. CoRR, abs/cs/0505073, 2005. [ http ]
[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. [ .pdf ]
[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. [ http ]
[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. [ .html ]
[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. [ .html ]
[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. [ http ]
[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. [ .ps.gz ]
[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. [ http ]
[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. [ .ps.gz ]

This web page has been partly generated by bibtex2html