| Publication | Date of Publication | Type |
|---|
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
Formal Methods in System Design | 2025-01-13 | Paper |
A formalization of Heisenbugs and their causes
| 2024-06-05 | Paper |
Effective entailment checking for separation logic with inductive definitions
Tools and Algorithms for the Construction and Analysis of Systems | 2023-11-24 | Paper |
Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
Static Analysis | 2023-05-26 | Paper |
A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
ACM Transactions on Computational Logic | 2023-02-07 | Paper |
Type-based analysis of logarithmic amortised complexity
Mathematical Structures in Computer Science | 2023-02-06 | Paper |
Eliminating Message Counters in Threshold Automata
1517.68216 | 2022-12-22 | Paper |
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
| 2022-12-07 | Paper |
Verification of agent navigation in partially-known environments
Artificial Intelligence | 2022-06-01 | Paper |
ATLAS: automated amortised complexity analysis of self-adjusting data structures
| 2022-03-25 | Paper |
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
Formal Methods in System Design | 2021-12-08 | Paper |
Strong-separation logic
| 2021-10-18 | Paper |
Multi-linear strategy extraction for QBF expansion proofs via local soundness
| 2021-04-07 | Paper |
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
The polynomial complexity of vector addition systems with states
| 2020-09-23 | Paper |
From Shapes to Amortized Complexity
Lecture Notes in Computer Science | 2020-07-07 | Paper |
Parameterized model checking of synchronous distributed algorithms by abstraction
Lecture Notes in Computer Science | 2020-07-07 | Paper |
On the automated verification of web applications with embedded SQL
| 2018-07-18 | Paper |
Extending \(\mathcal{ALCQIO}\) with trees
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
Automata and program analysis
| 2017-11-22 | Paper |
Complexity and resource bound analysis of imperative programs using difference constraints
Journal of Automated Reasoning | 2017-08-15 | Paper |
Monadic second order finite satisfiability and unbounded tree-width
| 2017-07-19 | Paper |
Unified reasoning about robustness properties of symbolic-heap separation logic
Programming Languages and Systems | 2017-05-19 | Paper |
Empirical software metrics for benchmarking of verification tools
Formal Methods in System Design | 2017-05-15 | Paper |
On the Expressive Power of Communication Primitives in Parameterised Systems
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Liveness of parameterized timed networks
Automata, Languages, and Programming | 2015-11-04 | Paper |
Asymptotically precise ranking functions for deterministic size-change systems
Lecture Notes in Computer Science | 2015-10-20 | Paper |
Size-Change Abstraction and Max-Plus Automata
Mathematical Foundations of Computer Science 2014 | 2014-10-14 | Paper |
Ramsey versus lexicographic termination proving
Tools and Algorithms for the Construction and Analysis of Systems | 2013-08-05 | Paper |
An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries
Lecture Notes in Computer Science | 2009-02-10 | Paper |
