Browse by Research Area

(2024) Multi-Stage Group Key Distribution and PAKEs: Securing Zoom Groups against Malicious Servers without New Security Elements. (Submitted)

(2024) Secure Messaging with Strong Compromise Resilience, Temporal Privacy, and Immediate Decryption. (Submitted)

(2024) Solving Infinite-State Games via Acceleration. (In Press)

(2023) Certifiers Make Neural Networks Vulnerable to Availability Attacks. (In Press)

(2023) Compositional High-Quality Synthesis. (In Press)

(2023) Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security. (Submitted)

(2023) Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations. (Submitted)

(2023) Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses.

(2023) Second-Order Hyperproperties.

(2023) nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models.

(2023) Hardware-Software Codesign for Mitigating Spectre.

(2023) Automata-Based Software Model Checking of Hyperproperties.

(2023) Counterfactuals Modulo Temporal Logics.

(2023) FIDO2, CTAP 2.1, and WebAuthn 2: Provable Security and Post-Quantum Instantiation. (In Press)

(2023) Iterative Circuit Repair Against Formal Specifications.

(2023) Taming Large Bounds in Synthesis from Bounded-Liveness Specifications. (In Press)

(2023) SEAL: Capability-Based Access Control for Data-Analytic Scenarios. (In Press)

(2023) Logics and Algorithms for Hyperproperties.

(2023) Formal Analysis of SPDM: Security Protocol and Data Model version 1.2.

(2022) Automated Program Repair Using Formal Verification Techniques.

(2022) Synthesizing Dominant Strategies for Liveness. (In Press)

(2022) Input Invariants.

(2022) Automatic Detection of Speculative Execution Combinations. (In Press)

(2022) Temporal Causality in Reactive Systems. (In Press)

(2022) Automatic Repair and Deadlock Detection for Parameterized Systems. (In Press)

(2022) Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties.

(2022) Real-time Visualization of Stream-based Monitoring Data. (In Press)

(2022) On the Adaptive Security of the Threshold BLS Signature Scheme. (In Press)

(2022) G-SINC: Global Synchronization Infrastructure for Network Clocks.

(2022) Subterm-based proof techniques for improving the automation and scope of security protocol analysis.

(2022) Metric Dimension Parameterized by Feedback Vertex Set and Other Structural Parameters.

(2022) Sample Compression Schemes for Balls in Graphs.

(2022) CHIP and CRISP: Protecting All Parties Against Compromise through Identity-Binding PAKEs.

(2022) Gossiping for Communication-Efficient Broadcast. (In Press)

(2022) (Nondeterministic) Hardness vs. Non-Malleability.

(2022) SAPIC+: protocol verifiers of the world, unite! (In Press)

(2022) ProxSkip: Yes! Local Gradient Steps Provably Lead to Communication Acceleration! Finally!

(2022) Specification decomposition for reactive synthesis.

(2022) Distributed edge coloring in time polylogarithmic in Δ. (Submitted)

(2022) Optimal Clock Synchronization with Signatures.

(2022) The landscape of distributed complexities on trees and beyond. (Submitted)

(2022) On a vertex-capturing game.

(2022) Axiomatic hardware-software contracts for security.

(2022) "Synthesizing Input Grammars": A Replication Study. (In Press)

(2022) Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?

(2022) Distributed ∆-Coloring Plays Hide-and-Seek. (Submitted)

(2022) The Largest Connected Subgraph Game.

(2022) Explaining Hyperproperty Violations. (Submitted)

(2022) BOCoSy: Small but Powerful Symbolic Output-Feedback Control.

(2022) A Recursive Early-Stopping Phase King Protocol. (Submitted)

(2022) Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols.

(2022) A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols.

(2022) Information Flow Guided Synthesis. (Unpublished)

(2022) Deciding Hyperproperties Combined with Functional Specifications. (In Press)

(2022) A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation.

(2022) Synthesis of Strategies for Autonomous Surveillance on Adversarial Targets.

(2022) Compositional synthesis of modular systems.

(2022) Live synthesis.

(2022) Temporal Stream Logic modulo Theories.

(2022) Masked Training of Neural Networks with Partial Gradients. (In Press)

(2022) From Input Coverage to Code Coverage: Systematically Covering Input Structure with k-Paths. (Submitted)

(2022) Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory.

(2022) Inferring Symbolic Automata.

(2022) Composing Secure Compilers.

(2022) Conformance Relations and Hyperproperties for Doping Detection in Time and Space.

(2022) Pareto-Optimal Defenses for the Web Infrastructure: Theory and Practice.

(2022) A Case Study in Information Flow Refinement for Low Level Systems.

(2021) Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity.

(2021) Formal Verification of Spectres Combination.

(2021) Algebraic Adversaries in the Universal Composability Framework.

(2021) Boosting the Security of Blind Signature Schemes.

(2021) Neural Circuit Synthesis from Specification Patterns.

(2021) Tardigrade: An Atomic Broadcast Protocol for Arbitrary Network Conditions.

(2021) Counting Homomorphisms to K4-minor-free Graphs, modulo 2.

(2021) Visual Analysis of Hyperproperties for Understanding Model Checking Results.

(2021) Compositional Synthesis of Modular Systems. (In Press)

(2021) Runtime Enforcement of Hyperproperties.

(2021) Live Synthesis.

(2021) Exorcising Spectres with secure compilers.

(2021) Monitoring with Verified Guarantees.

(2021) QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems. (In Press)

(2021) Reactive Synthesis Beyond Realizability (Invited Tutorial).

(2021) Robustness Certification for Point Cloud Models. (In Press)

(2021) Deep Learning for Temporal Logics. (Unpublished)

(2021) The Complexities of Healing in Secure Group Messaging: Why {Cross-Group} Effects Matter.

(2021) A Temporal Logic for Strategic Hyperproperties.

(2021) Künstliche Intelligenz in der Softwareentwicklung: Über die Schulter geschaut.

(2021) Causality-Based Game Solving.

(2021) A Temporal Logic for Asynchronous Hyperproperties.

(2021) AIGEN: Random Generation of Symbolic Transition Systems. (In Press)

(2021) Accountability in the Decentralised-Adversary Setting. (In Press)

(2021) CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle.

(2021) On the Soundness of Infrastructure Adversaries.

(2021) The Largest Connected Subgraph Game.

(2021) On Probabilistic Termination of Functional Programs with Continuous Distributions.

(2021) Verifying Accountability for Unbounded Sets of Participants.

(2021) Specification Decomposition for Reactive Synthesis. (In Press)

(2021) Robust Monitoring for Medical Cyber-Physical Systems.

(2021) BUFFing signature schemes beyond unforgeability and the case of post-quantum signatures. (In Press)

(2021) An Interactive Prover for Protocol Verification in the Computational Model.

(2021) The Provable Security of Ed25519: Theory and Practice. (In Press)

(2021) SoK: Computer-Aided Cryptography. (In Press)

(2021) Teaching Temporal Logics to Neural Networks.

(2021) RTLola on Board: Testing Real Driving Emissions on your Phone.

(2021) A Web Interface for Petri Nets with Transits and Petri Games.

(2021) Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade.

(2021) Model Checking Algorithms for Hyperproperties (Invited Paper).

(2020) Dependency-based Compositional Synthesis.

(2020) Model Checking Branching Properties on Petri Nets with Transits.

(2020) Probabilistic Hyperproperties of Markov Decision Processes.

(2020) Monitoring Cyber-Physical Systems: From Design to Integration.

(2020) Verified Rust Monitors for Lola Specifications.

(2020) Explainable Reactive Synthesis.

(2020) Modular Black-box Runtime Verification of Security Protocols.

(2020) Planning in the Browser.

(2020) A Formal Security Analysis of Key Establishment in the Signal Messaging Protocol. (In Press)

(2020) The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective.

(2020) Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS.

(2020) MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation.

(2020) Towards Post-Quantum Security for Signal's X3DH Handshake. (In Press)

(2020) Automatic Optimizations for Stream-based Monitoring Languages. (In Press)

(2020) A Formal Analysis of IEEE 802.11’s WPA2: Countering the Kracks Caused by Cracking the Counters.

(2020) Limiting the impact of unreliable randomness in deployed security protocols.

(2020) A Spectral Analysis of Noise:A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols.

(2020) Simulating Strong Practical Proof Systems with Extended Resolution.

(2020) Validation of Abstract Side-Channel Models for Computer Architectures.

(2020) Realizing Omega-regular Hyperproperties.

(2020) Clone Detection in Secure Messaging: Improving Post-Compromise Security in Practice. (In Press)

(2020) Parameterized Verification of Systems with Global Synchronization and Guards. (In Press)

(2020) Securing Asynchronous Exceptions.

(2020) Controller Synthesis for Hyperproperties.

(2020) Decentralized Privacy-Preserving Proximity Tracing.

(2020) From LTL to rLTL Monitoring: Improved Monitorability Through Robust Semantics.

(2020) Assume, Guarantee or Repair.

(2020) Simplex Architecture Meets RTLola.

(2020) Efficient monitoring of hyperproperties using prefix trees.

(2020) Novel Is Not Always Better:On the Relation between Novelty and Dominance Pruning.

(2020) Memory Safety Preservation for WebAssembly.

(2020) Promptness and Bounded Fairness in Concurrent and Parameterized Systems. (In Press)

(2020) How to Win First-Order Safety Games.

(2020) Universal Composability is Secure Compilation.

(2020) AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL.

(2020) RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft.

(2019) Parameterized synthesis of self-stabilizing protocols in symmetric networks.

(2019) Seems Legit: Automated Analysis of Subtle Attacks on Protocols that use Signatures. (In Press)

(2019) A symbolic algorithm for lazy synthesis of eager strategies.

(2019) Efficient Information-Flow Verification under Speculative Execution. (In Press)

(2019) FPGA Stream-Monitoring of Real-time Properties.

(2019) Highly Efficient Key Exchange Protocols with Optimal Tightness: Enabling real-world deployments with theoretically sound parameters. (In Press)

(2019) Translating Asynchronous Games for Distributed Synthesis.

(2019) Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman.

(2019) Improving Automated Symbolic Analysis of Ballot Secrecy for E-voting Protocols: A Method Based on Sufficient Conditions.

(2019) Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation.

(2019) Robustly Safe Compilation.

(2019) Real-time Stream Monitoring with StreamLAB.

(2019) Encoding Redundancy for Satisfaction-Driven Clause Learning.

(2019) Secure Authentication in the Grid: A Formal Analysis of DNP3 SAv5.

(2019) Strong Extension-Free Proof Systems.

(2019) Adversarial Initialization - when your network performs the way I want -.

(2019) Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion. (In Press)

(2019) Approximate Automata for Omega-Regular Languages.

(2019) Automated Verification of Accountability in Security Protocols. (In Press)

(2019) Bridging the Gap Between Abstractions and Critical-Path Heuristics via Hypergraphs.

(2019) Canonical Representations of k-Safety Hyperproperties.

(2019) Causality & Control flow. (In Press)

(2019) Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems.

(2019) The Hierarchy of Hyperlogics.

(2019) How to wrap it up - A formally verified proposal for the use of authenticated wrapping in PKCS#11. (In Press)

(2019) Membership Privacy for Fully Dynamic Group Signatures.

(2019) Model Checking Data Flows in Concurrent Network Updates.

(2019) Monitoring hyperproperties.

(2019) Program Repair for Hyperproperties.

(2019) QRAT Polynomially Simulates \forall-Exp+Res. (In Press)

(2019) StreamLAB: Stream-based Monitoring of Cyber-Physical Systems.

(2019) Synthesizing Approximate Implementations for Unrealizable Specifications.

(2019) Synthesizing functional reactive programs.

(2019) Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications.

(2019) Temporal Stream Logic: Synthesis beyond the Bools.

(2019) Truth Assignments as Conditional Autarkies.

(2019) Verifying Hyperliveness.

(2018) Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings.

(2018) A Symbolic Algorithm for Lazy Synthesis of Eager Strategies. (In Press)

(2018) Design Understanding: From Logic to Specification.

(2018) Distributed synthesis for parameterized temporal logics.

(2018) The Complexity of Monitoring Hyperproperties.

(2018) On Ends-to-Ends Encryption: Asynchronous Group Messaging with Strong Security Guarantees.

(2018) Killing Three Birds with one Gaussian Process: Analyzing Attack Vectors on Classification. (Submitted)

(2018) Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity.

(2018) Abstractions for security protocol verification. (In Press)

(2018) Bounded Synthesis of Reactive Programs.

(2018) Design, Analysis, and Implementation of ARPKI: An Attack-Resilient Public-Key Infrastructure.

(2018) MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \exists* \forall* Fragment.

(2018) Model Checking Quantitative Hyperproperties.

(2018) Model Checking Security Protocols.

(2018) RVHyper: A Runtime Verification Tool for Temporal Hyperproperties.

(2018) The Rise of the Citizen Developer: Assessing the Security Impact of Online App Generators.

(2018) Signatures with Flexible Public Key: Introducing Equivalence Classes for Public Keys. (In Press)

(2018) Synthesizing Reactive Systems from Hyperproperties.

(2018) When the Crypto in Cryptocurrencies Breaks: Bitcoin Security under Broken Primitives.

(2017) Parametricity Versus the Universal Type.

(2017) Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract).

(2017) A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange.

(2017) SilentWhispers: Enforcing Security and Privacy in Decentralized Credit Networks.

(2017) Relational cost analysis.

(2017) Security Analysis of Cache Replacement Policies.

(2017) Thread modularity at many levels: a pearl in compositional verification.

(2017) A promising semantics for relaxed-memory concurrency.

(2017) The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results.

(2017) ASICS: Authenticated Key Exchange Security Incorporating Certification Systems.

(2017) A Comprehensive Symbolic Analysis of TLS 1.3.

(2017) A Formal Security Analysis of the Signal Messaging Protocol.

(2017) Qapla: Policy compliance for database-backed systems.

(2017) Robust and compositional verification of object capability patterns.

(2017) Secure Authentication in the Grid: A Formal Analysis of DNP3: SAv5.

(2017) Symbolically Analyzing Security Protocols Using Tamarin.

(2017) The first reactive synthesis competition (SYNTCOMP 2014).

(2016) Automated analysis of security protocols with global state.

(2016) Simulating the Large-Scale Erosion of Genomic Privacy Over Time.

(2016) Light-Weight Contexts: An OS Abstraction for Safety and Performance.

(2016) Computational Soundness for Dalvik Bytecode.

(2016) Causally Consistent Dynamic Slicing.

(2016) T3: Comprehensive policy compliance in data retrieval systems.

(2016) Thoth: Comprehensive Policy Compliance in Data Retrieval Systems.

(2016) Micro-Policies for Web Session Security.

(2016) On Access Control, Capabilities, Their Equivalence, and Confused Deputy Attacks.

(2016) Progress-Sensitive Security for SPARK.

(2016) Asymmetric Secure Multi-execution with Declassification.

(2016) HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving.

(2016) Hitting Families of Schedules for Asynchronous Programs.

(2016) Lightweight verification of separate compilation.

(2016) MIRROR: symmetric timing analysis for real-time tasks on multicore platforms with shared resources.

(2016) Model Checking Population Protocols.

(2016) Partial Order Reduction for Event-Driven Multi-threaded Programs.

(2016) Probabilistic CTL*: The Deductive Way.

(2016) Runtime Verification for HyperLTL.

(2016) Safety Verification of Continuous-Space Pure Jump Markov Processes.

(2016) Security & Privacy Column.

(2016) Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents.

(2016) A Stream-Based Specification Language for Network Monitoring.

(2016) A Survey on Static Cache Analysis for Real-Time Systems.

(2016) Symbolic Model Checking for Factored Probabilistic Models.

(2016) System Architecture as an Ordinary Engineering Discipline.

(2016) Taming release-acquire consistency.

(2016) What You Really Need To Know About Your Neighbor.

(2016) A type theory for incremental computational complexity with control flow changes.

(2016) The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results.

(2016) Decidability in Parameterized Verification.

(2016) Distributed PROMPT-LTL Synthesis.

(2016) A High-Level LTL Synthesis Format: TLSF v1.1.

(2016) The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond.

(2016) Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems.

(2016) Tight Cutoffs for Guarded Protocols with Fairness.

(2015) Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits.

(2015) Affine Refinement Types for Secure Distributed Programming.

(2015) Information Flow Control for Event Handling and the DOM in Web Browsers.

(2015) A Logic of Programs with Interface-Confined Code.

(2015) Program Actions as Actual Causes: A Building Block for Accountability.

(2015) Guardat: enforcing data policies at the storage layer.

(2015) Refinement Types for Incremental Computational Complexity.

(2015) System M: A Program Logic for Code Sandboxing and Identification.

(2015) Privacy Preserving Payments in Credit Networks.

(2015) Achieving Optimal Utility for Distributed Differential Privacy Using SMPC.

(2015) Adam: Causality-Based Synthesis of Distributed Systems.

(2015) Algorithms for Model Checking HyperLTL and HyperCTL ^*.

(2015) Approximate Counting in SMT and Value Estimation for Probabilistic Programs.

(2015) Asynchronous Liquid Separation Types.

(2015) Bbs: A Phase-Bounded Model Checker for Asynchronous Programs.

(2015) CacheAudit: A Tool for the Static Analysis of Cache Side Channels.

(2015) Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).

(2015) Computational Soundness for Interactive Primitves.

(2015) Computing the Skorokhod distance between polygonal traces.

(2015) Dynamic scheduling for networked control systems.

(2015) Formal API Specification of the PikeOS Separation Kernel.

(2015) Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.

(2015) A Linear First-Order Functional Intermediate Language for Verified Compilers.

(2015) Model Checking Parameterized Asynchronous Shared-Memory Systems.

(2015) Modular Verification of Concurrency-Aware Linearizability.

(2015) Mtac: A monad for typed tactic programming in Coq.

(2015) Pilsner: a compositionally verified compiler for a higher-order imperative language.

(2015) Quantifying Conformance Using the Skorokhod Metric.

(2015) Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs.

(2015) Rely/Guarantee Reasoning for Asynchronous Programs.

(2015) Type-Based Verification of Electronic Voting Protocols.

(2015) Verifying read-copy-update in a logic for weak memory.

(2015) A formal C memory model supporting integer-pointer casts.

(2015) A generic and compositional framework for multicore response time analysis.

(2015) Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information.

(2015) Decidability of Parameterized Verification.

(2015) The Second Reactive Synthesis Competition (SYNTCOMP 2015).

(2014) TUC: Time-sensitive and Modular Analysis of Anonymous Communication.

(2014) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.

(2014) Architecture-parametric timing analysis.

(2014) Automatic Compositional Synthesis of Distributed Systems.

(2014) Automating the Choice of Consistency Levels in Replicated Systems.

(2014) Basic Problems in Multi-View Modeling.

(2014) Blocking Optimality in Distributed Real-Time Locking Protocols.

(2014) Bounds on mobility.

(2014) Building timing predictable embedded systems.

(2014) Causal Termination of Multi-threaded Programs.

(2014) A Compiler Optimization to Increase the Efficiency of WCET Analysis.

(2014) Computational Soundness Results for ProVerif - Bridging the Gap from Trace Properties to Uniformity.

(2014) Counting Models of Linear-Time Temporal Logic.

(2014) Cross-checking oracles from intrinsic software redundancy.

(2014) Deductive control synthesis for alternating-time logics.

(2014) Detecting Unrealizable Specifications of Distributed Systems.

(2014) Differentially Private Data Aggregation with Optimal Utility.

(2014) Dynamic package interfaces.

(2014) Edit Distance for Timed Automata.

(2014) F-ing modules.

(2014) Fast DQBF refutation.

(2014) Formal Specification of a Generic Separation Kernel.

(2014) GPS: navigating weak memory with ghosts, protocols, and separation.

(2014) Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis.

(2014) Information Flow Control in WebKit's JavaScript Bytecode.

(2014) Kuai: A model checker for software-defined networks.

(2014) Monitoring Parametric Temporal Logic.

(2014) Petri Games: Synthesis of Distributed Systems with Causal Memory.

(2014) A Pipelined Multi-core MIPS Machine -- Hardware Implementation and Correctness Proof.

(2014) Privacy-preserving Data Aggregation with Optimal Utility Using Arithmetic SMC -- Extended Abstract.

(2014) Privacy-preserving audit for broker-based health information exchange.

(2014) Race Detection for Android Applications.

(2014) Regression Test Selection for Distributed Software Histories.

(2014) Reverse engineering of cache replacement policies in Intel microprocessors and their evaluation.

(2014) An SMT-based Approach to Coverability Analysis.

(2014) Synthesis of Geometry Proof Problems.

(2014) Temporal Logics for Hyperproperties.

(2014) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.

(2014) Ubic: Bridging the Gap between Digital Cryptography and the Physical World.

(2014) Unary Pushdown Automata and Straight-Line Programs.

(2014) Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations.

(2014) Verification of Certifying Computations through AutoCorres and Simpl.

(2013) Relational Abstract Interpretation for the Verification of 2-Hypersafety Properties.

(2013) CacheAudit: A Tool for the Static Analysis of Cache Side Channels.

(2013) Differential Privacy by Typing in Security Protocols.

(2013) Security and Privacy by Declarative Design.

(2013) Computational Soundness of Symbolic Zero-Knowledge Proofs: Weaker Assumptions and Mechanized Verification.

(2013) Approximate Transient Analysis of Queuing Networks by Quasi Product Forms.

(2013) Automatic recovery from runtime failures.

(2013) Bisimilar finite abstractions of stochastic control systems.

(2013) Bounded synthesis.

(2013) Causality-Based Verification of Multi-threaded Programs.

(2013) CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.

(2013) Compositional Equivalence Checking for Models and Code of Control Systems.

(2013) Dependent Type Theory for Verification of Information Flow and Access Control Policies.

(2013) ESPOON$_ERBAC$: Enforcing Security Policies in Outsourced Environments.

(2013) Efficient partitioning of sporadic real-time tasks with shared resources and spin locks.

(2013) Every DFS Tree of a 3-Connected Graph Contains a Contractible Edge.

(2013) Expand, Enlarge, and Check for Branching Vector Addition Systems.

(2013) A Framework for the Verification of Certifying Computations.

(2013) A Fully Preemptive Multiprocessor Semaphore Protocol for Latency-Sensitive Real-Time Applications.

(2013) How to make ad hoc proof automation less ad hoc.

(2013) Improved analysis and evaluation of real-time semaphore protocols for P-FP scheduling.

(2013) Incremental Inductive Coverability.

(2013) Logical Foundations of Secure Resource Management.

(2013) Lossy Channel Games under Incomplete Information.

(2013) Measurement-based modeling of the cache replacement policy.

(2013) Model Checking Database Applications.

(2013) MrCrypt: Static Analysis for Secure Cloud Computations.

(2013) Mtac: a monad for typed tactic programming in Coq.

(2013) Multiprocessor Feasibility Analysis of Recurrent Task Systems with Specified Processor Affinities.

(2013) The OMLP family of optimal multiprocessor real-time locking protocols.

(2013) On Spin Locks in AUTOSAR: Blocking Analysis of FIFO, Unordered, and Priority-Ordered Spin Locks.

(2013) On-the-fly verification and optimization of DTA-properties for large Markov chains.

(2013) Parameterized verification of asynchronous shared-memory systems.

(2013) Precise timing analysis for direct-mapped caches.

(2013) A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism.

(2013) Relational abstract interpretation for the verification of 2-hypersafety properties.

(2013) Static Provenance Verification for Message Passing Programs.

(2013) Supervisor Synthesis for Controller Upgrades.

(2013) Synthesis of fixed-point programs.

(2013) Theory of Multi Core Hypervisor Verification.

(2013) A Theory of Name Boundedness.

(2013) A Theory of Partitioned Global Address Spaces.

(2013) A Uniformization Theorem for Nested Word to Word Transductions.

(2013) Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations.

(2012) Computational Soundness without Protocol Restrictions.

(2012) Verified Security of Merkle-Damgård.

(2012) Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction.

(2012) Automated Synthesis of Secure Distributed Applications.

(2012) Affine Refinement Types for Authentication and Authorization.

(2012) Algorithmic Verification of Asynchronous Programs.

(2012) Approximately Bisimilar Symbolic Models for Digital Control Systems.

(2012) Autonomous UAV.

(2012) CLSE: Closed-Loop Symbolic Execution.

(2012) Certifying 3-Connectivity in Linear Time.

(2012) Completing the Automated Verification of a Small Hypervisor - Assembler Code Verification.

(2012) The Complexity of Bounded Synthesis for Timed Control with Partial Observability.

(2012) Counterexample-Guided Synthesis of Observation Predicates.

(2012) Countermodels from Sequent Calculi in Multi-Modal Logics.

(2012) Detecting Deadlock in Programs with Data-Centric Synchronization. (Unpublished)

(2012) Efficient May Happen in Parallel Analysis for Async-finish Parallelism.

(2012) Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds.

(2012) An Empirical Evaluation of the Influence of the Load-Store Unit on WCET Analysis.

(2012) Enforceable Security Policies Revisited.

(2012) Engage: A Deployment Management System.

(2012) Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games.

(2012) Input-Output stability for discrete systems.

(2012) Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT.

(2012) Labeled Goal-Directed Search in Access Control Logic.

(2012) Language-Theoretic Abstraction Refinement.

(2012) Lazy Synthesis.

(2012) Merging the Cryptographic Security Analysis and the Algebraic-Logic Security Proof of PACE.

(2012) Model Checking Information Flow in Reactive Systems.

(2012) Model-based Monitoring for Sensitive SCADA Systems.

(2012) Monitoring Realizability.

(2012) Monitoring Temporal Information Flow.

(2012) An O(n+m) Certifying Triconnnectivity Algorithm for Hamiltonian Graphs.

(2012) On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols.

(2012) A Perfect Model for Bounded Verification.

(2012) SAFE Extensibility of Data-Driven Web Applications.

(2012) Scalable Testing of File System Checkers.

(2012) Stateful authorization logic - Proof theory and a case study.

(2012) Superficially substructural types.

(2012) Synthesis of minimal-error control software.

(2012) Template-Based Controller Synthesis for Timed Systems.

(2012) Three-valued abstraction for probabilistic systems.

(2012) Trigger memoization in self-triggered control.

(2012) Trusted Storage.

(2012) Verification of TLB Virtualization Implemented in C.

(2011) Policy auditing over incomplete logs: theory, implementation and applications.

(2011) Verification of Information Flow and Access Control Policies with Dependent Types.

(2011) A Security API for Distributed Social Networks.

(2011) Assumptions and Guarantees for Compositional Noninterference.

(2011) Automated proofs for Diffie-Hellman-based key exchanges.

(2011) Automatically Verifying Typing Constraints for a Data Processing Language.

(2011) Branch target buffers: WCET analysis framework and timing predictability.

(2011) Bug-Assist: Assisting Fault Localization in ANSI-C Programs.

(2011) CAMA: A Predictable Cache-Aware Memory Allocator.

(2011) Cause Clue Clauses: Error Localization Using Maximum Satisfiability.

(2011) Computational Soundness of Passively Secure Encryption in Presence of Active Adversaries.

(2011) Designing next-generation real-time streaming systems.

(2011) Does It Pay to Extend the Perimeter of a World Model?

(2011) Dynamic Enforcement of Knowledge-based Security Policies.

(2011) ESPOON: Enforcing Encrypted Security Policies in Outsourced Environments.

(2011) Efficient calculation of rare event probabilities in Markovian queueing networks.

(2011) A Formal Framework for Provenance Security.

(2011) Formal analysis of protocols based on TPM state registers.

(2011) Formalisms for Specifying Markovian Population Models.

(2011) G2C: Cryptographic Protocols from Goal-Driven Specifications.

(2011) Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.

(2011) HMC: Verifying Functional Programs Using Abstract Interpreters.

(2011) Integrated Specification and Verification of Security Protocols and Policies.

(2011) Low-Cost Byzantine Fault Tolerant Replication for a Cloud Environment.

(2011) A Lyapunov approach in incremental stability.

(2011) Minimum Attention Controller Synthesis for Omega-regular Objectives.

(2011) Non-Uniform Distributions in Quantitative Information-Flow.

(2011) On Adversary Models and Compositional Security.

(2011) PRET DRAM controller: bank privatization for predictability and temporal isolation.

(2011) Performance-aware Scheduler Synthesis for Control Systems.

(2011) Pessoa 2.0: A Controller Synthesis Tool for Cyber-physical Systems.

(2011) Reactive Safety.

(2011) Relaxed-memory concurrency and verified compilation.

(2011) Resource-aware Authorization Policies for Statically Typed Cryptographic Protocols.

(2011) Robust Discrete Synthesis Against Unspecified Disturbances.

(2011) SHAVE: stochastic hybrid analysis of markov population models.

(2011) Static analysis for efficient hybrid information-flow control.

(2011) Survey: Certifying Algorithms.

(2011) A Template for Predictability Definitions with Supporting Evidence.

(2011) Temporal isolation on multiprocessing architectures.

(2011) Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms.

(2011) Union and Intersection Types for Secure Protocol Implementations.

(2011) Verification of Certifying Computations.

(2011) Weak Kripke Structures and LTL.

(2010) Acoustic Side-Channel Attacks of Printers.

(2010) Experiences with PDG-based IFC.

(2010) A Type System for Data-Centric Synchronization.

(2009) Acoustic Side-Channel Attacks on Printers.

(2009) Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs.

(2009) Information Flow Control for Java - A Comprehensive Approach based on Path Conditions in Dependence Graphs.

(2009) Precise Slicing of Concurrent Programs -- An Evaluation of Precise Slicing Algorithms for Concurrent Programs.

(2008) Dynamic detection of atomic-set-serializability violations.

(2008) Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs. (Unpublished)

(2008) Precise Analysis of Java Programs using JOANA (Tool Demonstration).

(2008) Static path conditions for Java.

(2007) An Evaluation of Precise Slicing Algorithms for Concurrent Programs.

(2006) Dynamic path conditions in dependence graphs.

(2006) Information Flow Control for Java Based on Path Conditions in Dependence Graphs.

(2006) Intransitive Noninterference in Dependence Graphs.

(2004) An improved slicer for Java.