David Nowak

Proceedings of the Proceedings 7th Symposium on Working Formal Methods, 2023

2022

Defining Corecursive Functions in Coq Using Approximations (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2022

A Formal Correctness Proof for an EDF Scheduler Implementation.

[BibT_eX]

[DOI]

Proceedings of the 28th IEEE Real-Time and Embedded Technology and Applications Symposium, 2022

Defining Corecursive Functions in Coq Using Approximations.

[BibT_eX]

[DOI]

Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

2021

A trustful monad for axiomatic reasoning with probability and nondeterminism.

[BibT_eX]

[DOI]

J. Funct. Program., 2021

2020

Extending Equational Monadic Reasoning with Monad Transformers.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

2019

(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third Symposium on Working Formal Methods, 2019

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning.

[BibT_eX]

[DOI]

Takafumi Saikawa

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

2018

Formal proof of dynamic memory isolation based on MMU.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2018

Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base.

[BibT_eX]

[DOI]

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

Formalising Executable Specifications of Low-Level Systems.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Formal proof of polynomial-time complexity with quasi-interpretations.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

A Certified Procedure for RL Verification.

[BibT_eX]

[DOI]

Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

2015

Formal security proofs with minimal fuss: Implicit computational complexity at work.

[BibT_eX]

[DOI]

Inf. Comput., 2015

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications.

[BibT_eX]

[DOI]

Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014

Summer School on Coq (NII Shonan Meeting 2014-9).

[BibT_eX]

[DOI]

Pierre Castéran

Jacques Garrigue

NII Shonan Meet. Rep., 2014

2013

Implicit Computational Complexity and Applications: Resource Control, Security, Real-Number Computation (NII Shonan Meeting 2013-13).

[BibT_eX]

[DOI]

Akitoshi Kawamura

Jean-Yves Marion

NII Shonan Meet. Rep., 2013

2012

Certifying assembly with formal security proofs: The case of BBS.

[BibT_eX]

[DOI]

Kiyoshi Yamada

Sci. Comput. Program., 2012

Formal network packet processing with minimal fuss: invertible syntax descriptions at work.

[BibT_eX]

[DOI]

Yutaka Oiwa

Proceedings of the sixth workshop on Programming Languages meets Program Verification, 2012

2011

Component-based development and sensitivity analyses of an air pollutant dry deposition model.

[BibT_eX]

[DOI]

Satoshi Hirabayashi

Charles Kroll

Environ. Model. Softw., 2011

A Formalization of Polytime Functions.

[BibT_eX]

[DOI]

Sylvain Heraud

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

A calculus for game-based security proofs.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2010

2009

Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS.

[BibT_eX]

[DOI]

Kiyoshi Yamada

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

2008

Logical relations for monadic types.

[BibT_eX]

[DOI]

Jean Goubault-Larrecq

Slawomir Lasota

Math. Struct. Comput. Sci., 2008

On Formal Verification of Arithmetic-Based Cryptographic Primitives.

[BibT_eX]

[DOI]

Proceedings of the Information Security and Cryptology, 2008

2007

Reasoning about Transfinite Sequences.

[BibT_eX]

[DOI]

Stéphane Demri

Int. J. Found. Comput. Sci., 2007

On the freeze quantifier in Constraint LTL: Decidability and complexity.

[BibT_eX]

[DOI]

Stéphane Demri

Ranko Lazic

Inf. Comput., 2007

A Framework for Game-Based Security Proofs.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2007

2006

Synchronous structures.

[BibT_eX]

[DOI]

Inf. Comput., 2006

On Completeness of Logical Relations for Monadic Types.

[BibT_eX]

[DOI]

Slawomir Lasota

Proceedings of the Advances in Computer Science, 2006

2004

Complete Lax Logical Relations for Cryptographic Lambda-Calculi.

[BibT_eX]

[DOI]

Jean Goubault-Larrecq

Slawomir Lasota

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

On a Semantic Definition of Data Independence .

[BibT_eX]

[DOI]

Ranko Lazic

Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference, 2003

Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures.

[BibT_eX]

[DOI]

Mickaël Kerboeuf

Proceedings of the Formal Methods and Software Engineering, 2003

Logical Relations for Dynamic Name Creation.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 17th International Workshop, 2003

2000

Our perspective on the Alliance Program's benefits.

[BibT_eX]

[DOI]

Dona Crawford

Donald McCoy

Comput. Sci. Eng., 2000

Specification and Verification of a Steam-Boiler with Signal-Coq.

[BibT_eX]

[DOI]

Mickaël Kerboeuf

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

A Unifying Approach to Data-Independence.

[BibT_eX]

[DOI]

Ranko Lazic

Proceedings of the CONCUR 2000, 2000

1999

Synchronous Structures.

[BibT_eX]

[DOI]

Paul Le Guernic

Proceedings of the CONCUR '99: Concurrency Theory, 1999

1998

Co-inductive Axiomatization of a Synchronous Language.

[BibT_eX]

[DOI]

Jean-René Beauvais

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

A Synchronous Semantics of Higher-Order Processes for Modeling Reconfigurable Reactive Systems.

[BibT_eX]

[DOI]