| Publication | Date of Publication | Type |
|---|
Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
Journal of Automated Reasoning | 2024-09-27 | Paper |
| Refinement of parallel algorithms down to LLVM | 2024-07-15 | Paper |
| A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper) | 2024-04-26 | Paper |
| Bounded-Deducibility Security (Invited Paper) | 2023-06-20 | Paper |
| scientific article; zbMATH DE number 7649969 (Why is no real title available?) | 2023-02-03 | Paper |
| scientific article; zbMATH DE number 7649972 (Why is no real title available?) | 2023-02-03 | Paper |
| scientific article; zbMATH DE number 7649971 (Why is no real title available?) | 2023-02-03 | Paper |
Efficient Verified Implementation of Introsort and Pdqsort
Automated Reasoning | 2022-11-09 | Paper |
| For a few dollars more. Verified fine-grained algorithm analysis down to LLVM | 2021-10-18 | Paper |
| Iterable forward reachability analysis of monitor-DPNs | 2021-06-21 | Paper |
Iterable forward reachability analysis of monitor-DPNs
(available as arXiv preprint) | 2021-06-21 | Paper |
Efficient verified (UN)SAT certificate checking
Journal of Automated Reasoning | 2020-03-03 | Paper |
| Verified model checking of timed automata | 2019-09-16 | Paper |
Automatic refinement to efficient data structures: a comparison of two approaches
Journal of Automated Reasoning | 2019-05-31 | Paper |
Refinement to imperative HOL
Journal of Automated Reasoning | 2019-04-29 | Paper |
Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
Journal of Automated Reasoning | 2019-02-18 | Paper |
A verified SAT solver framework with learn, forget, restart, and incrementality
Journal of Automated Reasoning | 2018-08-21 | Paper |
Formal verification of an executable LTL model checker with partial order reduction
Journal of Automated Reasoning | 2018-02-02 | Paper |
Efficient verified (UN)SAT certificate checking
Automated Deduction – CADE 26 | 2017-09-22 | Paper |
Formalizing the Edmonds-Karp algorithm
Interactive Theorem Proving | 2016-10-27 | Paper |
Refinement to Imperative/HOL
Interactive Theorem Proving | 2015-09-14 | Paper |
Verified efficient implementation of Gabow's strongly connected component algorithm
Interactive Theorem Proving | 2014-09-08 | Paper |
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-04-10 | Paper |
Automatic Data Refinement
Interactive Theorem Proving | 2013-08-07 | Paper |
Applying data refinement for monadic programs to Hopcroft's algorithm
Interactive Theorem Proving | 2012-09-20 | Paper |
| scientific article; zbMATH DE number 5954655 (Why is no real title available?) | 2011-10-06 | Paper |
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
Lecture Notes in Computer Science | 2011-02-15 | Paper |
The Isabelle collections framework
Interactive Theorem Proving | 2010-09-14 | Paper |
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
Computer Aided Verification | 2009-06-30 | Paper |
Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures
CONCUR 2007 – Concurrency Theory | 2008-09-18 | Paper |
Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors
Static Analysis | 2008-08-28 | Paper |
