Number of items: 479.
Conference or Workshop Item (A Paper)
Cremers, Cas and Ronen, Eyal and Zhao, Mang
(2024)
Multi-Stage Group Key Distribution and PAKEs: Securing Zoom Groups against Malicious Servers without New Security Elements.
(Submitted)
Cremers, Cas and Zhao, Mang
(2024)
Secure Messaging with Strong Compromise Resilience, Temporal Privacy, and Immediate Decryption.
(Submitted)
Heim, Philippe and Dimitrova, Rayna
(2024)
Solving Infinite-State Games via Acceleration.
(In Press)
Lorenz, Tobias and Kwiatkowska, Marta and Fritz, Mario
(2023)
Certifiers Make Neural Networks Vulnerable to Availability Attacks.
(In Press)
Dewes, Rafael and Dimitrova, Rayna
(2023)
Compositional High-Quality Synthesis.
(In Press)
Cremers, Cas and Dax, Alexander and Jacomme, Charlie and Zhao, Mang
(2023)
Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security.
(Submitted)
Cremers, Cas and Jacomme, Charlie and Naska, Aurora
(2023)
Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations.
(Submitted)
Cheval, Vincent and Cremers, Cas and Dax, Alexander and Hirschi, Lucca and Jacomme, Charlie and Kremer, Steve
(2023)
Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses.
Beutner, Raven and Finkbeiner, Bernd and Frenkel, Hadar and Metzger, Niklas
(2023)
Second-Order Hyperproperties.
Cosler, Matthias and Hahn, Christopher and Mendoza, Daniel and Schmitt, Frederik and Trippel, Caroline
(2023)
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models.
Mosier, Nicholas and Eselius, Kate and Nemati, Hamed and Mitchell, John and Trippel, Caroline
(2023)
Hardware-Software Codesign for Mitigating Spectre.
Finkbeiner, Bernd and Frenkel, Hadar and Hofmann, Jana and Janine, Lohse
(2023)
Automata-Based Software Model Checking of Hyperproperties.
Finkbeiner, Bernd and Siber, Julian
(2023)
Counterfactuals Modulo Temporal Logics.
Bindel, Nina and Cremers, Cas and Zhao, Mang
(2023)
FIDO2, CTAP 2.1, and WebAuthn 2: Provable Security and Post-Quantum Instantiation.
(In Press)
Cosler, Matthias and Schmitt, Frederik and Hahn, Christopher and Finkbeiner, Bernd
(2023)
Iterative Circuit Repair Against Formal Specifications.
Heim, Philippe and Dimitrova, Rayna
(2023)
Taming Large Bounds in Synthesis from Bounded-Liveness Specifications.
(In Press)
Rasifard, Hamed and Gopinath, Rahul and Backes, Michael and Nemati, Hamed
(2023)
SEAL: Capability-Based Access Control for Data-Analytic Scenarios.
(In Press)
Cremers, Cas and Dax, Alexander and Naska, Aurora
(2023)
Formal Analysis of SPDM: Security Protocol and Data Model version 1.2.
Finkbeiner, Bernd and Passing, Noemi
(2022)
Synthesizing Dominant Strategies for Liveness.
(In Press)
Steinhöfel, Dominic and Zeller, Andreas
(2022)
Input Invariants.
Fabian, Xaver and Guarnieri, Marco and Patrignani, Marco
(2022)
Automatic Detection of Speculative Execution Combinations.
(In Press)
Coenen, Norine and Finkbeiner, Bernd and Frenkel, Hadar and Hahn, Christopher and Metzger, Niklas and Siber, Julian
(2022)
Temporal Causality in Reactive Systems.
(In Press)
Jacobs, Swen and Sakr, Mouhammad and Völp, Marcus
(2022)
Automatic Repair and Deadlock Detection for Parameterized Systems.
(In Press)
Baumeister, Jan and Finkbeiner, Bernd and Gumhold, Stefan and Schledjewski, Malte
(2022)
Real-time Visualization of Stream-based Monitoring Data.
(In Press)
Bacho, Renas and Loss, Julian
(2022)
On the Adaptive Security of the Threshold BLS Signature Scheme.
(In Press)
Frei, Marc and Kwon, Jonghoon and Seyedali, Tabaeiaghdaei and Wyss, Marc and Lenzen, Christoph and Perrig, Adrian
(2022)
G-SINC: Global Synchronization Infrastructure for Network Clocks.
Cremers, Cas and Jacomme, Charlie and Lukert, Philip
(2022)
Subterm-based proof techniques for improving the automation and scope of security protocol analysis.
Galby, Esther and Khazaliya, Liana and Mc Inerney, Fionn and Sharma, Roohani and Tale, Prafullkumar
(2022)
Metric Dimension Parameterized by Feedback Vertex Set and Other Structural Parameters.
Chalopin, Jérémie and Chepoi, Victor and Mc Inerney, Fionn and Ratel, Sébastien and Vaxès, Yann
(2022)
Sample Compression Schemes for Balls in Graphs.
Cremers, Cas and Naor, Moni and Paz, Shahar and Ronen, Eyal
(2022)
CHIP and CRISP: Protecting All Parties Against Compromise through Identity-Binding PAKEs.
Tsimos, Georgios and Loss, Julian and Papamanthou, Charalampos
(2022)
Gossiping for Communication-Efficient Broadcast.
(In Press)
Ball, Marshall and Dachman-Soled, Dana and Loss, Julian
(2022)
(Nondeterministic) Hardness vs. Non-Malleability.
Cheval, Vincent and Jacomme, Charlie and Kremer, Steve and Künnemann, Robert
(2022)
SAPIC+: protocol verifiers of the world, unite!
(In Press)
Mishchenko, Konstantin and Malinovsky, Grigory and Stich, Sebastian U. and Richtarik, Peter
(2022)
ProxSkip: Yes! Local Gradient Steps Provably Lead to Communication Acceleration! Finally!
Balliu, Alkida and Brandt, Sebastian and Kuhn, Fabian and Olivetti, Dennis
(2022)
Distributed edge coloring in time polylogarithmic in Δ.
(Submitted)
Lenzen, Christoph and Loss, Julian
(2022)
Optimal Clock Synchronization with Signatures.
Grunau, Christoph and Rozhoň, Václav and Brandt, Sebastian
(2022)
The landscape of distributed complexities on trees and beyond.
(Submitted)
Mosier, Nicholas and Lachnitt, Hanna and Nemati, Hamed and Trippel, Caroline
(2022)
Axiomatic hardware-software contracts for security.
Bendrissou, Bachir and Gopinath, Rahul and Zeller, Andreas
(2022)
"Synthesizing Input Grammars": A Replication Study.
(In Press)
Choi, Wonhyuk and Finkbeiner, Bernd and Piskac, Ruzica and Santolucito, Mark
(2022)
Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?
Balliu, Alkida and Brandt, Sebastian and Kuhn, Fabian and Olivetti, Dennis
(2022)
Distributed ∆-Coloring Plays Hide-and-Seek.
(Submitted)
Coenen, Norine and Dachselt, Raimund and Finkbeiner, Bernd and Frenkel, Hadar and Hahn, Christopher and Horak, Tom and Metzger, Niklas and Siber, Julian
(2022)
Explaining Hyperproperty Violations.
(Submitted)
Finkbeiner, Bernd and Mallik, Kaushik and Passing, Noemi and Schledjewski, Malte and Schmuck, Anne-Kathrin
(2022)
BOCoSy: Small but Powerful Symbolic Output-Feedback Control.
Lenzen, Christoph and Sheikholeslami, Sahar
(2022)
A Recursive Early-Stopping Phase King Protocol.
(Submitted)
Cremers, Cas and Fontaine, Caroline and Jacomme, Charlie
(2022)
A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols.
Finkbeiner, Bernd and Metzger, Niklas and Moses, Yoram
(2022)
Information Flow Guided Synthesis.
(Unpublished)
Beutner, Raven and Carral, David and Finkbeiner, Bernd and Hofmann, Jana and Krötzsch, Markus
(2022)
Deciding Hyperproperties Combined with Functional Specifications.
(In Press)
Finkbeiner, Bernd and Heim, Philippe and Passing, Noemi
(2022)
Temporal Stream Logic modulo Theories.
Mohtashami, Amirkeivan and Jaggi, Martin and Stich, Sebastian U.
(2022)
Masked Training of Neural Networks with Partial Gradients.
(In Press)
Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-Rüdiger
(2022)
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory.
Fisman, Dana and Frenkel, Hadar and Zilles, Sandra
(2022)
Inferring Symbolic Automata.
Kruse, Matthis and Patrignani, Marco
(2022)
Composing Secure Compilers.
Virtema, Jonni and Hofmann, Jana and Finkbeiner, Bernd and Kontinen, Juha and Yang, Fan
(2021)
Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity.
Fabian, Xaver and Chan, Koby and Patrignani, Marco
(2021)
Formal Verification of Spectres Combination.
Abdalla, Michel and Barbosa, Manuel and Katz, Jonathan and Loss, Julian and Xu, Jiayu
(2021)
Algebraic Adversaries in the Universal Composability Framework.
Katz, Jonathan and Loss, Julian and Rosenberg, Michael
(2021)
Boosting the Security of Blind Signature Schemes.
Schmitt, Frederik and Hahn, Christopher and Rabe, Markus N. and Finkbeiner, Bernd
(2021)
Neural Circuit Synthesis from Specification Patterns.
Blum, Erica and Katz, Jonathan and Loss, Julian
(2021)
Tardigrade: An Atomic Broadcast Protocol for Arbitrary Network Conditions.
Horak, Tom and Coenen, Norine and Metzger, Niklas and Hahn, Christopher and Flemisch, Tamara and Méndez, Julián and Dimov, Dennis and Finkbeiner, Bernd and Dachselt, Raimund
(2021)
Visual Analysis of Hyperproperties for Understanding Model Checking Results.
Finkbeiner, Bernd and Passing, Noemi
(2021)
Compositional Synthesis of Modular Systems.
(In Press)
Coenen, Norine and Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana and Schillo, Yannick
(2021)
Runtime Enforcement of Hyperproperties.
Finkbeiner, Bernd and Klein, Felix and Metzger, Niklas
(2021)
Live Synthesis.
Patrignani, Marco and Guarnieri, Marco
(2021)
Exorcising Spectres with secure compilers.
Dauer, Johann C. and Finkbeiner, Bernd and Schirmer, Sebastian
(2021)
Monitoring with Verified Guarantees.
Jaber, Nouraldin and Wagner, Christopher and Jacobs, Swen and Kulkarni, Milind and Samanta, Roopsha
(2021)
QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems.
(In Press)
Lorenz, Tobias and Ruoss, Anian and Balunović, Mislav and Singh, Gagandeep and Vechev, Martin
(2021)
Robustness Certification for Point Cloud Models.
(In Press)
Cremers, Cas and Hale, Britta and Kohbrok, Konrad
(2021)
The Complexities of Healing in Secure Group Messaging: Why {Cross-Group} Effects Matter.
Beutner, Raven and Finkbeiner, Bernd
(2021)
A Temporal Logic for Strategic Hyperproperties.
Baier, Christel and Coenen, Norine and Finkbeiner, Bernd and Funke, Florian and Jantsch, Simon and Siber, Julian
(2021)
Causality-Based Game Solving.
Baumeister, Jan and Coenen, Norine and Bonakdarpour, Borzoo and Finkbeiner, Bernd and Sánchez, César
(2021)
A Temporal Logic for Asynchronous Hyperproperties.
Jacobs, Swen and Sakr, Mouhammad
(2021)
AIGEN: Random Generation of Symbolic Transition Systems.
(In Press)
Künnemann, Robert and Garg, Deepak and Backes, Michael
(2021)
Accountability in the Decentralised-Adversary Setting.
(In Press)
El-Korashy, Akram and Tsampas, Stelios and Patrignani, Marco and Devriese, Dominique and Garg, Deepak and Piessens, Frank
(2021)
CapablePtrs: Securely Compiling Partial Programs
Using the Pointers-as-Capabilities Principle.
Dax, Alexander and Künnemann, Robert
(2021)
On the Soundness of Infrastructure Adversaries.
Bensmail, Julien and Fioravantes, Foivos and Mc Inerney, Fionn and Nisse, Nicolas
(2021)
The Largest Connected Subgraph Game.
Beutner, Raven and Ong, Luke
(2021)
On Probabilistic Termination of Functional Programs
with Continuous Distributions.
Morio, Kevin and Künnemann, Robert
(2021)
Verifying Accountability for Unbounded Sets of Participants.
Finkbeiner, Bernd and Geier, Gideon and Passing, Noemi
(2021)
Specification Decomposition for Reactive Synthesis.
(In Press)
Finkbeiner, Bernd and Keller, Andreas and Schmidt, Jessica and Schwenger, Maximilian
(2021)
Robust Monitoring for Medical Cyber-Physical Systems.
Cremers, Cas and Düzlü, Samed and Fiedler, Rune and Fischlin, Marc and Janson, Christian
(2021)
BUFFing signature schemes beyond unforgeability and the case of post-quantum signatures.
(In Press)
Baelde, David and Delaune, Stephanie and Jacomme, Charlie and Koutsos, Adrien and Moreau, Solene
(2021)
An Interactive Prover for Protocol Verification in the Computational Model.
Brendel, Jacqueline and Cremers, Cas and Jackson, Dennis and Zhao, Mang
(2021)
The Provable Security of Ed25519: Theory and Practice.
(In Press)
Barbosa, Manuel and Barthe, Gilles and Bhargavan, Karthik and Blanchet, Bruno and Cremers, Cas and Liao, Kevin and Parno, Brian
(2021)
SoK: Computer-Aided Cryptography.
(In Press)
Hahn, Christopher and Schmitt, Frederik and Kreber, Jens U. and Rabe, Markus Norman and Finkbeiner, Bernd
(2021)
Teaching Temporal Logics to Neural Networks.
Biewer, Sebastian and Finkbeiner, Bernd and Hermanns, Holger and Köhl, Maximilian A. and Schnitzer, Yannik and Schwenger, Maximilian
(2021)
RTLola on Board: Testing Real Driving Emissions on your Phone.
Gieseking, Manuel and Hecking-Harbusch, Jesko and Yanich, Ann
(2021)
A Web Interface for Petri Nets with Transits and Petri Games.
Vassena, Marco and Disselkoen, Craig and Cauligi, Sunjay and Gleissenthall, Klaus and Kici, Rami Gökhan and Jhala, Ranjit and Stefan, Deian and Tullsen, Dean
(2021)
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade.
Finkbeiner, Bernd
(2021)
Model Checking Algorithms for Hyperproperties (Invited Paper).
Finkbeiner, Bernd and Passing, Noemi
(2020)
Dependency-based Compositional Synthesis.
Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-Rüdiger
(2020)
Model Checking Branching Properties on Petri Nets with Transits.
Dimitrova, Rayna and Finkbeiner, Bernd and Torfah, Hazem
(2020)
Probabilistic Hyperproperties of Markov Decision Processes.
Schwenger, Maximilian
(2020)
Monitoring Cyber-Physical Systems: From Design to Integration.
Finkbeiner, Bernd and Oswald, Stefan and Passing, Noemi and Schwenger, Maximilian
(2020)
Verified Rust Monitors for Lola Specifications.
Baumeister, Tom and Finkbeiner, Bernd and Torfah, Hazem
(2020)
Explainable Reactive Synthesis.
Morio, Kevin and Jackson, Dennis and Vassena, Marco and Künnemann, Robert
(2020)
Modular Black-box Runtime Verification of Security Protocols.
Tran, Nicolas and Speicher, Patrick and Künnemann, Robert and Backes, Michael and Torralba, Àlvaro and Hoffmann, Jörg
(2020)
Planning in the Browser.
Künnemann, Robert and Nemati, Hamed
(2020)
MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation.
Brendel, Jacqueline and Fischlin, Marc and Günther, Felix and Janson, Christian and Stebila, Douglas
(2020)
Towards Post-Quantum Security for Signal's X3DH Handshake.
(In Press)
Baumeister, Jan and Finkbeiner, Bernd and Kruse, Matthis and Schwenger, Maximilian
(2020)
Automatic Optimizations for Stream-based Monitoring Languages.
(In Press)
Cremers, Cas and Kiesl, Benjamin and Medinger, Niklas
(2020)
A Formal Analysis of IEEE 802.11’s WPA2: Countering the Kracks Caused by Cracking the Counters.
Akhmetzyanova, Liliya and Cremers, Cas and Garratt, Luke and Smyshlyaev, Stanislav and Sullivan, Nick
(2020)
Limiting the impact of unreliable randomness in deployed security protocols.
Girol, Guillaume and Hirschi, Lucca and Sasse, Ralf and Jackson, Dennis and Cremers, Cas and Basin, David
(2020)
A Spectral Analysis of Noise:A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols.
Nemati, Hamed and Buiras, Pablo and Lindner, Andreas and Guanciale, Roberto and Jacobs, Swen
(2020)
Validation of Abstract Side-Channel Models for Computer Architectures.
Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana and Tentrup, Leander
(2020)
Realizing Omega-regular Hyperproperties.
Cremers, Cas and Fairoze, Jaiden and Kiesl, Benjamin and Naska, Aurora
(2020)
Clone Detection in Secure Messaging: Improving Post-Compromise Security in Practice.
(In Press)
Jaber, Nouraldin and Jacobs, Swen and Wagner, Christopher and Kulkarni, Milind and Samanta, Roopsha
(2020)
Parameterized Verification of Systems with Global Synchronization and Guards.
(In Press)
Cortiñas, Carlos Tomé and Vassena, Marco and Russo, Alejandro
(2020)
Securing Asynchronous Exceptions.
Bonakdarpour, B. and Finkbeiner, B.
(2020)
Controller Synthesis for Hyperproperties.
Mascle, Corto and Neider, Daniel and Schwenger, Maximilian and Tabuada, Paulo and Weinert, Alexander and Zimmermann, Martin
(2020)
From LTL to rLTL Monitoring: Improved Monitorability Through Robust Semantics.
Frenkel, Hadar and Grumberg, Orna and Pasareanu, Corina and Sheinvald, Sarai
(2020)
Assume, Guarantee or Repair.
Finkbeiner, Bernd and Schmidt, Jessica and Schwenger, Maximilian
(2020)
Simplex Architecture Meets RTLola.
Groß, Joschka and Torralba, Àlvaro and Fickert, Maximilian
(2020)
Novel Is Not Always Better:On the Relation between Novelty and Dominance Pruning.
Jacobs, Swen and Sakr, Mouhammad and Zimmermann, Martin
(2020)
Promptness and Bounded Fairness in
Concurrent and Parameterized Systems.
(In Press)
Seidl, Helmut and Müller, Christian and Finkbeiner, Bernd
(2020)
How to Win First-Order Safety Games.
Patrignani, Marco and Wahby, Riad S. and Künnemann, Robert
(2020)
Universal Composability is Secure Compilation.
Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-Rüdiger
(2020)
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL.
Baumeister, Jan and Finkbeiner, Bernd and Schirmer, Sebastian and Schwenger, Maximilian and Torens, Christoph
(2020)
RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft.
Jackson, Dennis and Cremers, Cas and Cohn-Gordon, Katriel and Sasse, Ralf
(2019)
Seems Legit: Automated Analysis of Subtle Attacks on Protocols that use Signatures.
(In Press)
Bloem, Roderick and Jacobs, Swen and Vizel, Yakir
(2019)
Efficient Information-Flow Verification under Speculative Execution.
(In Press)
Cohn-Gordon, Katriel and Cremers, Cas and Gjøsteen, Kristian and Jacobsen, Hakon and Jager, Tibor
(2019)
Highly Efficient Key Exchange Protocols with Optimal Tightness: Enabling real-world deployments with theoretically sound parameters.
(In Press)
Beutner, Raven and Finkbeiner, Bernd and Hecking-Harbusch, Jesko
(2019)
Translating Asynchronous Games for Distributed
Synthesis.
Cremers, Cas and Jackson, Dennis
(2019)
Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman.
Cremers, Cas and Hirschi, Lucca
(2019)
Improving Automated Symbolic Analysis of Ballot Secrecy for E-voting Protocols: A Method Based on Sufficient Conditions.
Abate, Carmine and Blanco, Roberto and Garg, Deepak and Hritcu, Catalin and Patrignani, Marco and Thibault, Jeremy
(2019)
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation.
Patrignani, Marco and Garg, Deepak
(2019)
Robustly Safe Compilation.
Faymonville, Peter and Finkbeiner, Bernd and Schledjewski, Malte and Schwenger, Maximilian and Tentrup, Leander and Torfah, Hazem
(2019)
Real-time Stream Monitoring with StreamLAB.
Heule, Marijn J.H. and Kiesl, Benjamin and Biere, Armin
(2019)
Encoding Redundancy for Satisfaction-Driven Clause Learning.
Cremers, Cas and Dehnel-Wild, Martin
(2019)
Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion.
(In Press)
Dimitrova, Rayna and Finkbeiner, Bernd and Torfah, Hazem
(2019)
Approximate Automata for Omega-Regular Languages.
Künnemann, Robert and Esiyok, Ilkan and Backes, Michael
(2019)
Automated Verification of Accountability in Security Protocols.
(In Press)
Steinmetz, Marcel and Torralba, Àlvaro
(2019)
Bridging the Gap Between Abstractions and Critical-Path Heuristics via Hypergraphs.
Finkbeiner, Bernd and Haas, Lennart and Torfah, Hazem
(2019)
Canonical Representations of k-Safety Hyperproperties.
Künnemann, Robert and Garg, Deepak and Backes, Michael
(2019)
Causality & Control flow.
(In Press)
Hecking-Harbusch, Jesko and Metzger, Niklas
(2019)
Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems.
Coenen, Norine and Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana
(2019)
The Hierarchy of Hyperlogics.
Dax, Alexander and Tangermann, Sven and Künnemann, Robert and Backes, Michael
(2019)
How to wrap it up - A formally verified proposal for the use of authenticated wrapping in PKCS#11.
(In Press)
Backes, Michael and Hanzlik, Lucjan and Schneider-Bensch, Jonas
(2019)
Membership Privacy for Fully Dynamic Group Signatures.
Finkbeiner, Bernd and Gieseking, Manuel and Olderog, Ernst-Rüdiger and Hecking-Harbusch, Jesko
(2019)
Model Checking Data Flows in Concurrent Network Updates.
Bonakdarpour, Borzoo and Finkbeiner, Bernd
(2019)
Program Repair for Hyperproperties.
Kiesl, Benjamin and Seidl, Martina
(2019)
QRAT Polynomially Simulates \forall-Exp+Res.
(In Press)
Faymonville, Peter and Finkbeiner, Bernd and Schledjewski, Malte and Schwenger, Maximilian and Stenger, Marvin and Tentrup, Leander and Torfah, Hazem
(2019)
StreamLAB: Stream-based Monitoring of Cyber-Physical Systems.
Dimitrova, Rayna and Finkbeiner, Bernd and Torfah, Hazem
(2019)
Synthesizing Approximate Implementations for Unrealizable Specifications.
Finkbeiner, Bernd and Klein, Felix and Piskac, Ruzica and Santolucito, Mark
(2019)
Synthesizing functional reactive programs.
Geier, Gideon and Heim, Philippe and Klein, Felix and Finkbeiner, Bernd
(2019)
Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications.
Finkbeiner, Bernd and Klein, Felix and Piskac, Ruzica and Santolucito, Mark
(2019)
Temporal Stream Logic: Synthesis beyond the Bools.
Kiesl, Benjamin and Heule, Marijn J.H. and Biere, Armin
(2019)
Truth Assignments as Conditional Autarkies.
Coenen, Norine and Finkbeiner, Bernd and Sanchez, Cesar and Tentrup, Leander
(2019)
Verifying Hyperliveness.
Mirzaie, Nahal and Faghih, Fathiyeh and Jacobs, Swen and Bonakdarpour, Borzoo
(2018)
Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings.
Jacobs, Swen and Sakr, Mouhammad
(2018)
A Symbolic Algorithm for Lazy Synthesis of Eager Strategies.
(In Press)
Fey, G\"rschwin and Ghasempouri, Tara and Jacobs, Swen and Martino, Gianluca and Raik, Jaan and Riener, Heinz
(2018)
Design Understanding: From Logic to Specification.
Bonakdarpour, B. and Finkbeiner, Bernd
(2018)
The Complexity of Monitoring Hyperproperties.
Cohn-Gordon, Katriel and Cremers, Cas and Garratt, Luke and Millican, Jon and Milner, Kevin
(2018)
On Ends-to-Ends Encryption: Asynchronous Group Messaging with Strong Security Guarantees.
Jacobs, Swen and Sakr, Mouhammad
(2018)
Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity.
Gerstacker, Carsten and Klein, Felix and Finkbeiner, Bernd
(2018)
Bounded Synthesis of Reactive Programs.
Finkbeiner, Bernd and Hahn, Christopher and Hans, Tobias
(2018)
MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \exists* \forall* Fragment.
Finkbeiner, Bernd and Hahn, Christopher and Torfah, Hazem
(2018)
Model Checking Quantitative Hyperproperties.
Finkbeiner, Bernd and Hahn, Christopher and Stenger, Marvin and Tentrup, Leander
(2018)
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties.
Oltrogge, Marten and Derr, Erik and Stransky, Christian and Acar, Yasemin and Fahl, Sascha and Rossow, Christian and Pellegrino, Giancarlo and Bugiel, Sven and Backes, Michael
(2018)
The Rise of the Citizen Developer: Assessing the Security Impact of Online App Generators.
Backes, Michael and Hanzlik, Lucjan and Kluczniak, Kamil and Schneider, Jonas
(2018)
Signatures with Flexible Public Key: Introducing Equivalence Classes for Public Keys.
(In Press)
Finkbeiner, Bernd and Hahn, Christopher and Lukert, Philip and Stenger, Marvin and Tentrup, Leander
(2018)
Synthesizing Reactive Systems from Hyperproperties.
Devriese, Dominique and Patrignani, Marco and Piessens, Frank
(2017)
Parametricity Versus the Universal Type.
Garg, Deepak and Hriţcu, Cătălin and Patrignani, Marco and Stronati, Marco and Swasey, David
(2017)
Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract).
Backes, Michael and Dreier, Jannik and Kremer, Steve and Künnemann, Robert
(2017)
A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange.
Malavolta, Giulio and Moreno-Sanchez, Pedro and Kate, Aniket and Maffei, Matteo
(2017)
SilentWhispers: Enforcing Security and Privacy in Decentralized Credit Networks.
Çiçek, Ezgi and Barthe, Gilles and Gaboardi, Marco and Garg, Deepak and Hoffmann, Jan
(2017)
Relational cost analysis.
Canones, Pablo and Köpf, Boris and Reineke, Jan
(2017)
Security Analysis of Cache Replacement Policies.
Hoenicke, Jochen and Majumdar, Rupak and Podelski, Andreas
(2017)
Thread modularity at many levels: a pearl in compositional verification.
Kang, Jeehoon and Hur, Chung-Kil and Lahav, Ori and Vafeiadis, Viktor and Dreyer, Derek
(2017)
A promising semantics for relaxed-memory concurrency.
Jacobs, Swen and Basset, Nicolas and Bloem, Roderick and Brenguier, Romain and Colange, Maximilien and Faymonville, Peter and Finkbeiner, Bernd and Khalimov, Ayrat and Klein, Felix and Michaud, Thibaud and Perez, Guillermo A. and Raskin, Jean-Francois and Sankur, Ocan and Tentrup, Leander
(2017)
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results.
Cohn-Gordon, Katriel and Cremers, Cas and Dowling, Benjamin and Stebila, Douglas
(2017)
A Formal Security Analysis of the Signal Messaging Protocol.
Mehta, Aastha and Elnikety, Eslam and Harvey, Katura and Garg, Deepak and Druschel, Peter
(2017)
Qapla: Policy compliance for database-backed systems.
Cremers, Cas and Dehnel-Wild, Martin and Milner, Kevin
(2017)
Secure Authentication in the Grid:
A Formal Analysis of DNP3: SAv5.
Backes, Michael and Berrang, Pascal and Humbert, Mathias and Shen, Xiaoyu and Wolf, Verena
(2016)
Simulating the Large-Scale Erosion of Genomic Privacy Over Time.
Vahldiek-Oberwanger, Anjo and Bhattacharjee, Bobby and Garg, Deepak and Elnikety, Eslam and Druschel, Peter and Litton, James
(2016)
Light-Weight Contexts: An OS Abstraction for Safety and Performance.
Backes, Michael and Künnemann, Robert and Mohammadi, Esfandiar
(2016)
Computational Soundness for Dalvik Bytecode.
Garg, Deepak and Cheney, James and Perera, Roly
(2016)
Causally Consistent Dynamic Slicing.
Elnikety, Eslam and Mehta, Aastha and Vahldiek-Oberwanger, Anjo and Garg, Deepak and Druschel, Peter
(2016)
T3: Comprehensive policy compliance in data retrieval systems.
Elnikety, Eslam and Mehta, Aastha and Vahldiek-Oberwanger, Anjo and Garg, Deepak and Druschel, Peter
(2016)
Thoth: Comprehensive Policy Compliance in Data Retrieval Systems.
Maffei, Matteo and Grimm, Niklas and Focardi, Riccardo and Calzavara, Stefano
(2016)
Micro-Policies for Web Session Security.
Garg, Deepak and Rezk, Tamara and Rajani, Vineet
(2016)
On Access Control, Capabilities, Their Equivalence, and Confused Deputy Attacks.
Garg, Deepak and Rafnsson, Willard and Sabelfeld, Andrei
(2016)
Progress-Sensitive Security for SPARK.
Garg, Deepak and Bolosteanu, Iulia
(2016)
Asymmetric Secure Multi-execution with Declassification.
Grishchenko, Ilya and Maffei, Matteo and Calzavara, Stefano
(2016)
HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving.
Chistikov, Dmitry and Majumdar, Rupak and Niksic, Filip
(2016)
Hitting Families of Schedules for Asynchronous Programs.
Kang, Jeehoon and Kim, Yoonseung and Hur, Chung-Kil and Dreyer, Derek and Vafeiadis, Viktor
(2016)
Lightweight verification of separate compilation.
Huang, Wen-Hung and Chen, Jian-Jia and Reineke, Jan
(2016)
MIRROR: symmetric timing analysis for real-time tasks on multicore platforms with shared resources.
Esparza, Javier and Ganty, Pierre and Leroux, Jérôme and Majumdar, Rupak
(2016)
Model Checking Population Protocols.
Maiya, Pallavi and Gupta, Rahul and Kanade, Aditya and Majumdar, Rupak
(2016)
Partial Order Reduction for Event-Driven Multi-threaded Programs.
Dimitrova, Rayna and Fioriti, Luis María Ferrer and Hermanns, Holger and Majumdar, Rupak
(2016)
Probabilistic CTL*: The Deductive Way.
Bonakdarpour, Borzoo and Finkbeiner, Bernd
(2016)
Runtime Verification for HyperLTL.
Soudjani, Sadegh Esmaeil Zadeh and Majumdar, Rupak and Abate, Alessandro
(2016)
Safety Verification of Continuous-Space Pure Jump Markov Processes.
Finkbeiner, Bernd and Seidl, Helmut and Müller, Christian
(2016)
Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents.
Faymonville, Peter and Finkbeiner, Bernd and Schirmer, Sebastian and Torfah, Hazem
(2016)
A Stream-Based Specification Language for Network Monitoring.
Deininger, David and Dimitrova, Rayna and Majumdar, Rupak
(2016)
Symbolic Model Checking for Factored Probabilistic Models.
Lahav, Ori and Giannarakis, Nick and Vafeiadis, Viktor
(2016)
Taming release-acquire consistency.
Damm, Werner and Finkbeiner, Bernd and Rakow, Astrid
(2016)
What You Really Need To Know About Your Neighbor.
Garg, Deepak and Çiçek, Ezgi and Paraskevopoulou, Zoe
(2016)
A type theory for incremental computational complexity with control flow changes.
Jacobs, Swen and Bloem, Roderick and Brenguier, Romain and Khalimov, Ayrat and Klein, Felix and Könighofer, Robert and Kreber, Jens and Legg, Alexander and Narodytska, Nina and Perez, Guillermo A. and Raskin, Jean-Francois and Ryzhyk, Leonid and Sankur, Ocan and Seidl, Martina and Tentrup, Leander and Walker, Adam
(2016)
The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results.
Jacobs, Swen and Tentrup, Leander and Zimmermann, Martin
(2016)
Distributed PROMPT-LTL Synthesis.
Jacobs, Swen and Klein, Felix and Schirmer, Sebastian
(2016)
A High-Level LTL Synthesis Format: TLSF v1.1.
Jacobs, Swen and Bloem, Roderick
(2016)
The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond.
Bloem, Roderick and Braud-Santoni, Nicolas and Jacobs, Swen
(2016)
Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems.
Außerlechner, Simon and Jacobs, Swen and Khalimov, Ayrat
(2016)
Tight Cutoffs for Guarded Protocols with Fairness.
Chowdhury, Omar and Garg, Deepak and Jia, Limin and Datta, Anupam
(2015)
Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits.
Bichhawat, Abhishek and Hammer, Christian and Garg, Deepak and Rajani, Vineet
(2015)
Information Flow Control for Event Handling and the DOM in Web Browsers.
Datta, Anupam and Garg, Deepak and Jia, Limin and Sen, Shayak
(2015)
A Logic of Programs with Interface-Confined Code.
Datta, Anupam and Garg, Deepak and Kaynar, Dilsun Kirli and Sharma, Divya and Sinha, Arunesh
(2015)
Program Actions as Actual Causes: A Building Block for Accountability.
Mehta, Aastha and Vahldiek-Oberwanger, Anjo and Post, Ansley and Garg, Deepak and Elnikety, Eslam and Gehrke, Johannes and Druschel, Peter and Rodrigues, Rodrigo
(2015)
Guardat: enforcing data policies at the storage layer.
Garg, Deepak and Çiçek, Ezgi and Acar, Umut A.
(2015)
Refinement Types for Incremental Computational Complexity.
Moreno-Sanchez, Pedro and Kate, Aniket and Maffei, Matteo and Pecina, Kim
(2015)
Privacy Preserving Payments in Credit Networks.
Finkbeiner, Bernd and Gieseking, Manuel and Olderog, Ernst-Rüdiger
(2015)
Adam: Causality-Based Synthesis of Distributed Systems.
Finkbeiner, Bernd and Rabe, Markus N. and Sanchez, Cesar
(2015)
Algorithms for Model Checking HyperLTL and HyperCTL ^*.
Chistikov, Dmitry and Dimitrova, Rayna and Majumdar, Rupak
(2015)
Approximate Counting in SMT and Value Estimation for Probabilistic Programs.
Kloos, Johannes and Majumdar, Rupak and Vafeiadis, Viktor
(2015)
Asynchronous Liquid Separation Types.
Majumdar, Rupak and Wang, Zilong
(2015)
Bbs: A Phase-Bounded Model Checker for Asynchronous Programs.
Backes, Michael and Mohammadi, Esfandiar and Ruffing, Tim
(2015)
Computational Soundness for Interactive Primitves.
Majumdar, Rupak and Prabhu, Vinayak S.
(2015)
Computing the Skorokhod distance between polygonal traces.
Saha, Indranil and Baruah, Sanjoy and Majumdar, Rupak
(2015)
Dynamic scheduling for networked control systems.
Verbeek, Freek and Havle, Oto and Schmaltz, Julien and Tverdyshev, Sergey and Blasum, Holger and Langenstein, Bruno and Stephan, Werner and Wolff, Burkhart and Nemouchi, Yakoub
(2015)
Formal API Specification of the PikeOS Separation Kernel.
Jung, Ralf and Swasey, David and Sieczkowski, Filip and Svendsen, Kasper and Turon, Aaron and Birkedal, Lars and Dreyer, Derek
(2015)
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.
Schneider, Sigurd and Smolka, Gert and Hack, Sebastian
(2015)
A Linear First-Order Functional Intermediate Language for Verified Compilers.
Durand-Gasselin, Antoine and Esparza, Javier and Ganty, Pierre and Majumdar, Rupak
(2015)
Model Checking Parameterized Asynchronous Shared-Memory Systems.
Hemed, Nir and Rinetzky, Noam and Vafeiadis, Viktor
(2015)
Modular Verification of Concurrency-Aware Linearizability.
Neis, Georg and Hur, Chung-Kil and Kaiser, Jan-Oliver and McLaughlin, Craig and Dreyer, Derek and Vafeiadis, Viktor
(2015)
Pilsner: a compositionally verified compiler for a higher-order imperative language.
Deshmukh, Jyotirmoy V. and Majumdar, Rupak and Prabhu, Vinayak S.
(2015)
Quantifying Conformance Using the Skorokhod Metric.
Dimitrova, Rayna and Majumdar, Rupak
(2015)
Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs.
Gavran, Ivan and Niksic, Filip and Kanade, Aditya and Majumdar, Rupak and Vafeiadis, Viktor
(2015)
Rely/Guarantee Reasoning for Asynchronous Programs.
Cortier, Véronique and Eigner, Fabienne and Kremer, Steve and Maffei, Matteo and Wiedling, Cyrille
(2015)
Type-Based Verification of Electronic Voting Protocols.
Tassarotti, Joseph and Dreyer, Derek and Vafeiadis, Viktor
(2015)
Verifying read-copy-update in a logic for weak memory.
Kang, Jeehoon and Hur, Chung-Kil and Mansky, William and Garbuzov, Dmitri and Zdancewic, Steve and Vafeiadis, Viktor
(2015)
A formal C memory model supporting integer-pointer casts.
Altmeyer, Sebastian and Davis, Robert I. and Indrusiak, Leandro Soares and Maiza, Claire and Nélis, Vincent and Reineke, Jan
(2015)
A generic and compositional framework for multicore response time analysis.
Bloem, Roderick and Chatterjee, Krishnendu and Jacobs, Swen and Könighofer, Robert
(2015)
Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information.
Jacobs, Swen and Bloem, Roderick and Brenguier, Romain and Könighofer, Robert and Perez, Guillermo A. and Raskin, Jean-Francois and Ryzhyk, Leonid and Sankur, Ocan and Seidl, Martina and Tentrup, Leander and Walker, Adam
(2015)
The Second Reactive Synthesis Competition (SYNTCOMP 2015).
Backes, Michael and Manoharan, Praveen and Mohammadi, Esfandiar
(2014)
TUC: Time-sensitive and Modular Analysis of Anonymous Communication.
Datta, Anupam and Garg, Deepak and Jia, Limin and Chowdhury, Omar
(2014)
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.
Reineke, Jan and Doerfert, Johannes
(2014)
Architecture-parametric timing analysis.
Damm, Werner and Finkbeiner, Bernd
(2014)
Automatic Compositional Synthesis of Distributed Systems.
Li, Cheng and Leitão, João and Clement, Allen and Preguiça, Nuno M. and Rodrigues, Rodrigo and Vafeiadis, Viktor
(2014)
Automating the Choice of Consistency Levels in Replicated Systems.
Reineke, Jan and Tripakis, Stavros
(2014)
Basic Problems in Multi-View Modeling.
Hüchting, Reiner and Majumdar, Rupak and Meyer, Roland
(2014)
Bounds on mobility.
Kupriyanov, Andrey and Finkbeiner, Bernd
(2014)
Causal Termination of Multi-threaded Programs.
Reineke, Jan and Maksoud, Mohamed Abdel
(2014)
A Compiler Optimization to Increase the Efficiency of WCET Analysis.
Backes, Michael and Mohammadi, Esfandiar and Ruffing, Tim
(2014)
Computational Soundness Results for ProVerif - Bridging the Gap from Trace Properties to Uniformity.
Finkbeiner, Bernd and Torfah, Hazem
(2014)
Counting Models of Linear-Time Temporal Logic.
Carzaniga, Antonio and Goffi, Alberto and Gorla, Alessandra and Mattavelli, Andrea and Pezzè, Mauro
(2014)
Cross-checking oracles from intrinsic software redundancy.
Dimitrova, Rayna and Majumdar, Rupak
(2014)
Deductive control synthesis for alternating-time logics.
Finkbeiner, Bernd and Tentrup, Leander
(2014)
Detecting Unrealizable Specifications of Distributed Systems.
Eigner, Fabienne and Kate, Aniket and Maffei, Matteo and Pampaloni, Francesca and Pryvalov, Ivan
(2014)
Differentially Private Data Aggregation with Optimal Utility.
Esmaeilsabzali, Shahram and Majumdar, Rupak and Wies, Thomas and Zufferey, Damien
(2014)
Dynamic package interfaces.
Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Majumdar, Rupak
(2014)
Edit Distance for Timed Automata.
Finkbeiner, Bernd and Tentrup, Leander
(2014)
Fast DQBF refutation.
Turon, Aaron and Vafeiadis, Viktor and Dreyer, Derek
(2014)
GPS: navigating weak memory with ghosts, protocols, and separation.
Bichhawat, Abhishek and Rajani, Vineet and Garg, Deepak and Hammer, Christian
(2014)
Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis.
Majumdar, Rupak and Tetali, Sai Deep and Wang, Zilong
(2014)
Kuai: A model checker for software-defined networks.
Faymonville, Peter and Finkbeiner, Bernd and Peled, Doron
(2014)
Monitoring Parametric Temporal Logic.
Finkbeiner, Bernd and Olderog, Ernst-Rüdiger
(2014)
Petri Games: Synthesis of Distributed Systems with Causal Memory.
Eigner, Fabienne and Kate, Aniket and Maffei, Matteo and Pampaloni, Francesca and Pryvalov, Ivan
(2014)
Privacy-preserving Data Aggregation with Optimal Utility Using Arithmetic SMC -- Extended Abstract.
Oh, Se Eun and Chun, Ji Young and Jia, Limin and Garg, Deepak and Gunter, Carl A. and Datta, Anupam
(2014)
Privacy-preserving audit for broker-based health information exchange.
Maiya, Pallavi and Kanade, Aditya and Majumdar, Rupak
(2014)
Race Detection for Android Applications.
Gligoric, Milos and Majumdar, Rupak and Sharma, Rohan and Eloussi, Lamyaa and Marinov, Darko
(2014)
Regression Test Selection for Distributed Software Histories.
Abel, Andreas and Reineke, Jan
(2014)
Reverse engineering of cache replacement policies in Intel microprocessors and their evaluation.
Esparza, Javier and Ledesma-Garza, Ruslán and Majumdar, Rupak and Meyer, Philipp J. and Niksic, Filip
(2014)
An SMT-based Approach to Coverability Analysis.
Alvin, Christopher and Gulwani, Sumit and Mukhopadhyay, Supratik and Majumdar, Rupak
(2014)
Synthesis of Geometry Proof Problems.
Clarkson, Michael R. and Finkbeiner, Bernd and Koleini, Masoud and Micinski, Kristopher K. and Rabe, Markus N. and Sanchez, Cesar
(2014)
Temporal Logics for Hyperproperties.
Chowdhury, Omar and Jia, Limin and Garg, Deepak and Datta, Anupam
(2014)
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.
Simkin, Mark and Schröder, Dominique and Bulling, Andreas and Fritz, Mario
(2014)
Ubic: Bridging the Gap between Digital Cryptography and the Physical World.
Chistikov, Dmitry and Majumdar, Rupak
(2014)
Unary Pushdown Automata and Straight-Line Programs.
Noschinski, Lars and Rizkallah, Christine and Mehlhorn, Kurt
(2014)
Verification of Certifying Computations through AutoCorres and Simpl.
Finkbeiner, Bernd and Seidl, Helmut and Kovács, Máté
(2013)
Relational Abstract Interpretation for the Verification of 2-Hypersafety Properties.
Doychev, Goran and Feld, Dominik and Köpf, Boris and Mauborgne, Laurent and Reineke, Jan
(2013)
CacheAudit: A Tool for the Static Analysis of Cache Side Channels.
Eigner, Fabienne and Maffei, Matteo
(2013)
Differential Privacy by Typing in Security Protocols.
Maffei, Matteo and Pecina, Kim and Reinert, Manuel
(2013)
Security and Privacy by Declarative Design.
Backes, Michael and Bendun, Fabian and Unruh, Dominique
(2013)
Computational Soundness of Symbolic Zero-Knowledge Proofs: Weaker Assumptions and Mechanized Verification.
Angius, Alessio and Horváth, András and Wolf, Verena
(2013)
Approximate Transient Analysis of Queuing Networks by Quasi Product Forms.
Carzaniga, Antonio and Gorla, Alessandra and Mattavelli, Andrea and Perino, Nicolò and Pezzè, Mauro
(2013)
Automatic recovery from runtime failures.
Zamani, Majid and Esfahani, Peyman Mohajerin and Majumdar, Rupak and Abate, Alessandro and Lygeros, John
(2013)
Bisimilar finite abstractions of stochastic control systems.
Finkbeiner, Bernd and Schewe, Sven
(2013)
Bounded synthesis.
Kupriyanov, Andrey and Finkbeiner, Bernd
(2013)
Causality-Based Verification of Multi-threaded Programs.
Majumdar, Rupak and Saha, Indranil and Ueda, Koichi and Yazarel, Hakan
(2013)
Compositional Equivalence Checking for Models and Code of Control Systems.
Wieder, Alexander and Brandenburg, Björn B.
(2013)
Efficient partitioning of sporadic real-time tasks with shared resources and spin locks.
Majumdar, Rupak and Wang, Zilong
(2013)
Expand, Enlarge, and Check for Branching Vector Addition Systems.
Brandenburg, Björn B.
(2013)
A Fully Preemptive Multiprocessor Semaphore Protocol for Latency-Sensitive Real-Time Applications.
Brandenburg, Björn B.
(2013)
Improved analysis and evaluation of real-time semaphore protocols for P-FP scheduling.
Kloos, Johannes and Majumdar, Rupak and Niksic, Filip and Piskac, Ruzica
(2013)
Incremental Inductive Coverability.
Bugliesi, Michele and Calzavara, Stefano and Eigner, Fabienne and Maffei, Matteo
(2013)
Logical Foundations of Secure Resource Management.
Dimitrova, Rayna and Finkbeiner, Bernd
(2013)
Lossy Channel Games under Incomplete Information.
Abel, Andreas and Reineke, Jan
(2013)
Measurement-based modeling of the cache replacement policy.
Gligoric, Milos and Majumdar, Rupak
(2013)
Model Checking Database Applications.
Tetali, Sai Deep and Lesani, Mohsen and Majumdar, Rupak and Millstein, Todd
(2013)
MrCrypt: Static Analysis for Secure Cloud Computations.
Ziliani, Beta and Dreyer, Derek and Krishnaswami, Neelakantan R. and Nanevski, Aleksandar and Vafeiadis, Viktor
(2013)
Mtac: a monad for typed tactic programming in Coq.
Baruah, Sanjoy and Brandenburg, Björn B.
(2013)
Multiprocessor Feasibility Analysis of Recurrent Task Systems with Specified Processor Affinities.
Wieder, Alexander and Brandenburg, Björn B.
(2013)
On Spin Locks in AUTOSAR: Blocking Analysis of FIFO, Unordered, and Priority-Ordered Spin Locks.
Esparza, Javier and Ganty, Pierre and Majumdar, Rupak
(2013)
Parameterized verification of asynchronous shared-memory systems.
Andalam, Sidharta and Girault, Alain and Sinha, Roopak and Roop, Partha S. and Reineke, Jan
(2013)
Precise timing analysis for direct-mapped caches.
Zengin, Mustafa and Vafeiadis, Viktor
(2013)
A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism.
Kovács, Máté and Seidl, Helmut and Finkbeiner, Bernd
(2013)
Relational abstract interpretation for the verification of 2-hypersafety properties.
Majumdar, Rupak and Meyer, Roland and Wang, Zilong
(2013)
Static Provenance Verification for Message Passing Programs.
Kloos, Johannes and Majumdar, Rupak
(2013)
Supervisor Synthesis for Controller Upgrades.
Darulova, Eva and Kuncak, Viktor and Majumdar, Rupak and Saha, Indranil
(2013)
Synthesis of fixed-point programs.
Cohen, Ernie and Paul, Wolfgang J. and Schmaltz, Sabine
(2013)
Theory of Multi Core Hypervisor Verification.
Hüchting, Reiner and Majumdar, Rupak and Meyer, Roland
(2013)
A Theory of Name Boundedness.
Calin, Georgel and Derevenetc, Egor and Majumdar, Rupak and Meyer, Roland
(2013)
A Theory of Partitioned Global Address Spaces.
Chistikov, Dmitry and Majumdar, Rupak
(2013)
A Uniformization Theorem for Nested Word to Word Transductions.
Backes, Michael and Malik, Ankit and Unruh, Dominique
(2012)
Computational Soundness without Protocol Restrictions.
Backes, Michael and Barthe, Gilles and Berg, Matthias and Grégoire, Benjamin and Kunz, César and Skoruppa, Malte and Béguelin, Santiago Zanella
(2012)
Verified Security of Merkle-Damgård.
Genovese, Valerio and Garg, Deepak and Rispoli, Daniele
(2012)
Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction.
Backes, Michael and Maffei, Matteo and Pecina, Kim
(2012)
Automated Synthesis of Secure Distributed Applications.
Bugliesi, Michele and Calzavara, Stefano and Eigner, Fabienne and Maffei, Matteo
(2012)
Affine Refinement Types for Authentication and Authorization.
Majumdar, Rupak and Zamani, Majid
(2012)
Approximately Bisimilar Symbolic Models for Digital Control Systems.
Majumdar, Rupak and Saha, Indranil and Shashidhar, K C and Wang, Zilong
(2012)
CLSE: Closed-Loop Symbolic Execution.
Schmidt, Jens M
(2012)
Certifying 3-Connectivity in Linear Time.
Paul, Wolfgang J. and Schmaltz, Sabine and Shadrin, Andrey
(2012)
Completing the Automated Verification of a Small Hypervisor - Assembler Code Verification.
Peter, Hans-Jörg and Finkbeiner, Bernd
(2012)
The Complexity of Bounded Synthesis for Timed Control with Partial Observability.
Dimitrova, Rayna and Finkbeiner, Bernd
(2012)
Counterexample-Guided Synthesis of Observation Predicates.
Garg, Deepak and Genovese, Valerio and Negri, Sara
(2012)
Countermodels from Sequent Calculi in Multi-Modal Logics.
Lee, Jonathan K. and Palsberg, Jens and Majumdar, Rupak and Hong, Hong
(2012)
Efficient May Happen in Parallel Analysis for Async-finish Parallelism.
Kuhtz, Lars and Finkbeiner, Bernd
(2012)
Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds.
Maksoud, Mohamed Abdel and Reineke, Jan
(2012)
An Empirical Evaluation of the Influence of the Load-Store Unit on WCET Analysis.
Basin, David and Jugé, Vincent and Klaedtke, Felix and Zvalinescu, Eugen
(2012)
Enforceable Security Policies Revisited.
Fischer, Jeffrey and Majumdar, Rupak and Esmaeilsabzali, Shahram
(2012)
Engage: A Deployment Management System.
Chatterjee, Krishnendu and Chmelik, Martin and Majumdar, Rupak
(2012)
Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games.
Tabuada, Paulo and Balkan, Ayca and Caliskan, Sina Yamac and Shoukry, Yasser and Majumdar, Rupak
(2012)
Input-Output stability for discrete systems.
Schmaltz, Sabine and Shadrin, Andrey
(2012)
Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT.
Genovese, Valerio and Garg, Deepak and Rispoli, Daniele
(2012)
Labeled Goal-Directed Search in Access Control Logic.
Long, Zhenyue and Calin, Georgel and Majumdar, Rupak and Meyer, Roland
(2012)
Language-Theoretic Abstraction Refinement.
Finkbeiner, Bernd and Jacobs, Swen
(2012)
Lazy Synthesis.
Cheikhrouhou, Lassaad and Stephan, Werner and Fischlin, Marc and Ullmann, Markus
(2012)
Merging the Cryptographic Security Analysis and the Algebraic-Logic Security Proof of PACE.
Dimitrova, Rayna and Finkbeiner, Bernd and Kovács, Máté and Rabe, Markus N. and Seidl, Helmut
(2012)
Model Checking Information Flow in Reactive Systems.
Ehlers, Rüdiger and Finkbeiner, Bernd
(2012)
Monitoring Realizability.
Dimitrova, Rayna and Finkbeiner, Bernd and Rabe, Markus N.
(2012)
Monitoring Temporal Information Flow.
Backes, Michael and Busenius, Alex and Hriţcu, Cătălin
(2012)
On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols.
Esparza, Javier and Ganty, Pierre and Majumdar, Rupak
(2012)
A Perfect Model for Bounded Verification.
Reischuk, Raphael M. and Backes, Michael and Gehrke, Johannes
(2012)
SAFE Extensibility of Data-Driven Web Applications.
Carreira, João Carlos Menezes and Rodrigues, Rodrigo and Candea, George and Majumdar, Rupak
(2012)
Scalable Testing of File System Checkers.
Krishnaswami, Neelakantan R. and Turon, Aaron and Dreyer, Derek and Garg, Deepak
(2012)
Superficially substructural types.
Majumdar, Rupak and Saha, Indranil and Zamani, Majid
(2012)
Synthesis of minimal-error control software.
Finkbeiner, Bernd and Peter, Hans-Jörg
(2012)
Template-Based Controller Synthesis for Timed Systems.
Saha, Indranil and Majumdar, Rupak
(2012)
Trigger memoization in self-triggered control.
Vahldiek, Anjo and Elnikety, Eslam and Post, Ansley and Druschel, Peter and Garg, Deepak and Gehrke, Johannes and Rodrigues, Rodrigo
(2012)
Trusted Storage.
Alkassar, Eyad and Cohen, Ernie and Kovalev, Mikhail and Paul, Wolfgang J.
(2012)
Verification of TLB Virtualization Implemented in C.
Datta, Anupam and Garg, Deepak and Jia, Limin
(2011)
Policy auditing over incomplete logs: theory, implementation and applications.
Nanevski, Aleksandar and Banerjee, Anindya and Garg, Deepak
(2011)
Verification of Information Flow and Access Control Policies with Dependent Types.
Backes, Michael and Maffei, Matteo and Pecina, Kim
(2011)
A Security API for Distributed Social Networks.
Mantel, Heiko and Sands, David and Sudbrock, Henning
(2011)
Assumptions and Guarantees for Compositional Noninterference.
Ngo, Long and Boyd, Colin and Nieto, Juan Gonzalez
(2011)
Automated proofs for Diffie-Hellman-based key exchanges.
Backes, Michael and Hriţcu, Cătălin and Tarrach, Thorsten
(2011)
Automatically Verifying Typing Constraints for a Data Processing Language.
Jose, Manu and Majumdar, Rupak
(2011)
Bug-Assist: Assisting Fault Localization in ANSI-C Programs.
Herter, Jörg and Backes, Peter and Haupenthal, Florian and Reineke, Jan
(2011)
CAMA: A Predictable Cache-Aware Memory Allocator.
Jose, Manu and Majumdar, Rupak
(2011)
Cause Clue Clauses: Error Localization Using Maximum Satisfiability.
Meiser, Sebastian
(2011)
Computational Soundness of Passively Secure Encryption in Presence of Active Adversaries.
Stuijk, Sander and Basten, Twan and Akesson, Benny and Geilen, Marc and Moreira, Orlando and Reineke, Jan
(2011)
Designing next-generation real-time streaming systems.
Damm, Werner and Finkbeiner, Bernd
(2011)
Does It Pay to Extend the Perimeter of a World Model?
Mardziel, Piotr and Magill, Stephen and Hicks, Michael and Srivatsa, Mudhakar
(2011)
Dynamic Enforcement of Knowledge-based Security Policies.
Asghar, Muhammad Rizwan and Ion, Mihaela and Russello, Giovanni and Crispo, Bruno
(2011)
ESPOON: Enforcing Encrypted Security Policies in Outsourced Environments.
Mikeev, Linar and Sandmann, Werner and Wolf, Verena
(2011)
Efficient calculation of rare event probabilities in Markovian queueing networks.
Cheney, James
(2011)
A Formal Framework for Provenance Security.
Delaune, Stephanie and Kremer, Steve and Ryan, Mark D. and Steel, Graham
(2011)
Formal analysis of protocols based on TPM state registers.
Backes, Michael and Maffei, Matteo and Pecina, Kim and Reischuk, Raphael M.
(2011)
G2C: Cryptographic Protocols from Goal-Driven Specifications.
Dupressoir, Francois and Gordon, Andrew D. and Jurjens, Jan and Naumann, David A.
(2011)
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.
Jhala, Ranjit and Majumdar, Rupak and Rybalchenko, Andrey
(2011)
HMC: Verifying Functional Programs Using Abstract Interpreters.
Frau, Simone and Dashti, Mohammad Torabi
(2011)
Integrated Specification and Verification of Security Protocols and Policies.
Zamani, Majid and Majumdar, Rupak
(2011)
A Lyapunov approach in incremental stability.
Chatterjee, Krishnendu and Majumdar, Rupak
(2011)
Minimum Attention Controller Synthesis for Omega-regular Objectives.
Backes, Michael and Berg, Matthias and Köpf, Boris
(2011)
Non-Uniform Distributions in Quantitative Information-Flow.
Reineke, Jan and Liu, Isaac and Patel, Hiren D. and Kim, Sungjun and Lee, Edward A.
(2011)
PRET DRAM controller: bank privatization for predictability and temporal isolation.
Majumdar, Rupak and Saha, Indranil and Zamani, Majid
(2011)
Performance-aware Scheduler Synthesis for Control Systems.
Roy, Pritam and Tabuada, Paulo and Majumdar, Rupak
(2011)
Pessoa 2.0: A Controller Synthesis Tool for Cyber-physical Systems.
Ehlers, Rüdiger and Finkbeiner, Bernd
(2011)
Reactive Safety.
Sevcík, Jaroslav and Vafeiadis, Viktor and Nardelli, Francesco Zappa and Jagannathan, Suresh and Sewell, Peter
(2011)
Relaxed-memory concurrency and verified compilation.
Bugliesi, Michele and Calzavara, Stefano and Eigner, Fabienne and Maffei, Matteo
(2011)
Resource-aware Authorization Policies for Statically Typed Cryptographic Protocols.
Majumdar, Rupak and Render, Elaine and Tabuada, Paulo
(2011)
Robust Discrete Synthesis Against Unspecified Disturbances.
Lapin, Maksim and Mikeev, Linar and Wolf, Verena
(2011)
SHAVE: stochastic hybrid analysis of markov population models.
Moore, Scott and Chong, Stephen
(2011)
Static analysis for efficient hybrid information-flow control.
Grund, Daniel and Reineke, Jan and Wilhelm, Reinhard
(2011)
A Template for Predictability Definitions with Supporting Evidence.
Bui, Dai N and Lee, Edward A. and Liu, Isaac and Patel, Hiren D. and Reineke, Jan
(2011)
Temporal isolation on multiprocessing architectures.
Datta, Anupam and Blocki, Jeremiah and Christin, Nicolas and DeYoung, Henry and Garg, Deepak and Jia, Limin and Kaynar, Dilsun Kirli and Sinha, Arunesh
(2011)
Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms.
Backes, Michael and Hriţcu, Cătălin and Maffei, Matteo
(2011)
Union and Intersection Types for Secure Protocol Implementations.
Alkassar, Eyad and Böhme, Sascha and Mehlhorn, Kurt and Rizkallah, Christine
(2011)
Verification of Certifying Computations.
Finkbeiner, Bernd and Kuhtz, Lars
(2011)
Weak Kripke Structures and LTL.
Backes, Michael and Dürmuth, Markus and Gerling, Sebastian and Pinkal, Manfred and Sporleder, Caroline
(2010)
Acoustic Side-Channel Attacks of Printers.
Hammer, Christian
(2010)
Experiences with PDG-based IFC.
Vaziri, Mandana and Tip, Frank and Dolby, Julian and Hammer, Christian and Vitek, Jan
(2010)
A Type System for Data-Centric Synchronization.
Hammer, Christian and Dolby, Julian and Vaziri, Mandana and Tip, Frank
(2008)
Dynamic detection of atomic-set-serializability violations.
Giffhorn, Dennis and Hammer, Christian
(2008)
Precise Analysis of Java Programs using JOANA (Tool Demonstration).
Hammer, Christian and Schaade, Rüdiger and Snelting, Gregor
(2008)
Static path conditions for Java.
Giffhorn, Dennis and Hammer, Christian
(2007)
An Evaluation of Precise Slicing Algorithms for Concurrent Programs.
Hammer, Christian and Grimme, Martin and Krinke, Jens
(2006)
Dynamic path conditions in dependence graphs.
Hammer, Christian and Krinke, Jens and Snelting, Gregor
(2006)
Information Flow Control for Java Based on Path Conditions in Dependence Graphs.
Hammer, Christian and Krinke, Jens and Nodes, Frank
(2006)
Intransitive Noninterference in Dependence Graphs.
Hammer, Christian and Snelting, Gregor
(2004)
An improved slicer for Java.
Article
Finkbeiner, Bernd
(2023)
Logics and Algorithms for Hyperproperties.
ACM SIGLOG News, 10 (2).
pp. 4-23.
ISSN 2372-3491
Frenkel, Hadar and Grumberg, Orna and Pasareanu, Corina and Sheinvald, Sarai
(2022)
Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties.
International Journal on Software Tools for Technology Transfer.
ISSN 1433-2779
Finkbeiner, Bernd and Geier, Gideon and Passing, Noemi
(2022)
Specification decomposition for reactive synthesis.
Innovations in Systems and Software Engineering.
Bensmail, Julien and Mc Inerney, Fionn
(2022)
On a vertex-capturing game.
Theoretical Computer Science, 923.
pp. 27-46.
ISSN 0304-3975
Bensmail, Julien and Fioravantes, Foivos and Mc Inerney, Fionn and Nisse, Nicolas
(2022)
The Largest Connected Subgraph Game.
Algorithmica, 84 (9).
pp. 2533-2555.
ISSN 0178-4617
Basin, David and Cremers, Cas and Dreier, Jannik and Sasse, Ralf
(2022)
Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols.
IEEE Security and Privacy.
ISSN 1540-7993
Finkbeiner, Bernd and Fränzle, Martin and Kohn, Florian and Kröger, Paul
(2022)
A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation.
Algorithms, 15 (4).
Bharadwaj, Suda and Dimitrova, Rayna and Quattrociocchi, Jesse and Topcu, Ufuk
(2022)
Synthesis of Strategies for Autonomous Surveillance on Adversarial Targets.
Robotics and Autonomous Systems, 153.
ISSN 0921-8890
Finkbeiner, Bernd and Passing, Noemi
(2022)
Compositional synthesis of modular systems.
Innovations in Systems and Software Engineering.
Finkbeiner, Bernd and Klein, Felix and Metzger, Niklas
(2022)
Live synthesis.
Innovations in Systems and Software Engineering.
ISSN 1614-5046
Havrikov, Nikolas and Kampmann, Alexander and Zeller, Andreas
(2022)
From Input Coverage to Code Coverage:
Systematically Covering Input Structure with k-Paths.
ACM Transactions on Software Engineering and Methodology.
ISSN 1049-331X
(Submitted)
Biewer, Sebastian and Dimitrova, Rayna and Fries, Michael and Gazda, Maciej and Heinze, Thomas and Hermanns, Holger and Mousavi, Mohammad Reza
(2022)
Conformance Relations and Hyperproperties for Doping Detection in Time and Space.
Logical Methods in Computer Science, 18 (1).
Di Tizio, Giorgio and Speicher, Patrick and Simeonovski, Milivoj and Backes, Michael and Stock, Ben and Künnemann, Robert
(2022)
Pareto-Optimal Defenses for the Web Infrastructure: Theory and Practice.
ACM Transactions on Privacy and Security, 1 (1).
ISSN 2471-2566
Focke, Jacob and Goldberg, Leslie Ann and Roth, Marc and Živný, Stanislav
(2021)
Counting Homomorphisms to K4-minor-free Graphs, modulo 2.
SIAM Journal on Discrete Mathematics, 35 (4).
pp. 2749-2814.
ISSN 0895-4801
Finkbeiner, Bernd and Schmitt, Frederik
(2021)
Künstliche Intelligenz in der Softwareentwicklung: Über die Schulter geschaut.
iX Magazin für professionelle Informationstechnik (8).
pp. 40-43.
ISSN 0935-9680
Cohn-Gordon, Katriel and Cremers, Cas and Dowling, Benjamin and Garratt, Luke and Stebila, Douglas
(2020)
A Formal Security Analysis of Key Establishment in the Signal Messaging Protocol.
Journal of Cryptology.
(In Press)
Kiesl, Benjamin and Rebola-Pardo, Adrián and Heule, Marijn J.H. and Biere, Armin
(2020)
Simulating Strong Practical Proof Systems with Extended Resolution.
Journal of Automated Reasoning, 64.
pp. 1247-1267.
ISSN 0168-7433
Troncoso, Carmela and Payer, Matthias and Hubaux, Jean-Pierre and Salathé, Marcel and Larus, James and Lueks, Wouter and Stadler, Theresa and Pyrgelis, Apostolos and Antonioli, Daniele and Barman, Ludovic and Chatel, Sylvain and Paterson, Kenneth G. and Capkun, Srdjan and Basin, David and Beutel, Jan and Jackson, Dennis and Roeschlin, Marc and Leu, Patrick and Preneel, Bart and Smart, Nigel and Abidin, Aysajan and Gürses, Seda and Veale, Michael and Cremers, Cas and Backes, Michael and Tippenhauer, Nils Ole and Binns, Reuben and Cattuto, Ciro and Barrat, Alain and Fiore, Dario and Barbosa, Manuel and Oliveira, Rui and Pereira, José
(2020)
Decentralized Privacy-Preserving Proximity Tracing.
IEEE Data Engineering Bulletin Volume 43, Number 2, June 2020.
pp. 36-66.
Finkbeiner, Bernd and Hahn, Christopher and Stenger, Marvin and Tentrup, Leander
(2020)
Efficient monitoring of hyperproperties using prefix trees.
International Journal on Software Tools for Technology Transfer.
ISSN 1433-2779
Mirzaie, Nahal and Faghih, Fathiyeh and Jacobs, Swen and Bonakdarpour, Borzoo
(2019)
Parameterized synthesis of self-stabilizing protocols in symmetric networks.
Acta Informatica.
ISSN 1432-0525
Jacobs, Swen and Sakr, Mouhammad
(2019)
A symbolic algorithm for lazy synthesis of eager strategies.
Acta Informatica.
ISSN 1432-0525
Baumeister, Jan and Finkbeiner, Bernd and Schwenger, Maximilian and Torfah, Hazem
(2019)
FPGA Stream-Monitoring of Real-time Properties.
ACM Trans. Embed. Comput. Syst., 18 (5s).
88:1-88:24.
Cremers, Cas and Dehnel-Wild, Martin and Milner, Kevin
(2019)
Secure Authentication in the Grid: A Formal Analysis of DNP3 SAv5.
Journal of Computer Security, 27 (2).
pp. 203-232.
Heule, Marijn J.H. and Kiesl, Benjamin and Biere, Armin
(2019)
Strong Extension-Free Proof Systems.
Journal of Automated Reasoning.
ISSN 0168-7433
Grosse, Kathrin and Trost, Thomas A. and Mosbach, Marius and Backes, Michael
(2019)
Adversarial Initialization - when your network performs the way I want -.
ArXiv e-prints.
Finkbeiner, Bernd and Hahn, Christopher and Stenger, Marvin and Tentrup, Leander
(2019)
Monitoring hyperproperties.
Formal Methods Syst. Des., 54 (3).
pp. 336-363.
Jacobs, Swen and Tentrup, Leander and Zimmermann, Martin
(2018)
Distributed synthesis for parameterized temporal logics.
Information and Computation, 262 (2).
pp. 311-328.
Grosse, Kathrin and Smith, Michael Thomas and Backes, Michael
(2018)
Killing Three Birds with one Gaussian Process:
Analyzing Attack Vectors on Classification.
ArXiv e-prints.
(Submitted)
Thanh Nguyen, Binh and Sprenger, Christoph and Cremers, Cas
(2018)
Abstractions for security protocol verification.
Journal of Computer Security.
(In Press)
Basin, David and Cremers, Cas and Kim, Tiffany Hyun-Jin and Perrig, Adrian and Sasse, Ralf and Szalachowski, Pavel
(2018)
Design, Analysis, and Implementation of ARPKI: An Attack-Resilient Public-Key Infrastructure.
IEEE Transactions on Dependable and Secure Computing, 15 (3).
pp. 393-408.
Giechaskiel, Ilias and Cremers, Cas and Rasmussen, Kasper B.
(2018)
When the Crypto in Cryptocurrencies Breaks: Bitcoin Security under Broken Primitives.
IEEE Security & Privacy.
Boyd, Colin and Cremers, Cas and Feltz, Michèle and Paterson, Kenneth G. and Poettering, Bertram and Stebila, Douglas
(2017)
ASICS: Authenticated Key Exchange Security Incorporating
Certification Systems.
International Journal of Information Security, 16 (2).
pp. 151-171.
Cremers, Cas and Horvat, Marko and Hoyland, Jonathan and Scott, Sam and van der Merwe, Thyla
(2017)
A Comprehensive Symbolic Analysis of TLS 1.3.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security.
Swasey, David and Garg, Deepak and Dreyer, Derek
(2017)
Robust and compositional verification of object capability patterns.
OOPSLA, 1.
89:1–89:26.
Basin, David and Cremers, Cas and Dreier, Jannik and Sasse, Ralf
(2017)
Symbolically Analyzing Security Protocols Using Tamarin.
SIGLOG News, 4 (4).
pp. 19-30.
Jacobs, Swen and Bloem, Roderick and Brenguier, Romain and Ehlers, Rüdiger and Hell, Timotheus and Könighofer, Robert and Perez, Guillermo A. and Raskin, Jean-Francois and Ryzhyk, Leonid and Sankur, Ocan and Seidl, Martina and Tentrup, Leander and Walker, Adam
(2017)
The first reactive synthesis competition (SYNTCOMP 2014).
STTT, 19 (3).
pp. 367-390.
Kremer, Steve and Künnemann, Robert
(2016)
Automated analysis of security protocols with global state.
Journal of Computer Security.
Maffei, Matteo
(2016)
Security & Privacy Column.
SIGLOG News.
Lv, Mingsong and Guan, Nan and Reineke, Jan and Wilhelm, Reinhard and Yi, Wang
(2016)
A Survey on Static Cache Analysis for Real-Time Systems.
LITES, 3 (1).
05:1-05:48.
Bloem, Roderick and Jacobs, Swen and Khalimov, Ayrat and Konnov, Igor and Rubin, Sasha and Veith, Helmut and Widder, Josef
(2016)
Decidability in Parameterized Verification.
SIGACT News, 47 (2).
pp. 53-64.
Bugliesi, Michele and Calzavara, Stefano and Eigner, Fabienne and Maffei, Matteo
(2015)
Affine Refinement Types for Secure Distributed Programming.
ACM Transactions on Programming Languages and Systems, 37 (4).
11:1-11:66.
Datta, Anupam and Garg, Deepak and Jia, Limin and Sen, Shayak
(2015)
System M: A Program Logic for Code Sandboxing and Identification.
The Computing Research Repository (CoRR).
Doychev, Goran and Köpf, Boris and Mauborgne, Laurent and Reineke, Jan
(2015)
CacheAudit: A Tool for the Static Analysis of Cache Side Channels.
ACM Trans. Inf. Syst. Secur., 18 (1).
4:1-4:32.
Birkedal, Lars and Dreyer, Derek and Gardner, Philippa and Shao, Zhong
(2015)
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).
Dagstuhl Reports, 5 (5).
pp. 1-23.
Ziliani, Beta and Dreyer, Derek and Krishnaswami, Neelakantan R. and Nanevski, Aleksandar and Vafeiadis, Viktor
(2015)
Mtac: A monad for typed tactic programming in Coq.
J. Funct. Program., 25.
Brandenburg, Björn B.
(2014)
Blocking Optimality in Distributed Real-Time Locking Protocols.
LITES, 1 (2).
01: 1-01: 22.
Axer, Philip and Ernst, Rolf and Falk, Heiko and Girault, Alain and Grund, Daniel and Guan, Nan and Jonsson, Bengt and Marwedel, Peter and Reineke, Jan and Rochange, Christine and Sebastian, Maurice and Hanxleden, Reinhard von and Wilhelm, Reinhard and Yi, Wang
(2014)
Building timing predictable embedded systems.
ACM Transactions on Embedded Computing Systems, 13 (4).
p. 82.
Rossberg, Andreas and Russo, Claudio V and Dreyer, Derek
(2014)
F-ing modules.
J. Funct. Program., 24 (5).
pp. 529-607.
Verbeek, Freek and Tverdyshev, Sergey and Havle, Oto and Blasum, Holger and Langenstein, Bruno and Stephan, Werner and Nemouchi, Yakoub and Feliachi, Abderrahmane and Wolff, Burkhart and Schmaltz, Julien
(2014)
Formal Specification of a Generic Separation Kernel.
Archive of Formal Proofs, 2014.
Backes, Michael and Hriţcu, Cătălin and Maffei, Matteo
(2014)
Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations.
Journal of Computer Security, 22 (2).
pp. 301-353.
Sevcík, Jaroslav and Vafeiadis, Viktor and Nardelli, Francesco Zappa and Jagannathan, Suresh and Sewell, Peter
(2013)
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.
Journal of the ACM, 60 (3).
p. 22.
Nanevski, Aleksandar and Banerjee, Anindya and Garg, Deepak
(2013)
Dependent Type Theory for Verification of Information Flow and Access Control Policies.
ACM Transactions on Programming Languages and Systems, 35 (2).
Asghar, Muhammad Rizwan and Ion, Mihaela and Russello, Giovanni and Crispo, Bruno
(2013)
ESPOON$_ERBAC$: Enforcing Security Policies in Outsourced Environments.
Computers and Security, 35.
pp. 2-24.
ISSN 0167-4048
Elmasry, Amr and Schmidt, Jens M. and Mehlhorn, Kurt
(2013)
Every DFS Tree of a 3-Connected Graph Contains a Contractible Edge.
Journal of Graph Theory, 72 (1).
pp. 112-121.
Alkassar, Eyad and Böhme, Sascha and Mehlhorn, Kurt and Rizkallah, Christine
(2013)
A Framework for the Verification of Certifying Computations.
Journal of Automated Reasoning.
pp. 1-33.
Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek
(2013)
How to make ad hoc proof automation less ad hoc.
J. Funct. Program., 23 (4).
pp. 357-401.
Brandenburg, Björn B. and Anderson, James H.
(2013)
The OMLP family of optimal multiprocessor real-time locking protocols.
Design Automation for Embedded Systems, 17 (2).
pp. 277-342.
Mikeev, Linar and Neuhäußer, Martin R. and Spieler, David and Wolf, Verena
(2013)
On-the-fly verification and optimization of DTA-properties for large Markov chains.
Formal Methods in System Design, 43 (2).
pp. 313-337.
Backes, Michael and Hriţcu, Cătălin and Maffei, Matteo
(2013)
Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations.
Special issue of the Journal of Computer Security (JCS) for TOSCA-SecCo.
Ganty, Pierre and Majumdar, Rupak
(2012)
Algorithmic Verification of Asynchronous Programs.
ACM Transactions on Programming Languages and Systems, 34 (1).
6:1-6:48.
Elmasry, Amr and Mehlhorn, Kurt and Schmidt, Jens M.
(2012)
An O(n+m) Certifying Triconnnectivity Algorithm for Hamiltonian Graphs.
Algorithmica, 62 (3-4).
pp. 754-766.
Garg, Deepak and Pfenning, Frank
(2012)
Stateful authorization logic - Proof theory and a case study.
Journal of Computer Security, 20 (4).
pp. 353-391.
Katoen, Joost-Pieter and Klink, Daniel and Leucker, Martin and Wolf, Verena
(2012)
Three-valued abstraction for probabilistic systems.
Journal of Logic and Algebraic Programming, 81 (4).
pp. 356-389.
Grund, Daniel and Reineke, Jan and Gebhard, Gernot
(2011)
Branch target buffers: WCET analysis framework and timing predictability.
Journal of Systems Architecture - Embedded Systems Design, 57 (6).
pp. 625-637.
Henzinger, Thomas A and Jobstmann, Barbara and Wolf, Verena
(2011)
Formalisms for Specifying Markovian Population Models.
International Journal of Foundations of Computer Science, 22 (4).
pp. 823-841.
Datta, Anupam and Garg, Deepak and Kaynar, Dilsun Kirli and Jia, Limin and Franklin, Jason
(2011)
On Adversary Models and Compositional Security.
IEEE Security & Privacy, 9 (3).
pp. 26-32.
McConnell, Ross M and Mehlhorn, Kurt and Näher, Stefan and Schweitzer, Pascal
(2011)
Survey: Certifying Algorithms.
Computer Science Review, 5 (2).
pp. 119-161.
ISSN 1574-0137
Hammer, Christian and Snelting, Gregor
(2009)
Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs.
International Journal of Information Security, 8 (6).
pp. 399-422.
Giffhorn, Dennis and Hammer, Christian
(2009)
Precise Slicing of Concurrent Programs -- An Evaluation of Precise Slicing Algorithms for Concurrent Programs.
Journal of Automated Software Engineering, 16 (2).
pp. 197-234.
Thesis
Schwenger, Maximilian
(2020)
Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS.
Masters thesis, Saarland University.
Peter, Philip
(2012)
Autonomous UAV.
Bachelors thesis, Saarland University.
Lutz, Joachim
(2012)
Model-based Monitoring for Sensitive SCADA Systems.
Bachelors thesis, Saarland University.
Tombers, Stefan
(2011)
Low-Cost Byzantine Fault Tolerant Replication for a Cloud Environment.
Bachelors thesis, Saarland University.
Gerling, Sebastian
(2009)
Acoustic Side-Channel Attacks on Printers.
Masters thesis, Saarland University.
Hammer, Christian
(2009)
Information Flow Control for Java - A Comprehensive Approach based on Path Conditions in Dependence Graphs.
Doctoral thesis, Universit.
Book Section
Guanciale, Roberto and Baumann, Christoph and Buiras, Pablo and Dam, Mads and Nemati, Hamed
(2022)
A Case Study in Information Flow Refinement for Low Level Systems.
In:
The Logic of Software. A Tasting Menu of Formal Methods.
Springer International Publishing, pp. 54-79.
ISBN 978-3-031-08166-8
Basin, David and Cremers, Cas and Meadows, Catherine A.
(2018)
Model Checking Security Protocols.
In:
Handbook of Model Checking.
Springer International Publishing, pp. 727-762.
ISBN 978-3-319-10574-1
Eigner, Fabienne and Kate, Aniket and Maffei, Matteo and Pampaloni, Francesca and Pryvalov, Ivan
(2015)
Achieving Optimal Utility for Distributed Differential Privacy Using SMPC.
In:
UNSPECIFIED
Cryptology and Information Security Series, 13
.
IOS Press, 81 - 105.
Bichhawat, Abhishek and Rajani, Vineet and Garg, Deepak and Hammer, Christian
(2014)
Information Flow Control in WebKit's JavaScript Bytecode.
In:
Principles of Security and Trust.
Springer.
Book
Paul, Wolfgang J. and Baumann, Christoph and Lutsyk, P. and Schmaltz, Sabine and Oberhauser, J.
(2016)
System Architecture as an Ordinary Engineering Discipline.
Springer.
Bloem, Roderick and Jacobs, Swen and Khalimov, Ayrat and Konnov, Igor and Rubin, Sasha and Veith, Helmut and Widder, Josef
(2015)
Decidability of Parameterized Verification.
Synthesis Lectures on Distributed Computing Theory
.
Morgan & Claypool Publishers.
Kovalev, Mikhail and Müller, Silvia M. and Paul, Wolfgang J.
(2014)
A Pipelined Multi-core MIPS Machine -- Hardware Implementation and Correctness Proof.
UNSPECIFIED.
Monograph
Marino, Daniel and Hammer, Christian and Dolby, Julian and Vaziri, Mandana and Tip, Frank and Vitek, Jan
(2012)
Detecting Deadlock in Programs with Data-Centric Synchronization.
Technical Report.
UNSPECIFIED.
(Unpublished)
Hammer, Christian and Snelting, Gregor
(2008)
Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs.
Technical Report.
UNSPECIFIED.
(Unpublished)
Other
Frenkel, Hadar and Grumberg, Orna and Rothenberg, Bat-Chen and Sheinvald, Sarai
(2022)
Automated Program Repair Using Formal Verification Techniques.
Dimitrova, Rayna
(2021)
Reactive Synthesis Beyond Realizability (Invited Tutorial).
Schmitt, Frederik and Hahn, Christopher and Kreber, Jens U. and Rabe, Markus N. and Finkbeiner, Bernd
(2021)
Deep Learning for Temporal Logics.
(Unpublished)
Coenen, Norine and Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana
(2020)
The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective.
Vassena, Marco and Patrignani, Marco
(2020)
Memory Safety Preservation for WebAssembly.
This list was generated on Wed Nov 20 10:05:00 2024 CET.