David Nowak - RankMe

64 papers A 2B 9C 5Misc 3Journal 28Unranked 17

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