| Publication | Date of Publication | Type |
|---|
| Modeling a hardware synthesis methodology in Isabelle | 2024-07-05 | Paper |
| Practical relational calculus query evaluation | 2024-04-25 | Paper |
| Practical relational calculus query evaluation | 2024-04-23 | Paper |
Efficient Evaluation of Arbitrary Relational Calculus Queries
Logical Methods in Computer Science | 2024-01-16 | Paper |
Real-time policy enforcement with metric first-order temporal logic
Computer Security – ESORICS 2022 | 2023-07-28 | Paper |
VeriMon: a formally verified monitoring tool
Lecture Notes in Computer Science | 2023-07-28 | Paper |
Optimal proofs for linear temporal logic on lasso words
Automated Technology for Verification and Analysis | 2023-07-28 | Paper |
| Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete | 2023-04-28 | Paper |
Multi-head Monitoring of Metric Dynamic Logic
1517.6825 | 2022-12-22 | Paper |
| A formally verified, optimized monitor for metric first-order dynamic logic | 2022-11-09 | Paper |
Some normalization properties of Martin-Löf's type theory, and applications
Lecture Notes in Computer Science | 2022-08-16 | Paper |
| Cutoff bounds for consensus algorithms | 2022-08-12 | Paper |
Tests and refutation
Automated Technology for Verification and Analysis | 2022-08-12 | Paper |
| From Nondeterministic to Multi-Head Deterministic Finite-State Transducers | 2022-07-21 | Paper |
Runtime verification of temporal properties over out-of-order data streams
(available as arXiv preprint) | 2022-07-01 | Paper |
Timing-sensitive information flow analysis for synchronous systems
Computer Security – ESORICS 2006 | 2022-03-09 | Paper |
On obligations
Computer Security – ESORICS 2005 | 2022-03-09 | Paper |
Natural projection as partial model checking
Journal of Automated Reasoning | 2020-11-02 | Paper |
Almost event-rate independent monitoring of metric temporal logic
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Multi-head monitoring of metric temporal logic
Automated Technology for Verification and Analysis | 2020-07-20 | Paper |
Adaptive online first-order monitoring
Automated Technology for Verification and Analysis | 2020-07-20 | Paper |
CryptHOL: game-based proofs in higher-order logic
Journal of Cryptology | 2020-04-28 | Paper |
| Symbolic analysis of identity-based protocols | 2020-03-03 | Paper |
Termination orderings for rippling
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Almost event-rate independent monitoring
Formal Methods in System Design | 2019-11-25 | Paper |
Runtime Verification over Out-of-order Streams
ACM Transactions on Computational Logic | 2019-11-22 | Paper |
| From natural projection to partial model checking and back | 2019-09-16 | Paper |
Structuring metatheory on inductive definitions
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
Model Checking Security Protocols
Handbook of Model Checking | 2018-07-20 | Paper |
Algorithms for monitoring real-time properties
Acta Informatica | 2018-06-26 | Paper |
Anchored LTL separation
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | 2018-04-23 | Paper |
Scalable offline monitoring of temporal specifications
Formal Methods in System Design | 2018-02-12 | Paper |
| Failure-aware runtime verification of distributed systems | 2017-07-13 | Paper |
Reflective metalogical frameworks
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Monitoring metric first-order temporal properties
Journal of the ACM | 2016-03-24 | Paper |
Monitoring of temporal first-order properties with aggregations
Formal Methods in System Design | 2015-10-30 | Paper |
Automated complexity analysis based on ordered resolution
Journal of the ACM | 2015-09-20 | Paper |
Alice and Bob meet equational theories
Lecture Notes in Computer Science | 2015-09-14 | Paper |
Greedily computing associative aggregations on sliding windows
Information Processing Letters | 2014-12-09 | Paper |
Deciding safety and liveness in TPTL
Information Processing Letters | 2014-08-28 | Paper |
LTL is closed under topological closure
Information Processing Letters | 2014-04-30 | Paper |
| Multi-assignment clustering for Boolean data | 2014-04-01 | Paper |
| Deconstructing Alice and Bob | 2013-09-26 | Paper |
| Metareasoning about security protocols using distributed temporal logic | 2013-09-25 | Paper |
Towards an awareness-based semantics for security protocol analysis
Electronic Notes in Theoretical Computer Science | 2013-07-24 | Paper |
| Runtime monitoring of metric first-order temporal properties | 2012-10-19 | Paper |
Enforceable Security Policies Revisited
Lecture Notes in Computer Science | 2012-06-29 | Paper |
Provably repairing the ISO/IEC 9798 standard for entity authentication
Lecture Notes in Computer Science | 2012-06-29 | Paper |
| FAST: an efficient decision procedure for deduction and static equivalence | 2012-04-24 | Paper |
Model-Driven Development of Security-Aware GUIs for Data-Centric Applications
Foundations of Security Analysis and Design VI | 2011-09-16 | Paper |
Distributed temporal logic for the analysis of security protocol models
Theoretical Computer Science | 2011-07-18 | Paper |
Degrees of security: protocol guarantees in the face of compromising adversaries
Computer Science Logic | 2010-09-03 | Paper |
Labelled tableaux for distributed temporal logic
Journal Of Logic And Computation | 2010-01-14 | Paper |
Developing topology discovery in Event-B
Science of Computer Programming | 2009-12-11 | Paper |
Let’s Get Physical: Models and Methods for Real-World Security Protocols
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Midpoints Versus Endpoints: From Protocols to Firewalls
Applied Cryptography and Network Security | 2009-03-10 | Paper |
BAP: Broadcast Authentication Using Cryptographic Puzzles
Applied Cryptography and Network Security | 2009-03-10 | Paper |
Developing Topology Discovery in Event-B
Lecture Notes in Computer Science | 2009-02-24 | Paper |
A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Algebraic Intruder Deductions
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Verifying a signature architecture: a comparative case study
Formal Aspects of Computing | 2007-04-19 | Paper |
On the semantics of Alice \& Bob specifications of security protocols
Theoretical Computer Science | 2007-01-09 | Paper |
Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis
Logic Journal of the IGPL | 2006-03-30 | Paper |
FM 2005: Formal Methods
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Program Development in Computational Logic
Lecture Notes in Computer Science | 2005-12-23 | Paper |
| Rippling: Meta-Level Guidance for Mathematical Reasoning | 2005-07-28 | Paper |
| scientific article; zbMATH DE number 2102730 (Why is no real title available?) | 2004-09-24 | Paper |
| scientific article; zbMATH DE number 2090150 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2087621 (Why is no real title available?) | 2004-08-11 | Paper |
| scientific article; zbMATH DE number 2080191 (Why is no real title available?) | 2004-08-04 | Paper |
| scientific article; zbMATH DE number 2080008 (Why is no real title available?) | 2004-08-03 | Paper |
| scientific article; zbMATH DE number 1979551 (Why is no real title available?) | 2003-09-14 | Paper |
Bytecode verification by model checking
Journal of Automated Reasoning | 2003-09-09 | Paper |
Decision procedures for inductive Boolean functions based on alternating automata
Theoretical Computer Science | 2003-07-30 | Paper |
| scientific article; zbMATH DE number 1946752 (Why is no real title available?) | 2003-07-07 | Paper |
| scientific article; zbMATH DE number 1927414 (Why is no real title available?) | 2003-06-12 | Paper |
| scientific article; zbMATH DE number 1903364 (Why is no real title available?) | 2003-05-01 | Paper |
Current trends in logical frameworks and metalanguages
Journal of Automated Reasoning | 2003-02-16 | Paper |
Structuring metatheory on inductive definitions
Information and Computation | 2003-01-14 | Paper |
| Combining WS1S and HOL | 2002-07-22 | Paper |
| A recipe for the complexity analysis of non-classical logics | 2002-07-14 | Paper |
Program development schemata as derived rules
Journal of Symbolic Computation | 2002-02-27 | Paper |
| scientific article; zbMATH DE number 1670776 (Why is no real title available?) | 2001-11-11 | Paper |
| scientific article; zbMATH DE number 1670771 (Why is no real title available?) | 2001-11-11 | Paper |
A higher-order interpretation of deductive tableau
Journal of Symbolic Computation | 2001-07-22 | Paper |
| Maude versus Haskell: An experimental comparison in security protocol analysis | 2001-05-07 | Paper |
| scientific article; zbMATH DE number 1368960 (Why is no real title available?) | 2001-04-01 | Paper |
Natural deduction for non-classical logics
Studia Logica | 2001-02-14 | Paper |
| scientific article; zbMATH DE number 1523046 (Why is no real title available?) | 2000-10-30 | Paper |
Labelled modal logics: Quantifiers
Journal of Logic, Language and Information | 2000-03-29 | Paper |
| scientific article; zbMATH DE number 1354137 (Why is no real title available?) | 1999-10-31 | Paper |
| scientific article; zbMATH DE number 1348478 (Why is no real title available?) | 1999-10-10 | Paper |
| scientific article; zbMATH DE number 1331927 (Why is no real title available?) | 1999-09-02 | Paper |
| scientific article; zbMATH DE number 1231653 (Why is no real title available?) | 1999-01-07 | Paper |
| scientific article; zbMATH DE number 1223610 (Why is no real title available?) | 1998-11-15 | Paper |
Search in games with incomplete information: a case study using Bridge card play
Artificial Intelligence | 1998-08-13 | Paper |
| scientific article; zbMATH DE number 1140672 (Why is no real title available?) | 1998-04-13 | Paper |
Labelled propositional modal logics: theory and practice
Journal Of Logic And Computation | 1998-03-25 | Paper |
| scientific article; zbMATH DE number 1088193 (Why is no real title available?) | 1998-01-07 | Paper |
Adding metatheoretic facilities to first-order theories
Journal of Logic and Computation | 1997-08-03 | Paper |
A recursion planning analysis of inductive completion
Annals of Mathematics and Artificial Intelligence | 1997-05-12 | Paper |
Middle-out reasoning for synthesis and induction
Journal of Automated Reasoning | 1996-06-11 | Paper |
A calculus for and termination of rippling
Journal of Automated Reasoning | 1996-06-11 | Paper |
| scientific article; zbMATH DE number 827981 (Why is no real title available?) | 1996-05-27 | Paper |
A term equality problem equivalent to graph isomorphism
Information Processing Letters | 1994-09-05 | Paper |
| scientific article; zbMATH DE number 65529 (Why is no real title available?) | 1992-09-27 | Paper |
| scientific article; zbMATH DE number 4126684 (Why is no real title available?) | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 4101139 (Why is no real title available?) | 1989-01-01 | Paper |
| scientific article; zbMATH DE number 4074542 (Why is no real title available?) | 1988-01-01 | Paper |
