%%% ==================================================================== %%% BibTeX-file{ %%% author = {David Nowak}, %%% date = {1 February 2012}, %%% filename = {NowakDJJ.bib}, %%% url = {http://staff.aist.go.jp/david.nowak/NowakDJJ.bib}, %%% www-home = {http://staff.aist.go.jp/david.nowak/}, %%% address = {DeITy, ITRI, AIST, Japan}, %%% telephone = {}, %%% FAX = {}, %%% FTP-archive = {}, %%% email = {}, %%% dates = {197?--}, %%% keywords = {}, %%% supported = {yes}, %%% supported-by = {David Nowak}, %%% abstract = {Bibliography for David Nowak} %%% } %%% ==================================================================== @article{NowakDJJ:cerafs, author = {Affeldt, Reynald and Nowak, David and Yamada, Kiyoshi}, title = {Certifying Assembly with Formal Security Proofs: the Case of {BBS}}, journal = {Science of Computer Programming}, publisher = {Elsevier}, booktitle = {special issue on Automated Verification of Critical Systems}, OPTeditor = {Roggenbach, Markus}, month = {}, year = {2011}, volume = {}, number = {}, pages = {}, url = {http://dx.doi.org/10.1016/j.scico.2011.07.003}, note = {In press.}, } @article{NowakDJJ:logrmt4, author = {Goubault-Larrecq, Jean and Lasota, Slawomir and Nowak, David}, title = {Logical Relations for Monadic Types}, journal = {Mathematical Structures in Computer Science}, publisher = {Cambridge University Press}, month = Dec, year = {2008}, volume = {18}, number = {6}, pages = {1169--1217}, url = {http://dx.doi.org/10.1017/S0960129508007172}, } @article{NowakDJJ:reats2, author = {Demri, St{\'e}phane and Nowak, David}, title = {Reasoning about transfinite sequences}, booktitle = {Special Issue: Automated Technology for Verification and Analysis (ATVA 2005)}, OPTeditor = {Peled, Doron A. and Tsay, Yih-Kuen}, journal = {International Journal of Foundations of Computer Science}, publisher = {World Scientific}, month = Feb, year = {2007}, volume = {18}, number = {1}, pages = {87--112}, url = {http://dx.doi.org/10.1142/S0129054107004589}, } @article{NowakDJJ:freqcl3, author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Nowak, David}, title = {On the freeze quantifier in {C}onstraint {LTL}: decidability and complexity}, booktitle = {Special Issue: TIME 2005}, OPTeditor = {Chomicki, Jan and Toman, David}, journal = {Information and Computation}, publisher = {Elsevier}, month = Jan, year = {2007}, volume = {205}, number = {1}, pages = {2--24}, url = {http://dx.doi.org/10.1016/j.ic.2006.08.003}, } @article{NowakDJJ:syns2, author = {Nowak, David}, title = {Synchronous Structures}, journal = {Information and Computation}, publisher = {Elsevier}, month = Aug, year = {2006}, volume = {204}, number = {8}, pages = {1295--1324}, url = {http://dx.doi.org/10.1016/j.ic.2001.05.001}, } @inproceedings{NowakDJJ:fornpp, author = {Affeldt, Reynald and Nowak, David and Oiwa, Yutaka}, title = {Formal Network Packet Processing with Minimal Fuss: Invertible Syntax Descriptions at Work}, booktitle = {Proceedings of the 6th ACM Workshop Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012}, OPTeditor = {Koen Claessen and Nikhil Swamy}, OPTaddress = {Philadelphia, PA, USA}, OPTmonth = Jan, OPTyear = {2012}, pages = {27-36}, publisher = {ACM}, OPTisbn = {978-1-4503-1125-0}, url = {http://dx.doi.org/10.1145/2103776.2103781}, } @inproceedings{NowakDJJ:forpf2, author = {Heraud, Sylvain and Nowak, David}, title = {A Formalization of Polytime Functions}, booktitle = {Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings}, OPTeditor = {Marko C. J. D. van Eekelen and Herman Geuvers and Julien Schmaltz and Freek Wiedijk}, OPTaddress = {Nijmegen, The Netherlands}, OPTmonth = Aug, OPTyear = {2011}, volume = {6898}, pages = {119--134}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, OPTisbn = {978-3-642-22862-9}, url = {http://dx.doi.org/10.1007/978-3-642-22863-6_11}, } @inproceedings{NowakDJJ:calgsp2, author = {Nowak, David and Zhang, Yu}, title = {A Calculus for Game-Based Security Proofs}, booktitle = {Provable Security - 4th International Conference, ProvSec 2010, Malacca, Malaysia, October 13-15, 2010. Proceedings}, OPTeditor = {Heng, Swee-Huay and Kurosawa, Kaoru}, OPTaddress = {Malacca, Malaysia}, OPTmonth = Oct, OPTyear = 2010, volume = {6402}, pages = {35--52}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, OPTisbn = {978-3-642-16279-4}, url = {http://dx.doi.org/10.1007/978-3-642-16280-0_3}, } @inproceedings{NowakDJJ:cerafc3, author = {Affeldt, Reynald and Nowak, David and Yamada, Kiyoshi}, title = {Certifying Assembly with Formal Cryptographic Proofs: the Case of {BBS}}, booktitle = {Automated Verification of Critical Systems 2009}, OPTeditor = {Roggenbach, Markus}, OPTaddress = {Swansea, UK}, OPTmonth = Sep, OPTyear = {2009}, volume = {23}, pages = {}, series = {Electronic Communications of the EASST}, publisher = {EASST}, OPTisbn = {}, url = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/article/view/316}, } @inproceedings{NowakDJJ:towcic, author = {Nowak, David and Yamada, Kiyoshi}, title = {Towards a certified implementation of a cryptographically secure pseudorandom bit generator}, booktitle = {The 11th JSSST Workshop on Programming and Programming Languages (PPL 2009)}, OPTeditor = {}, OPTaddress = {Takayama, Japan}, OPTmonth = Mar, OPTyear = {2009}, OPTvolume = {}, pages = {16--20}, OPTseries = {}, OPTpublisher = {}, OPTisbn = {}, url = {http://millsmess.cs.uec.ac.jp/ppl2009/}, } @inproceedings{NowakDJJ:forvac, author = {Nowak, David}, title = {On Formal Verification of Arithmetic-Based Cryptographic Primitives}, booktitle = {Information Security and Cryptology - ICISC 2008, 11th International Conference, Seoul, Korea, December 3-5, 2008, Proceedings}, OPTeditor = {Lee, Pil Joong and Cheon, Jung Hee}, OPTaddress = {Seoul, Korea}, OPTmonth = Dec, OPTyear = {2008}, volume = {5461}, pages = {368--382}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-00729-3}, url = {http://dx.doi.org/10.1007/978-3-642-00730-9_23}, } @inproceedings{NowakDJJ:fragsp2, author = {Nowak, David}, title = {A Framework for Game-Based Security Proofs}, booktitle = {Information and Communications Security, 9th International Conference, ICICS 2007, Zhengzhou, China, December 12-15, 2007, Proceedings}, OPTeditor = {Qing, Sihan and Imai, Hideki and Wang, Guilin}, OPTaddress = {Zhengzhou, China}, OPTmonth = Dec, OPTyear = {2008}, volume = {4861}, pages = {319--333}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-77047-3}, url = {http://dx.doi.org/10.1007/978-3-540-77048-0_25}, } @inproceedings{NowakDJJ:comlrmt, author = {Lasota, Slawomir and Nowak, David and Zhang, Yu}, title = {On completeness of logical relations for monadic types}, booktitle = {Advances in Computer Science - ASIAN 2006, Secure Software, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Proceedings}, OPTeditor = {Okada, Mitsu and Satoh, Ichiro}, OPTaddress = {Tokyo, Japan}, OPTmonth = Jan, OPTyear = {2008}, volume = {4435}, pages = {223--230}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-77504-1}, url = {http://dx.doi.org/10.1007/978-3-540-77505-8_17}, } @inproceedings{NowakDJJ:reatsea, author = {Demri, St{\'e}phane and Nowak, David}, title = {Reasoning about transfinite sequences (extended abstract)}, booktitle = {Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005. Proceedings}, OPTeditor = {Peled, Doron A. and Tsay, Yih-Kuen}, OPTaddress = {Taipei, Taiwan}, OPTmonth = Oct, OPTyear = {2005}, volume = {3707}, pages = {248--262}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-29209-8}, url = {http://dx.doi.org/10.1007/11562948_20}, } @inproceedings{NowakDJJ:freqcl, author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Nowak, David}, title = {On the freeze quantifier in {C}onstraint {LTL}: decidability and complexity}, booktitle = {12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA}, OPTeditor = {}, OPTaddress = {Burlington, Vermont, USA}, OPTmonth = Jun, OPTyear = {2005}, OPTvolume = {}, pages = {113--121}, OPTseries = {}, publisher = {IEEE Computer Society}, isbn = {0-7695-2370-6}, url = {http://dx.doi.org/10.1109/TIME.2005.28}, } @inproceedings{NowakDJJ:comllr, author = {Goubault-Larrecq, Jean and Lasota, Slawomir and Nowak, David and Zhang, Yu}, title = {Complete lax logical relations for cryptographic lambda-calculi}, booktitle = {Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings}, OPTeditor = {Marcinkowski, Jerzy and Tarlecki, Andrzej}, OPTaddress = {Karpacz, Poland}, OPTmonth = Sep, OPTyear = {2004}, volume = {3210}, pages = {400--414}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-23024-3}, url = {http://dx.doi.org/10.1007/b100120}, } @inproceedings{NowakDJJ:towsvp, author = {Bardin, S{\'e}bastien and Finkel, Alain and Nowak, David}, title = {Toward symbolic verification of programs handling pointers}, booktitle = {Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04)}, OPTeditor = {Bharadwaj, Ramesh}, address = {Barcelona, Spain}, month = Apr, year = {2004}, OPTvolume = {}, OPTpages = {}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, note = {To appear}, } @inproceedings{NowakDJJ:logrdn, author = {Zhang, Yu and Nowak, David}, title = {Logical Relations for Dynamic Name Creation}, booktitle = {Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G{\"u}del Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings}, OPTeditor = {Baaz, Matthias and Makowsky, Johann A.}, OPTaddress = {Vienna, Austria}, OPTmonth = Aug, OPTyear = {2003}, volume = {2803}, pages = {575--588}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-40801-7}, url = {http://dx.doi.org/10.1007/b13224}, } @inproceedings{NowakDJJ:forppp, author = {Kerb{\oe}uf, Micka{\"e}l and Nowak, David and Talpin, Jean-Pierre}, title = {Formal proof of a polychronous protocol for loosely time-triggered architectures}, booktitle = {Formal Methods and Software Engineering, 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, Proceedings}, OPTeditor = {Song Dong, Jin and Woodcock, Jim}, OPTaddress = {Singapore}, OPTmonth = Nov, OPTyear = {2003}, volume = {2885}, pages = {359--374}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-20461-9}, url = {http://dx.doi.org/10.1007/b94115}, } @inproceedings{NowakDJJ:semddi, author = {Lazi{\'c}, Ranko and Nowak, David}, title = {On a Semantic Definition of Data Independence}, booktitle = {Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings}, OPTeditor = {Hofmann, Martin}, OPTaddress = {Valencia, Spain}, OPTmonth = Jun, OPTyear = {2003}, volume = {2701}, pages = {226--240}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-40332-6}, url = {http://dx.doi.org/10.1007/3-540-44904-3_16}, } @inproceedings{NowakDJJ:logrmt, author = {Goubault-Larrecq, Jean and Lasota, Slawomir and Nowak, David}, title = {Logical Relations for Monadic Types}, booktitle = {Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings}, OPTeditor = {Bradfield, Julian C.}, OPTaddress = {Edinburgh, Scotland, UK}, OPTmonth = Sep, OPTyear = {2002}, volume = {2471}, pages = {553--568}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-44240-0}, url = {http://dx.doi.org/10.1007/3-540-45793-3_37}, } @inproceedings{NowakDJJ:uniadi, author = {Lazi{\'c}, Ranko and Nowak, David}, title = {A Unifying Approach to Data-independence}, booktitle = {CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings}, OPTeditor = {Palamidessi, Catuscia}, OPTaddress = {Pennsylvania State University, Pennsylvania, USA}, OPTmonth = Aug, OPTyear = {2000}, volume = {1877}, pages = {581--595}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-67897-7}, url = {http://dx.doi.org/10.1007/3-540-44618-4_41}, } @inproceedings{NowakDJJ:spevsb, author = {Kerb{\oe}uf, Micka{\"e}l and Nowak, David and Talpin, Jean-Pierre}, title = {Specification and Verification of a Steam-Boiler with {S}ignal-{C}oq}, booktitle = {Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings}, OPTaddress = {Portland, Oregon, USA}, OPTeditor = {Aagaard, Mark and Harrison, John}, OPTmonth = Aug, OPTyear = {2000}, volume = {1869}, pages = {356--371}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-67863-2}, url = {http://dx.doi.org/10.1007/3-540-44659-1_22}, } @inproceedings{NowakDJJ:syns, author = {Nowak, David and Talpin, Jean-Pierre and Le Guernic, Paul}, title = {Synchronous Structures}, booktitle = {CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings}, OPTeditor = {Baeten, Jos C. M. and Mauw, Sjouke}, OPTaddress = {Eindhoven, The Netherlands}, OPTmonth = Aug, OPTyear = {1999}, volume = {1664}, pages = {494--509}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-66425-3}, url = {http://dx.doi.org/10.1007/3-540-48320-9_34}, } @inproceedings{NowakDJJ:synsho, author = {Talpin, Jean-Pierre and Nowak, David}, title = {A Synchronous Semantics of Higher-Order Processes for Modeling Reconfigurable Reactive Systems}, booktitle = {Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings}, OPTeditor = {Arvind, Vikraman and Ramanujam, R.}, OPTaddress = {Chennai, India}, OPTmonth = Dec, OPTyear = {1998}, volume = {1530}, pages = {78--89}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-65384-4}, url = {http://dx.doi.org/10.1007/b71635}, } @inproceedings{NowakDJJ:coias, author = {Nowak, David and Beauvais, Jean-Ren{\'e} and Talpin, Jean-Pierre}, title = {Co-Inductive Axiomatization of a Synchronous Language}, booktitle = {Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98)}, OPTeditor = {Grundy, Jim and Newey, Malcolm C.}, OPTaddress = {Canberra, Australia}, OPTmonth = Sep, OPTyear = {1998}, volume = {1479}, pages = {387--399}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-64987-8}, url = {http://dx.doi.org/10.1007/BFb0055148}, } @inproceedings{NowakDJJ:mllms, author = {Nowak, David and Talpin, Jean-Pierre and Gautier, Thierry and Le Guernic, Paul}, title = {An {ML}-Like Module System for the Synchronous Language {S}ignal}, booktitle = {Euro-Par '97 Parallel Processing, Third International Euro-Par Conference, Passau, Germany, August 26-29, 1997, Proceedings}, OPTeditor = {Lengauer, Christian and Griebl, Martin and Gorlatch, Sergei}, OPTaddress = {Passau, Germany}, OPTmonth = Aug, OPTyear = {1997}, volume = {1300}, pages = {1244--1253}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-63440-9}, url = {http://dx.doi.org/10.1007/BFb0002880}, } @conference{NowakDJJ:calgsp3, title = {A Calculus for Game-based Security Proofs (extended abstract)}, author = {Nowak, David and Zhang, Yu}, booktitle = {Proceedings of the 2010 annual conference of the Japan Society for Industrial and Applied Mathematics (JSIAM)}, address = {Chiyoda, Tokyo, Japan}, month = Sep, year = {2010}, issn = {1345-3378}, pages = {57--58}, url = {http://www.jsiam.org/annualmeeting/2010}, } @conference{NowakDJJ:cerafc2, title = {Certifying Assembly with Formal Cryptographic Proofs: the Case of {BBS}}, author = {Affeldt, Reynald and Nowak, David and Yamada, Kiyoshi}, booktitle = {Proceedings of the 2009 annual conference of the Japan Society for Industrial and Applied Mathematics (JSIAM)}, address = {Toyonaka, Osaka, Japan}, month = Sep, year = {2009}, issn = {1345-3378}, pages = {53--54}, url = {http://www.jsiam.org/annualmeeting/2009}, } @techreport{NowakDJJ:forpf, author = {Heraud, Sylvain and Nowak, David}, title = {A Formalization of Polytime Functions}, institution = {arXiv}, month = Feb, year = {2011}, number = {1102.5495}, type = {Research report}, note = {13 pages}, url = {http://arxiv.org/abs/1102.5495}, } @techreport{NowakDJJ:calgsp, author = {Nowak, David and Zhang, Yu}, title = {A calculus for game-based security proofs}, institution = {Cryptology ePrint Archive}, month = Apr, year = {2010}, note = {18 pages}, number = {2010/230}, type = {Research report}, url = {http://eprint.iacr.org/2010/230}, } @techreport{NowakDJJ:cerafc, author = {Affeldt, Reynald and Nowak, David and Yamada, Kiyoshi}, title = {Certifying Assembly with Formal Cryptographic Proofs: the Case of {BBS}}, institution = {Cryptology ePrint Archive}, month = Jul, year = {2009}, note = {18 pages}, number = {2009/322}, type = {Research report}, url = {http://eprint.iacr.org/2009/322}, } @techreport{NowakDJJ:forvac2, author = {Nowak, David}, title = {On Formal Verification of Arithmetic-Based Cryptographic Primitives}, institution = {arXiv}, month = Apr, year = {2009}, number = {0904.1110}, type = {Research report}, note = {13 pages}, url = {http://arxiv.org/abs/0904.1110}, } @conference{NowakDJJ:vertcp, title = {A Verification Toolbox for Cryptographic Primitives (extended abstract)}, author = {Nowak, David}, booktitle = {Proceedings of the 2008 annual conference of the Japan Society for Industrial and Applied Mathematics (JSIAM)}, address = {Ichikawa, Chiba, Japan}, month = Sep, year = {2008}, issn = {1345-3378}, pages = {181--182}, url = {http://www.jsiam.org/annualmeeting/2008}, } @techreport{NowakDJJ:fragsp, author = {Nowak, David}, title = {A Framework for Game-Based Security Proofs}, institution = {Cryptology ePrint Archive}, month = May, year = {2007}, note = {Revised in November 2007. 16 pages}, number = {2007/199}, type = {Research report}, url = {http://eprint.iacr.org/2007/199}, } @techreport{NowakDJJ:comlrmt2, author = {Lasota, Slawomir and Nowak, David and Zhang, Yu}, title = {On completeness of logical relations for monadic types}, institution = {arXiv}, month = Dec, year = {2006}, number = {cs.LO/0612106}, type = {Research report}, note = {20 pages}, url = {http://arXiv.org/abs/cs.LO/0612106}, } @techreport{NowakDJJ:freqcl4, author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Nowak, David}, title = {On the freeze quantifier in {C}onstraint {LTL}: decidability and complexity}, institution = {arXiv}, month = Sep, note = {29 pages}, year = {2006}, number = {cs.LO/0609008}, type = {Research report}, url = {http://arXiv.org/abs/cs.LO/0609008}, } @techreport{NowakDJJ:logrmt2, author = {Jean Goubault-Larrecq and Slawomir Lasota and David Nowak}, title = {Logical Relations for Monadic Types}, institution = {arXiv}, month = Nov, note = {Revised in March 2008. 83 pages}, year = {2005}, number = {cs.LO/0511006}, type = {Research report}, url = {http://arxiv.org/abs/cs/0511006}, } @techreport{NowakDJJ:reats, author = {Demri, St{\'e}phane and Nowak, David}, institution = {arXiv}, month = May, note = {Revised in August 2006. 38 pages}, number = {cs.LO/0505073}, type = {Research report}, title = {Reasoning about transfinite sequences}, year = {2005}, url = {http://arxiv.org/abs/cs.LO/0505073}, } @techreport{NowakDJJ:freqcl2, author ={Demri, St{\'e}phane and Lazi{\'c}, Ranko and Nowak, David}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan}, month = Apr, note = {13 pages}, number = {LSV-05-03}, type = {Research report}, title = {On the Freeze Quantifier in Constraint {LTL}: Decidability and Complexity}, year = {2005}, nmonth = {04}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf}, } @techreport{NowakDJJ:comllr2, author = {Jean Goubault-Larrecq and Slawomir Lasota and David Nowak and Yu Zhang}, title = {Complete lax logical relations for cryptographic lambda-calculi}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, {\'E}cole Normale Sup{\'e}rieure de Cachan}, month = Feb, note = {16 pages}, year = {2004}, number = {LSV-04-4}, type = {Research report}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2004-4.rr.ps}, } @techreport{NowakDJJ:edf12, author = {Bardin, S{\'e}bastien and Finkel, Alain and Nowak, David}, institution = {Contract P11L03/F01304/0 + 50.0241 between EDF and LSV}, month = Nov, note = {50 pages}, type = {Contract report}, title = {Rapport final}, year = {2003}, } @techreport{NowakDJJ:edf10, author = {Bardin, S{\'e}bastien and Finkel, Alain and Nowak, David}, institution = {Contract P11L03/F01304/0 + 50.0241 between EDF and LSV}, month = Aug, note = {21 pages}, type = {Contract report}, title = {Note de synth{\`e}se {\`a}~10~mois}, year = {2003}, } @techreport{NowakDJJ:edf6, author = {Bardin, S{\'e}bastien and Finkel, Alain and Nowak, David and Schnoebelen, {\relax Ph}ilippe}, institution = {Contract P11L03/F01304/0 + 50.0241 between EDF and LSV}, month = Jul, note = {43 pages}, type = {Contract report}, title = {Note de synth{\`e}se {\`a} 6 mois}, year = {2003}, } @techreport{NowakDJJ:semddi2, author = {Ranko Lazi{\'c} and David Nowak}, title = {On a Semantic Definition of Data Independence}, institution = {Department of Computer Science, University of Warwick}, month = Dec, note = {20 pages}, year = {2002}, number = {CS-RR-392}, type = {Research report}, url = {ftp://ftp.dcs.warwick.ac.uk/pub/reports/rr/392/all.ps.gz}, } @proceedings{NowakDJJ:avocs01, editor = {Nowak, David}, title = {Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS'01)}, institution = {Oxford University Computing Laboratory}, address = {Oxford, England, UK}, month = Apr, year = {2001}, series = {{P}rogramming {R}esearch {G}roup research reports}, number = {PRG-RR-01-07}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techreports/RR-01-07.ps.gz}, } @techreport{NowakDJJ:uniadi2, author = {Ranko Lazi{\'c} and David Nowak}, title = {A Unifying Approach to Data-independence}, institution = {Oxford University Computing Laboratory (OUCL)}, month = Jun, note = {30 pages}, year = {2000}, number = {PRG-TR-4-00}, url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techreports/TR-4-00.ps.gz} } @techreport{NowakDJJ:stebcp, author = {Micka{\"e}l Kerb{\oe}uf and David Nowak and Jean-Pierre Talpin}, title = {The Steam Boiler Controller Problem in {S}ignal-{C}oq}, institution = {{I}nstitut {N}ational de {R}echerche en {I}nformatique et {A}utomatique (INRIA)}, month = Oct, year = {1999}, number = {3773}, type = {Research report}, note = {59 pages}, url = {http://www.inria.fr/rrrt/rr-3773.html}, } @techreport{NowakDJJ:stebcp2, author = {Micka{\"e}l Kerb{\oe}uf and David Nowak and Jean-Pierre Talpin}, title = {The Steam Boiler Controller Problem in {S}ignal-{C}oq}, institution = {{I}nstitut de {R}echerche en {I}nformatique et {S}yst{\`e}mes {A}l{\'e}atoires (IRISA)}, month = Oct, year = {1999}, number = {1266}, type = {Internal Publication}, note = {59 pages}, url = {http://www.irisa.fr/centredoc/publis/PI/1999/irisapublication.2006-02-09.5861600982}, } @phdthesis{NowakDJJ:spepsr, author = {Nowak, David}, title = {Sp{\'e}cification et preuve de syst{\`e}mes r{\'e}actifs}, school = {Universit{\'e} de {R}ennes 1}, month = Oct, year = {1999}, note = {176 pages}, url = {ftp://ftp.irisa.fr/techreports/theses/1999/nowak.ps.gz}, } @techreport{NowakDJJ:semt, author = {David Nowak}, title = {The Semantics of {T}uplink}, institution = {IBM Japan Ltd., Tokyo Research Laboratory}, month = Sep, year = {1998}, type = {Research report}, number = {RT0292}, } @techreport{NowakDJJ:sysmas, author = {David Nowak and Jean-Pierre Talpin and Thierry Gautier}, title = {Un syst{\`e}me de modules avanc{\'e} pour {S}ignal}, institution = {{I}nstitut {N}ational de {R}echerche en {I}nformatique et {A}utomatique (INRIA)}, month = Jun, year = {1997}, number = {3176}, type = {Research report}, note = {34 pages}, url = {http://www.inria.fr/rrrt/rr-3176.html}, } @techreport{NowakDJJ:sysmas2, author = {David Nowak and Jean-Pierre Talpin and Thierry Gautier}, title = {Un syst{\`e}me de modules avanc{\'e} pour {S}ignal}, institution = {{I}nstitut de {R}echerche en {I}nformatique et {S}yst{\`e}mes {A}l{\'e}atoires (IRISA)}, month = Jun, year = {1997}, number = {1109}, type = {Internal Publication}, note = {34 pages}, url = {http://www.irisa.fr/centredoc/publis/PI/1997/irisapublication.2006-02-21.9179676863}, } @misc{NowakDJJ:beyo, title = {Beyond Omega}, author = {Nowak, David}, address = {Tokyo, Japan}, howpublished = {1st Workshop on Omega-Automata (OMEGA 2007)}, month = Oct, year = {2007}, url = {http://www.im.ntu.edu.tw/~omega2007/}, } @misc{NowakDJJ:logrmt3, title = {Logical Relations for Monadic Types}, author = {Nowak, David}, address = {Nanjing, China}, howpublished = {International Workshop on Formal Methods and Security ({IWFMS}'04)}, month = May, year = {2004}, url = {http://www.lsv.ens-cachan.fr/~zhang/workshop/}, }