David Nowak

Publication Activity (10 Years)

Years Active: 1997-2024
Publications (10 Years): 19

Top Topics

Recursive Functions

Top Venues

J. Log. Algebraic Methods Program.

Electron. Commun. Eur. Assoc. Softw. Sci. Technol.

Publications

David Nowak, Bettina Distel
Trust in Times of Cyber Crisis: Understanding Organizational Trust Repair in the Public Sector. EGOV (2024)
Horatiu Cheval, David Nowak, Vlad Rusu
Formal definitions and proofs for partial (co)recursive functions. J. Log. Algebraic Methods Program. 141 (2024)
David Nowak, Vlad Rusu
While Loops in Coq. FROM (2023)
Florian Vanhems, Vlad Rusu, David Nowak, Gilles Grimaud
A Formal Correctness Proof for an EDF Scheduler Implementation. RTAS (2022)
Vlad Rusu, David Nowak
Defining Corecursive Functions in Coq Using Approximations (Artifact). Dagstuhl Artifacts Ser. 8 (2) (2022)
Vlad Rusu, David Nowak
Defining Corecursive Functions in Coq Using Approximations. ECOOP (2022)
Vlad Rusu, David Nowak
(Co)inductive proof systems for compositional proofs in reachability logic. J. Log. Algebraic Methods Program. 118 (2021)
Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
A trustful monad for axiomatic reasoning with probability and nondeterminism. J. Funct. Program. 31 (2021)
Reynald Affeldt, David Nowak
Extending Equational Monadic Reasoning with Monad Transformers. TYPES (2020)
Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism. CoRR (2020)
Reynald Affeldt, David Nowak
Extending Equational Monadic Reasoning with Monad Transformers. CoRR (2020)
Reynald Affeldt, David Nowak, Takafumi Saikawa
A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. MPC (2019)
Vlad Rusu, David Nowak
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic. FROM (2019)
Narjes Jomaa, Paolo Torrini, David Nowak, Gilles Grimaud, Samuel Hym
Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 76 (2018)
Paolo Torrini, David Nowak, Narjes Jomaa, Mohamed Sami Cherif
Formalising Executable Specifications of Low-Level Systems. VSTTE (2018)
Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak
Formal proof of polynomial-time complexity with quasi-interpretations. CPP (2018)
Narjes Jomaa, David Nowak, Gilles Grimaud, Samuel Hym
Formal proof of dynamic memory isolation based on MMU. Sci. Comput. Program. 162 (2018)
Andrei Arusoaie, David Nowak, Vlad Rusu, Dorel Lucanu
A Certified Procedure for RL Verification. SYNASC (2017)
Narjes Jomaa, David Nowak, Gilles Grimaud, Samuel Hym
Formal Proof of Dynamic Memory Isolation Based on MMU. TASE (2016)
David Nowak, Yu Zhang
Formal security proofs with minimal fuss: Implicit computational complexity at work. Inf. Comput. 241 (2015)
Dorel Lucanu, Vlad Rusu, Andrei Arusoaie, David Nowak
Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. Logic, Rewriting, and Concurrency (2015)
Pierre Castéran, Jacques Garrigue, David Nowak
Summer School on Coq (NII Shonan Meeting 2014-9). NII Shonan Meet. Rep. 2014 (2014)
Akitoshi Kawamura, Jean-Yves Marion, David Nowak
Implicit Computational Complexity and Applications: Resource Control, Security, Real-Number Computation (NII Shonan Meeting 2013-13). NII Shonan Meet. Rep. 2013 (2013)
Reynald Affeldt, David Nowak, Kiyoshi Yamada
Certifying assembly with formal security proofs: The case of BBS. Sci. Comput. Program. 77 (10-11) (2012)
Reynald Affeldt, David Nowak, Yutaka Oiwa
Formal network packet processing with minimal fuss: invertible syntax descriptions at work. PLPV (2012)
Sylvain Heraud, David Nowak
A Formalization of Polytime Functions. ITP (2011)
Satoshi Hirabayashi, Charles Kroll, David Nowak
Component-based development and sensitivity analyses of an air pollutant dry deposition model. Environ. Model. Softw. 26 (6) (2011)
Sylvain Heraud, David Nowak
A Formalization of Polytime Functions CoRR (2011)
David Nowak, Yu Zhang
A calculus for game-based security proofs. IACR Cryptol. ePrint Arch. 2010 (2010)
David Nowak, Yu Zhang
A Calculus for Game-Based Security Proofs. ProvSec (2010)
David Nowak
On formal verification of arithmetic-based cryptographic primitives CoRR (2009)
Reynald Affeldt, David Nowak, Kiyoshi Yamada
Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 23 (2009)
Reynald Affeldt, David Nowak, Kiyoshi Yamada
Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. IACR Cryptol. ePrint Arch. 2009 (2009)
Jean Goubault-Larrecq, Slawomir Lasota, David Nowak
Logical relations for monadic types. Math. Struct. Comput. Sci. 18 (6) (2008)
David Nowak
On Formal Verification of Arithmetic-Based Cryptographic Primitives. ICISC (2008)
David Nowak
A Framework for Game-Based Security Proofs. IACR Cryptol. ePrint Arch. 2007 (2007)
David Nowak
A Framework for Game-Based Security Proofs. ICICS (2007)
Stéphane Demri, Ranko Lazic, David Nowak
On the freeze quantifier in Constraint LTL: Decidability and complexity. Inf. Comput. 205 (1) (2007)
Stéphane Demri, David Nowak
Reasoning about Transfinite Sequences. Int. J. Found. Comput. Sci. 18 (1) (2007)
Slawomir Lasota, David Nowak, Yu Zhang
On Completeness of Logical Relations for Monadic Types CoRR (2006)
Slawomir Lasota, David Nowak, Yu Zhang
On Completeness of Logical Relations for Monadic Types. ASIAN (2006)
David Nowak
Synchronous structures. Inf. Comput. 204 (8) (2006)
Stéphane Demri, Ranko Lazic, David Nowak
On the freeze quantifier in Constraint LTL: decidability and complexity CoRR (2006)
Jean Goubault-Larrecq, Slawomir Lasota, David Nowak
Logical Relations for Monadic Types CoRR (2005)
Stéphane Demri, Ranko Lazic, David Nowak
On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. TIME (2005)
Stéphane Demri, David Nowak
Reasoning About Transfinite Sequences. ATVA (2005)
Stéphane Demri, David Nowak
Reasoning about transfinite sequences CoRR (2005)
Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, Yu Zhang
Complete Lax Logical Relations for Cryptographic Lambda-Calculi. CSL (2004)
Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin
Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures. ICFEM (2003)
Ranko Lazic, David Nowak
On a Semantic Definition of Data Independence . TLCA (2003)
Yu Zhang, David Nowak
Logical Relations for Dynamic Name Creation. CSL (2003)
Jean Goubault-Larrecq, Slawomir Lasota, David Nowak
Logical Relations for Monadic Types. CSL (2002)
Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin
Specification and Verification of a Steam-Boiler with Signal-Coq. TPHOLs (2000)
Dona Crawford, Donald McCoy, David Nowak
Our perspective on the Alliance Program's benefits. Comput. Sci. Eng. 2 (2) (2000)
Ranko Lazic, David Nowak
A Unifying Approach to Data-Independence. CONCUR (2000)
David Nowak, Jean-Pierre Talpin, Paul Le Guernic
Synchronous Structures. CONCUR (1999)
David Nowak, Jean-René Beauvais, Jean-Pierre Talpin
Co-inductive Axiomatization of a Synchronous Language. TPHOLs (1998)
Jean-Pierre Talpin, David Nowak
A Synchronous Semantics of Higher-Order Processes for Modeling Reconfigurable Reactive Systems. FSTTCS (1998)
David Nowak, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic
An ML-Like Module System for the Synchronous Language SIGNAL. Euro-Par (1997)