| Publication | Date of Publication | Type |
|---|
Stack-aware hyperproperties
| 2023-12-13 | Paper |
Model checking indistinguishability of randomized security protocols
Computer Aided Verification | 2023-05-05 | Paper |
Modular verification of protocol equivalence in the presence of randomness
| 2022-08-25 | Paper |
Modelchecking safety properties in randomized security protocols
| 2021-07-08 | Paper |
Verification methods for the computationally complete symbolic attacker based on indistinguishability
ACM Transactions on Computational Logic | 2019-11-22 | Paper |
Automated verification of equivalence properties of cryptographic protocols
ACM Transactions on Computational Logic | 2017-07-13 | Paper |
Computing Information Flow Using Symbolic Model-Checking
| 2017-04-25 | Paper |
The complexity of quantitative information flow in recursive programs
| 2017-01-26 | Paper |
A counterexample-guided abstraction-refinement framework for Markov decision processes
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Least upper bounds for probability measures and their applications to abstractions
Information and Computation | 2014-02-11 | Paper |
Reasoning about imperative quantum programs
| 2013-10-10 | Paper |
Extending classical logic for reasoning about quantum systems
| 2013-10-04 | Paper |
Reachability under contextual locking
Logical Methods in Computer Science | 2013-09-26 | Paper |
Probabilistic automata with isolated cut-points
Mathematical Foundations of Computer Science 2013 | 2013-09-20 | Paper |
Bounded context-switching and reentrant locking
Lecture Notes in Computer Science | 2013-03-18 | Paper |
Model checking concurrent programs with nondeterminism and randomization
| 2012-08-29 | Paper |
Reachability under contextual locking
Tools and Algorithms for the Construction and Analysis of Systems | 2012-06-29 | Paper |
Automated verification of equivalence properties of cryptographic protocols
Programming Languages and Systems | 2012-06-22 | Paper |
Power of randomization in automata on infinite strings
Logical Methods in Computer Science | 2012-04-02 | Paper |
Contract signing, optimism, and advantage.
Lecture Notes in Computer Science | 2010-03-30 | Paper |
Complexity bounds for the verification of real-time software
Lecture Notes in Computer Science | 2010-01-14 | Paper |
Deciding branching time properties for asynchronous programs
Theoretical Computer Science | 2009-10-09 | Paper |
Reasoning About States of Probabilistic Sequential Programs
Computer Science Logic | 2009-03-12 | Paper |
Least Upper Bounds for Probability Measures and Their Applications to Abstractions
CONCUR 2008 - Concurrency Theory | 2008-11-25 | Paper |
QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS
International Journal of Quantum Information | 2008-11-03 | Paper |
Decidability Results for Well-Structured Transition Systems with Auxiliary Storage
CONCUR 2007 – Concurrency Theory | 2008-09-18 | Paper |
Reasoning about probabilistic sequential programs
Theoretical Computer Science | 2007-07-16 | Paper |
Formal analysis of multiparty contract signing
Journal of Automated Reasoning | 2007-01-30 | Paper |
A Hybrid Intuitionistic Logic: Semantics and Decidability
Journal Of Logic And Computation | 2006-09-22 | Paper |
Contract signing, optimism, and advantage
The Journal of Logic and Algebraic Programming | 2005-08-01 | Paper |
