|
[1]
|
David Nowak and Vlad Rusu.
While loops in Coq.
In Horatiu Cheval, Laurentiu Leustean, and Andrei Sipos, editors,
Proceedings 7th Symposium on Working Formal Methods, FROM 2023,
Bucharest, Romania, 21-22 September 2023, volume 389 of EPTCS, pages
96--109, 2023.
[ http ]
|
|
[2]
|
Vlad Rusu and David Nowak.
Towards corecursion without corecursion in Coq.
In Stefan Ciobaca and Keisuke Nakano, editors, 9th International
Workshop on Rewriting Techniques for Program Transformations and Evaluation,
WPTE 2022, Haifa, Israel, July 31, 2022. Proceedings, number 8442, Haifa,
Israel, July 2022.
[ http ]
|
|
[3]
|
Vlad Rusu and David Nowak.
Defining corecursive functions in Coq using approximations.
In Karim Ali and Jan Vitek, editors, 36th European Conference on
Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany,
volume 222 of LIPIcs, pages 12:1--12:24. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2022.
[ http ]
|
|
[4]
|
Florian Vanhems, Vlad Rusu, David Nowak, and Gilles Grimaud.
A formal correctness proof for an EDF scheduler implementation.
In 28th IEEE Real-Time and Embedded Technology and
Applications Symposium, RTAS 2022, Milano, Italy, May 4-6, 2022, pages
281--292. IEEE, 2022.
[ http ]
|
|
[5]
|
Célestine Sauvage, Reynald Affeldt, and David Nowak.
Vers la formalisation en Coq des transformateurs de monades
modulaires.
In Zaynah Dargaye and Yann Regis-Gianas, editors,
Trente-et-unièmes Journées Francophones des Langages Applicatifs,
JFLA 2020, Gruissan, France, 29 janvier - 1er février 2020.
Proceedings, pages 23--30, Gruissan, France, January 2020.
[ http ]
|
|
[6]
|
Reynald Affeldt and David Nowak.
Extending equational monadic reasoning with monad transformers.
In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors,
26th International Conference on Types for Proofs and Programs, TYPES
2020, March 2-5, 2020, University of Turin, Italy, volume 188 of
LIPIcs, pages 2:1--2:21. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2020.
[ http ]
|
|
[7]
|
Florian Vanhems, Narjes Jomaa, Samuel Hym, and David Nowak.
On the proof-oriented design of a context-switching service in the
Pip protokernel.
In Mads Dam and David Nowak, editors, ENabling TRust through Os
Proofs... and beYond - 2nd International Workshop, ENTROPY 2019, Stockholm,
Sweden, June 16, 2019. Proceedings, June 2019.
[ .pdf ]
|
|
[8]
|
Reynald Affeldt, David Nowak, and Takafumi Saikawa.
A hierarchy of monadic effects for program verification using
equational reasoning.
In Graham Hutton, editor, Mathematics of Program Construction -
13th International Conference, MPC 2019, Porto, Portugal, October 7-9,
2019, Proceedings, volume 11825 of Lecture Notes in Computer Science,
pages 226--254. Springer, 2019.
[ http ]
|
|
[9]
|
Vlad Rusu and David Nowak.
(Co)inductive proof systems for compositional proofs in
reachability logic.
In Mircea Marin and Adrian Craciun, editors, Proceedings Third
Symposium on Working Formal Methods, FROM 2019, Timisoara, Romania,
3-5 September 2019, volume 303 of EPTCS, pages 32--47, 2019.
[ http ]
|
|
[10]
|
Narjes Jomaa, Samuel Hym, and David Nowak.
La conception d'un noyau orientée par sa preuve d'isolation
mémoire.
In Compas 2018, Juillet 2018, Toulouse, France, July 2018.
[ http ]
|
|
[11]
|
Narjes Jomaa, Paolo Torrini, David Nowak, Gilles Grimaud, and Samuel Hym.
Proof-oriented design of a separation kernel with minimal trusted
computing base.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 76, 2018.
[ http ]
|
|
[12]
|
Paolo Torrini, David Nowak, Narjes Jomaa, and Mohamed Sami Cherif.
Formalising executable specifications of low-level systems.
In Ruzica Piskac and Philipp Rümmer, editors, Verified
Software. Theories, Tools, and Experiments - 10th International Conference,
VSTTE 2018, Oxford, UK, July 18-19, 2018, Revised Selected Papers, volume
11294 of Lecture Notes in Computer Science, pages 155--176. Springer,
2018.
[ http ]
|
|
[13]
|
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 ]
|
|
[14]
|
Andrei Arusoaie, David Nowak, Vlad Rusu, and Dorel Lucanu.
A certified procedure for RL verification.
In Tudor Jebelean, Viorel Negru, Dana Petcu, Daniela Zaharie, Tetsuo
Ida, and Stephen M. Watt, editors, 19th International Symposium on
Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017,
Timisoara, Romania, September 21-24, 2017, pages 129--136. IEEE Computer
Society, 2017.
[ http ]
|
|
[15]
|
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 ]
|
|
[16]
|
Narjes Jomaa, David Nowak, Gilles Grimaud, and Julien Iguchi-Cartigny.
Preuve formelle d'isolation mémoire dynamique à base de
MMU.
In David Baelde and Jade Alglave, editors, Vingt-sixièmes
Journées Francophones des Langages Applicatifs, JFLA 2015, Le Val
d'Ajol, France, 7 - 10 Janvier 2015. Proceedings, pages 297--300, Le Val
d'Ajol, France, January 2015.
[ http ]
|
|
[17]
|
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 ]
|
|
[18]
|
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 ]
|
|
[19]
|
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 ]
|
|
[20]
|
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 ]
|
|
[21]
|
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 ]
|
|
[22]
|
Reynald Affeldt, David Nowak, and Kiyoshi Yamada.
Certifying assembly with formal cryptographic proofs: the case of
BBS.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 23, 2009.
[ http ]
|
|
[23]
|
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 ]
|
|
[24]
|
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 ]
|
|
[25]
|
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 ]
|
|
[26]
|
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 ]
|
|
[27]
|
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 ]
|
|
[28]
|
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.
|
|
[29]
|
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 ]
|
|
[30]
|
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 ]
|
|
[31]
|
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 ]
|
|
[32]
|
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 ]
|
|
[33]
|
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 ]
|
|
[34]
|
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 ]
|
|
[35]
|
Mickaël Kerboeuf, David Nowak, and Jean-Pierre Talpin.
Specification and verification of a steam-boiler with Signal-Coq.
In Mark D. 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 ]
|
|
[36]
|
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 ]
|
|
[37]
|
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 ]
|
|
[38]
|
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 ]
|
|
[39]
|
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 ]
|
|
[1]
|
Reynald Affeldt and David Nowak.
Extending equational monadic reasoning with monad transformers.
CoRR, abs/2011.03463, 2020.
[ http ]
|
|
[2]
|
Reynald Affeldt, Jacques Garrigue, David Nowak, and Takafumi Saikawa.
A trustful monad for axiomatic reasoning with probability and
nondeterminism.
CoRR, abs/2003.09993, 2020.
[ http ]
|
|
[3]
|
Julien Cartigny, Mahieddine Yaker, Quentin Bergougnoux, David Nowak, and Gilles
Grimaud.
Isolation API.
Deliverable D1.2, Celtic-Plus: On Demand Secure Isolation, January
2018.
22 pages.
[ .pdf ]
|
|
[4]
|
Narjes Jomaa, Gilles Grimaud, Samuel Hym, David Nowak, and Paolo Torrini.
Abstract model of the isolation manager.
Deliverable D1.1, Celtic-Plus: On Demand Secure Isolation, June 2017.
21 pages.
[ .pdf ]
|
|
[5]
|
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 ]
|
|
[6]
|
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 ]
|
|
[7]
|
Pierre Castéran, Jacques Garrigue, and David Nowak.
Summer school on Coq (NII shonan meeting 2014-9).
NII Shonan Meet. Rep., 2014, 2014.
[ http ]
|
|
[8]
|
Akitoshi Kawamura, Jean-Yves Marion, and David Nowak.
Implicit computational complexity and applications: Resource control,
security, real-number computation (NII shonan meeting 2013-13).
NII Shonan Meet. Rep., 2013, 2013.
[ http ]
|
|
[9]
|
Sylvain Heraud and David Nowak.
A formalization of polytime functions.
CoRR, abs/1102.5495, 2011.
[ http ]
|
|
[10]
|
David Nowak and Yu Zhang.
A calculus for game-based security proofs.
IACR Cryptol. ePrint Arch., page 230, 2010.
[ http ]
|
|
[11]
|
David Nowak.
On formal verification of arithmetic-based cryptographic primitives.
CoRR, abs/0904.1110, 2009.
[ http ]
|
|
[12]
|
Reynald Affeldt, David Nowak, and Kiyoshi Yamada.
Certifying assembly with formal cryptographic proofs: the case of
BBS.
IACR Cryptol. ePrint Arch., page 322, 2009.
[ http ]
|
|
[13]
|
David Nowak.
A framework for game-based security proofs.
IACR Cryptol. ePrint Arch., page 199, 2007.
[ http ]
|
|
[14]
|
Stéphane Demri, Ranko Lazic, and David Nowak.
On the freeze quantifier in constraint LTL: decidability and
complexity.
CoRR, abs/cs/0609008, 2006.
[ http ]
|
|
[15]
|
Slawomir Lasota, David Nowak, and Yu Zhang.
On completeness of logical relations for monadic types.
CoRR, abs/cs/0612106, 2006.
[ http ]
|
|
[16]
|
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 RC1, Projet PERSÉE de l'ACI Sécurité
Informatique, April 2005.
32 pages.
|
|
[17]
|
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 ]
|
|
[18]
|
Stéphane Demri and David Nowak.
Reasoning about transfinite sequences.
CoRR, abs/cs/0505073, 2005.
[ http ]
|
|
[19]
|
Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak.
Logical relations for monadic types.
CoRR, abs/cs/0511006, 2005.
[ http ]
|
|
[20]
|
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 ]
|
|
[21]
|
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.
|
|
[22]
|
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.
|
|
[23]
|
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.
|
|
[24]
|
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 ]
|
|
[25]
|
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 ]
|
|
[26]
|
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 ]
|
|
[27]
|
David Nowak.
Spécification et preuve de systèmes réactifs.
PhD thesis, Université de Rennes 1, October 1999.
176 pages.
[ .ps.gz ]
|
|
[28]
|
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 ]
|
|
[29]
|
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 ]
|
|
[30]
|
David Nowak.
The semantics of Tuplink.
Research report RT0292, IBM Japan Ltd., Tokyo Research Laboratory,
September 1998.
|
|
[31]
|
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 ]
|
|
[32]
|
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 ]
|