| Publication | Date of Publication | Type |
|---|
Semantic foundations for cost analysis of pipeline-optimized programs
Static Analysis | 2023-07-28 | Paper |
A Fast Verified Liveness Analysis in SSA Form
Automated Reasoning | 2022-11-09 | Paper |
| Verifying constant-time implementations by abstract interpretation | 2022-08-25 | Paper |
| A flow-insensitive-complete program representation | 2022-07-08 | Paper |
Verified functional programming of an abstract interpreter
(available as arXiv preprint) | 2022-06-17 | Paper |
System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
Journal of Automated Reasoning | 2021-02-17 | Paper |
Verifying a concurrent garbage collector with a rely-guarantee methodology
Journal of Automated Reasoning | 2019-08-21 | Paper |
| Verifying a concurrent garbage collector using a rely-guarantee methodology | 2018-01-04 | Paper |
An abstract memory functor for verified C static analyzers
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
Verified abstract interpretation techniques for disassembling low-level self-modifying code
Journal of Automated Reasoning | 2016-05-26 | Paper |
Validating dominator trees for a fast, verified dominance test
Interactive Theorem Proving | 2015-09-14 | Paper |
Plan B, a buffered memory model for Java
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
Verified abstract interpretation techniques for disassembling low-level self-modifying code
Interactive Theorem Proving | 2014-09-08 | Paper |
Building certified static analysers by modular construction of well-founded lattices
Electronic Notes in Theoretical Computer Science | 2014-05-13 | Paper |
A verified information-flow architecture
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
A certified lightweight non-interference Java bytecode verifier
Mathematical Structures in Computer Science | 2014-03-12 | Paper |
Secure the clones
Logical Methods in Computer Science | 2012-06-01 | Paper |
Modular SMT proofs for fast reflexive checking inside Coq
Certified Programs and Proofs | 2011-11-22 | Paper |
A certified denotational abstract interpreter
Interactive Theorem Proving | 2010-09-14 | Paper |
Embedding of Systems of Affine Recurrence Equations in Coq
Lecture Notes in Computer Science | 2010-05-07 | Paper |
A Certified Data Race Analysis for a Java-like Language
Lecture Notes in Computer Science | 2009-10-20 | Paper |
A Certified Lightweight Non-interference Java Bytecode Verifier
Programming Languages and Systems | 2007-09-04 | Paper |
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
Functional and Logic Programming | 2007-05-02 | Paper |
| scientific article; zbMATH DE number 1863395 (Why is no real title available?) | 2003-02-04 | Paper |
