Browse by Research Area

Up a level
Export as [feed] Atom [feed] RSS 1.0 [feed] RSS 2.0
Group by: Item Type | No Grouping
Number of items: 479.

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.
In: IEEE Symposium on Security and Privacy.
Conference: SP IEEE Symposium on Security and Privacy
(Submitted)

Cremers, Cas and Zhao, Mang
(2024) Secure Messaging with Strong Compromise Resilience, Temporal Privacy, and Immediate Decryption.
In: IEEE Symposium on Security and Privacy.
Conference: SP IEEE Symposium on Security and Privacy
(Submitted)

Heim, Philippe and Dimitrova, Rayna
(2024) Solving Infinite-State Games via Acceleration.
In: 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024).
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages
(In Press)

Lorenz, Tobias and Kwiatkowska, Marta and Fritz, Mario
(2023) Certifiers Make Neural Networks Vulnerable to Availability Attacks.
In: 16th ACM Workshop on Artificial Intelligence and Security, 30.11.2023, Copenhagen, Denmark.
Conference: AISec ACM Workshop on Artificial Intelligence and Security
(In Press)

Dewes, Rafael and Dimitrova, Rayna
(2023) Compositional High-Quality Synthesis.
In: 21st International Symposium on Automated Technology for Verification and Analysis.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis
(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.
In: USENIX Security Symposium.
Conference: USENIX-Security Usenix Security Symposium
(Submitted)

Cremers, Cas and Jacomme, Charlie and Naska, Aurora
(2023) Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations.
In: USENIX Security Symposium 2023.
Conference: USENIX-Security Usenix Security Symposium
(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.
In: USENIX 2023.
Conference: USENIX-Security Usenix Security Symposium

Beutner, Raven and Finkbeiner, Bernd and Frenkel, Hadar and Metzger, Niklas
(2023) Second-Order Hyperproperties.
In: CAV 2023, 17-22/07/23, Paris.
Conference: CAV Computer Aided Verification

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.
In: 35th International Conference on Computer Aided Verification (CAV 2023).
Conference: CAV Computer Aided Verification

Mosier, Nicholas and Eselius, Kate and Nemati, Hamed and Mitchell, John and Trippel, Caroline
(2023) Hardware-Software Codesign for Mitigating Spectre.
In: Workshop on Programming Languages for Architecture.
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation

Finkbeiner, Bernd and Frenkel, Hadar and Hofmann, Jana and Janine, Lohse
(2023) Automata-Based Software Model Checking of Hyperproperties.
In: NFM.
Conference: NFM NASA Formal Methods Symposium

Finkbeiner, Bernd and Siber, Julian
(2023) Counterfactuals Modulo Temporal Logics.
In: LPAR-23, June 4-9, 2023, Manizales, Colombia.
Conference: LPAR Logic Programming and Automated Reasoning

Bindel, Nina and Cremers, Cas and Zhao, Mang
(2023) FIDO2, CTAP 2.1, and WebAuthn 2: Provable Security and Post-Quantum Instantiation.
In: 44rd IEEE Symposium on Security and Privacy, May 22-25, 2023, San Francisco, CA, USA.
Conference: SP IEEE Symposium on Security and Privacy
(In Press)

Cosler, Matthias and Schmitt, Frederik and Hahn, Christopher and Finkbeiner, Bernd
(2023) Iterative Circuit Repair Against Formal Specifications.
In: Eleventh International Conference on Learning Representations.
Conference: ICLR International Conference on Learning Representations

Heim, Philippe and Dimitrova, Rayna
(2023) Taming Large Bounds in Synthesis from Bounded-Liveness Specifications.
In: 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems
(In Press)

Rasifard, Hamed and Gopinath, Rahul and Backes, Michael and Nemati, Hamed
(2023) SEAL: Capability-Based Access Control for Data-Analytic Scenarios.
In: ACM SACMAT 2023.
Conference: SACMAT ACM Symposium on Access Control Models and Technologies (previously ACM Workshop on Role-Based Access Control, RBAC, changed in 2000)
(In Press)

Finkbeiner, Bernd
(2023) Logics and Algorithms for Hyperproperties.
ACM SIGLOG News, 10 (2). pp. 4-23. ISSN 2372-3491

Cremers, Cas and Dax, Alexander and Naska, Aurora
(2023) Formal Analysis of SPDM: Security Protocol and Data Model version 1.2.
In: 32nd USENIX Security Symposium, 9-11 Aug 2023, Anaheim, CA, USA.
Conference: USENIX-Security Usenix Security Symposium

Frenkel, Hadar and Grumberg, Orna and Rothenberg, Bat-Chen and Sheinvald, Sarai
(2022) Automated Program Repair Using Formal Verification Techniques.
Springer, Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday
.

Finkbeiner, Bernd and Passing, Noemi
(2022) Synthesizing Dominant Strategies for Liveness.
In: 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science.
Conference: FST&TCS Foundations of Software Technology and Theoretical Computer Science
(In Press)

Steinhöfel, Dominic and Zeller, Andreas
(2022) Input Invariants.
In: Technical Track, 2022.
Conference: ESEC/FSE European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (formerly listed as ESEC)

Fabian, Xaver and Guarnieri, Marco and Patrignani, Marco
(2022) Automatic Detection of Speculative Execution Combinations.
In: CCS 2022, 7-11 Nov 2022, Los Angeles, CA, USA.
Conference: CCS ACM Conference on Computer and Communications Security
(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: ATVA 2022.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis
(In Press)

Jacobs, Swen and Sakr, Mouhammad and Völp, Marcus
(2022) Automatic Repair and Deadlock Detection for Parameterized Systems.
In: Formal Methods in Computer-Aided Design 2022.
Conference: FMCAD Formal Methods in Computer-Aided Design
(In Press)

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

Baumeister, Jan and Finkbeiner, Bernd and Gumhold, Stefan and Schledjewski, Malte
(2022) Real-time Visualization of Stream-based Monitoring Data.
In: Runtime Verification 2022.
Conference: RV International Conference on Runtime Verification (was workshop pre 2010)
(In Press)

Bacho, Renas and Loss, Julian
(2022) On the Adaptive Security of the Threshold BLS Signature Scheme.
In: ACM SIGSAC Conference on Computer and Communications Security.
Conference: CCS ACM Conference on Computer and Communications Security
(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.
In: SRDS 2022.
Conference: SRDS Symposium on Reliable Distributed Systems

Cremers, Cas and Jacomme, Charlie and Lukert, Philip
(2022) Subterm-based proof techniques for improving the automation and scope of security protocol analysis.
In: CSF 2023, July 10 - 14, 2023, Dubrovnik, Croatia.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

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.
In: MFCS 2022.
Conference: MFCS International Symposium on Mathematical Foundations of Computer Science

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.
In: MFCS 2022.
Conference: MFCS International Symposium on Mathematical Foundations of Computer Science

Cremers, Cas and Naor, Moni and Paz, Shahar and Ronen, Eyal
(2022) CHIP and CRISP: Protecting All Parties Against Compromise through Identity-Binding PAKEs.
In: CRYPTO 2022.
Conference: CRYPTO Advances in Cryptology

Tsimos, Georgios and Loss, Julian and Papamanthou, Charalampos
(2022) Gossiping for Communication-Efficient Broadcast.
In: CRYPTO 2022.
Conference: CRYPTO Advances in Cryptology
(In Press)

Ball, Marshall and Dachman-Soled, Dana and Loss, Julian
(2022) (Nondeterministic) Hardness vs. Non-Malleability.
In: CRYPTO.
Conference: CRYPTO Advances in Cryptology

Cheval, Vincent and Jacomme, Charlie and Kremer, Steve and Künnemann, Robert
(2022) SAPIC+: protocol verifiers of the world, unite!
In: USENIX Security Symposium (USENIX Security), 2022..
Conference: USENIX-Security Usenix Security Symposium
(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!
In: International Conference on Machine Learning (ICML).
Conference: ICML International Conference on Machine Learning

Finkbeiner, Bernd and Geier, Gideon and Passing, Noemi
(2022) Specification decomposition for reactive synthesis.
Innovations in Systems and Software Engineering.

Balliu, Alkida and Brandt, Sebastian and Kuhn, Fabian and Olivetti, Dennis
(2022) Distributed edge coloring in time polylogarithmic in Δ.
In: PODC 2022.
Conference: PODC ACM Symposium on Principles of Distributed Computing
(Submitted)

Lenzen, Christoph and Loss, Julian
(2022) Optimal Clock Synchronization with Signatures.
In: 2022 ACM PODC.
Conference: PODC ACM Symposium on Principles of Distributed Computing

Grunau, Christoph and Rozhoň, Václav and Brandt, Sebastian
(2022) The landscape of distributed complexities on trees and beyond.
In: PODC 2022.
Conference: PODC ACM Symposium on Principles of Distributed Computing
(Submitted)

Bensmail, Julien and Mc Inerney, Fionn
(2022) On a vertex-capturing game.
Theoretical Computer Science, 923. pp. 27-46. ISSN 0304-3975

Mosier, Nicholas and Lachnitt, Hanna and Nemati, Hamed and Trippel, Caroline
(2022) Axiomatic hardware-software contracts for security.
In: The 49th International Symposium on Computer Architecture..
Conference: ISCA ACM International Symposium on Computer Architecture

Bendrissou, Bachir and Gopinath, Rahul and Zeller, Andreas
(2022) "Synthesizing Input Grammars": A Replication Study.
In: PLDI 2022, June 2022, San Diego.
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation
(In Press)

Choi, Wonhyuk and Finkbeiner, Bernd and Piskac, Ruzica and Santolucito, Mark
(2022) Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?
In: 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation

Balliu, Alkida and Brandt, Sebastian and Kuhn, Fabian and Olivetti, Dennis
(2022) Distributed ∆-Coloring Plays Hide-and-Seek.
In: STOC 2022.
Conference: STOC ACM Symposium on Theory of Computing
(Submitted)

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

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.
In: 34th International Conference on Computer Aided Verification (CAV 22).
Conference: CAV Computer Aided Verification
(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.
In: 25th ACM International Conference on Hybrid Systems: Computation and Control.
Conference: HSCC ACM International Conference on Hybrid Systems: Computation and Control

Lenzen, Christoph and Sheikholeslami, Sahar
(2022) A Recursive Early-Stopping Phase King Protocol.
In: ACM Symposium on Principles of Distributed Computing 2022, July 25-29, 2022, Salermo, Italy.
Conference: PODC ACM Symposium on Principles of Distributed Computing
(Submitted)

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

Cremers, Cas and Fontaine, Caroline and Jacomme, Charlie
(2022) A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols.
In: 43rd IEEE Symposium on Security and Privacy..
Conference: SP IEEE Symposium on Security and Privacy

Finkbeiner, Bernd and Metzger, Niklas and Moses, Yoram
(2022) Information Flow Guided Synthesis.
In: 34th International Conference on Computer Aided Verification (CAV 22), August 7-10, 2022, Haifa, Israel.
Conference: CAV Computer Aided Verification
(Unpublished)

Beutner, Raven and Carral, David and Finkbeiner, Bernd and Hofmann, Jana and Krötzsch, Markus
(2022) Deciding Hyperproperties Combined with Functional Specifications.
In: 37th Annual ACM/IEEE Symposium on Logic in Computer Science.
Conference: LICS IEEE Symposium on Logic in Computer Science
(In Press)

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

Finkbeiner, Bernd and Heim, Philippe and Passing, Noemi
(2022) Temporal Stream Logic modulo Theories.
In: ETAPS 2022, Apr 2022, Munich.
Conference: FOSSACS Foundations of Software Science and Computational Structures

Mohtashami, Amirkeivan and Jaggi, Martin and Stich, Sebastian U.
(2022) Masked Training of Neural Networks with Partial Gradients.
In: AISTATS 2022, 28 Mar - 30 Mar 2022, online.
Conference: AISTATS International Conference on Artificial Intelligence and Statistics
(In Press)

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)

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.
In: 30th EACSL Annual Conference on Computer Science Logic (CSL 2022).
Conference: CSL Annual Conference on Computer Science Logic

Fisman, Dana and Frenkel, Hadar and Zilles, Sandra
(2022) Inferring Symbolic Automata.
In: CSL.
Conference: CSL Annual Conference on Computer Science Logic

Kruse, Matthis and Patrignani, Marco
(2022) Composing Secure Compilers.
In: ACM SIGPLAN Workshop on Principles of Secure Compilation, 2022, Sun 16 - Fri 28 January 2022, Philadelphia, Pennsylvania, United States.
Conference: PriSC Workshop on Principles of Secure Compilation

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

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

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.
In: 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science.
Conference: FST&TCS Foundations of Software Technology and Theoretical Computer Science

Fabian, Xaver and Chan, Koby and Patrignani, Marco
(2021) Formal Verification of Spectres Combination.
In: PLAS 2021, 7 Dec 2021, Online.
Conference: PLAS Workshop on Programming Languages and Analysis for Security

Abdalla, Michel and Barbosa, Manuel and Katz, Jonathan and Loss, Julian and Xu, Jiayu
(2021) Algebraic Adversaries in the Universal Composability Framework.
In: 27th Annual International Conference on the Theory and Application of Cryptology and Information Security.
Conference: ASIACRYPT International Conference on the Theory and Application of Cryptology and Information Security

Katz, Jonathan and Loss, Julian and Rosenberg, Michael
(2021) Boosting the Security of Blind Signature Schemes.
In: 27th Annual International Conference on the Theory and Application of Cryptology and Information Security.
Conference: ASIACRYPT International Conference on the Theory and Application of Cryptology and Information Security

Schmitt, Frederik and Hahn, Christopher and Rabe, Markus N. and Finkbeiner, Bernd
(2021) Neural Circuit Synthesis from Specification Patterns.
In: Thirty-fifth Conference on Neural Information Processing Systems.
Conference: NeurIPS Conference on Neural Information Processing Systems

Blum, Erica and Katz, Jonathan and Loss, Julian
(2021) Tardigrade: An Atomic Broadcast Protocol for Arbitrary Network Conditions.
In: 27th Annual International Conference on the Theory and Application of Cryptology and Information Security.
Conference: ASIACRYPT International Conference on the Theory and Application of Cryptology and Information Security

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

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.
In: IEEE VIS 2021.
Conference: IEEE VIS IEEE Visualization

Finkbeiner, Bernd and Passing, Noemi
(2021) Compositional Synthesis of Modular Systems.
In: 19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021).
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis
(In Press)

Coenen, Norine and Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana and Schillo, Yannick
(2021) Runtime Enforcement of Hyperproperties.
In: ATVA 2021.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Finkbeiner, Bernd and Klein, Felix and Metzger, Niklas
(2021) Live Synthesis.
In: 19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021), 18 - 22 October 2021, Golden Coast, Australia.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Patrignani, Marco and Guarnieri, Marco
(2021) Exorcising Spectres with secure compilers.
In: ACM CCS 2021.
Conference: CCS ACM Conference on Computer and Communications Security

Dauer, Johann C. and Finkbeiner, Bernd and Schirmer, Sebastian
(2021) Monitoring with Verified Guarantees.
In: Runtime Verification - 21st International Conference, RV 2021, Virtual Event, October 11-14, 2021, Proceedings.
Conference: RV International Conference on Runtime Verification (was workshop pre 2010)

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: OOPSLA 2021.
Conference: OOPSLA ACM Conference on Object Oriented Programming Systems Languages and Applications
(In Press)

Dimitrova, Rayna
(2021) Reactive Synthesis Beyond Realizability (Invited Tutorial).
UNSPECIFIED, Conference Series: Formal Methods in Computer-Aided Design
.

Lorenz, Tobias and Ruoss, Anian and Balunović, Mislav and Singh, Gagandeep and Vechev, Martin
(2021) Robustness Certification for Point Cloud Models.
In: IEEE International Conference on Computer Vision (ICCV), 2021, Virtual.
Conference: ICCV IEEE International Conference on Computer Vision
(In Press)

Schmitt, Frederik and Hahn, Christopher and Kreber, Jens U. and Rabe, Markus N. and Finkbeiner, Bernd
(2021) Deep Learning for Temporal Logics.
Unpublished
.
(Unpublished)

Cremers, Cas and Hale, Britta and Kohbrok, Konrad
(2021) The Complexities of Healing in Secure Group Messaging: Why {Cross-Group} Effects Matter.
In: 30th USENIX Security Symposium (USENIX Security 21).
Conference: USENIX-Security Usenix Security Symposium

Beutner, Raven and Finkbeiner, Bernd
(2021) A Temporal Logic for Strategic Hyperproperties.
In: 32nd International Conference on Concurrency Theory, CONCUR 2021.
Conference: CONCUR International Conference on Concurrency Theory

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

Baier, Christel and Coenen, Norine and Finkbeiner, Bernd and Funke, Florian and Jantsch, Simon and Siber, Julian
(2021) Causality-Based Game Solving.
In: 33rd International Conference, CAV 2021, July 20–23, 2021, Virtual Event.
Conference: CAV Computer Aided Verification

Baumeister, Jan and Coenen, Norine and Bonakdarpour, Borzoo and Finkbeiner, Bernd and Sánchez, César
(2021) A Temporal Logic for Asynchronous Hyperproperties.
In: CAV 2021, July 20–23, 2021, Virtual Event.
Conference: CAV Computer Aided Verification

Jacobs, Swen and Sakr, Mouhammad
(2021) AIGEN: Random Generation of Symbolic Transition Systems.
In: 33rd International Conference on Computer-Aided Verification.
Conference: CAV Computer Aided Verification
(In Press)

Künnemann, Robert and Garg, Deepak and Backes, Michael
(2021) Accountability in the Decentralised-Adversary Setting.
In: CSF 2021.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)
(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.
In: 34th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Dax, Alexander and Künnemann, Robert
(2021) On the Soundness of Infrastructure Adversaries.
In: 34th IEEE Computer Security Foundations Symposium, 21-25 June 2021, Virtual Conference.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Bensmail, Julien and Fioravantes, Foivos and Mc Inerney, Fionn and Nisse, Nicolas
(2021) The Largest Connected Subgraph Game.
In: WG 2021.
Conference: WG International Workshop on Graph-Theoretic Concepts in Computer Science

Beutner, Raven and Ong, Luke
(2021) On Probabilistic Termination of Functional Programs with Continuous Distributions.
In: 42nd International Conference on Programming Language Design and Implementation.
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation

Morio, Kevin and Künnemann, Robert
(2021) Verifying Accountability for Unbounded Sets of Participants.
In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), Jun 21 2021 to Jun 25 2021, Online.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Finkbeiner, Bernd and Geier, Gideon and Passing, Noemi
(2021) Specification Decomposition for Reactive Synthesis.
In: 13th NASA Formal Methods Symposium, NFM 2021.
Conference: NFM NASA Formal Methods Symposium
(In Press)

Finkbeiner, Bernd and Keller, Andreas and Schmidt, Jessica and Schwenger, Maximilian
(2021) Robust Monitoring for Medical Cyber-Physical Systems.
In: 11th Workshop on Medical Cyber Physical Systems and Internet of Medical Things.
Conference: MCPS Medical Cyber Physical Systems and Internet of Medical Things Workshop

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: 42nd IEEE Symposium on Security and Privacy (S&P'21).
Conference: SP IEEE Symposium on Security and Privacy
(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.
In: 42nd IEEE Symposium on Security and Privacy (S&P'21), May 24-28, Virtual.
Conference: SP IEEE Symposium on Security and Privacy

Brendel, Jacqueline and Cremers, Cas and Jackson, Dennis and Zhao, Mang
(2021) The Provable Security of Ed25519: Theory and Practice.
In: S&P 2021.
Conference: SP IEEE Symposium on Security and Privacy
(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: S&P 2021.
Conference: SP IEEE Symposium on Security and Privacy
(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.
In: The Ninth International Conference on Learning Representations.
Conference: ICLR International Conference on Learning Representations

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.
In: 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2021.
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

Gieseking, Manuel and Hecking-Harbusch, Jesko and Yanich, Ann
(2021) A Web Interface for Petri Nets with Transits and Petri Games.
In: TACAS: Tools and Algorithms for the Construction and Analysis of Systems.
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

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.
In: 48th ACM SIGPLAN Symposium on Principles of Programming Languages.
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages

Finkbeiner, Bernd
(2021) Model Checking Algorithms for Hyperproperties (Invited Paper).
In: Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings.
Conference: VMCAI Verification, Model Checking and Abstract Interpretation

Finkbeiner, Bernd and Passing, Noemi
(2020) Dependency-based Compositional Synthesis.
In: 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-Rüdiger
(2020) Model Checking Branching Properties on Petri Nets with Transits.
In: Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Dimitrova, Rayna and Finkbeiner, Bernd and Torfah, Hazem
(2020) Probabilistic Hyperproperties of Markov Decision Processes.
In: 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Schwenger, Maximilian
(2020) Monitoring Cyber-Physical Systems: From Design to Integration.
In: RV 2020.
Conference: RV International Conference on Runtime Verification (was workshop pre 2010)

Finkbeiner, Bernd and Oswald, Stefan and Passing, Noemi and Schwenger, Maximilian
(2020) Verified Rust Monitors for Lola Specifications.
In: RV 2020.
Conference: RV International Conference on Runtime Verification (was workshop pre 2010)

Baumeister, Tom and Finkbeiner, Bernd and Torfah, Hazem
(2020) Explainable Reactive Synthesis.
In: Automated Technology for Verification and Analysis.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Morio, Kevin and Jackson, Dennis and Vassena, Marco and Künnemann, Robert
(2020) Modular Black-box Runtime Verification of Security Protocols.
In: PLAS 2020.
Conference: PLAS Workshop on Programming Languages and Analysis for Security

Tran, Nicolas and Speicher, Patrick and Künnemann, Robert and Backes, Michael and Torralba, Àlvaro and Hoffmann, Jörg
(2020) Planning in the Browser.
In: System Demonstration at the 30th International Conference on Automated Planning and Scheduling (ICAPS'20), October 2020.
Conference: ICAPS International Conference on Automated Planning and Scheduling

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)

Coenen, Norine and Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana
(2020) The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective.
UNSPECIFIED, International Conference on Principles of Knowledge Representation and Reasoning (KR)
.

Schwenger, Maximilian
(2020) Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS.
Masters thesis, Saarland University.

Künnemann, Robert and Nemati, Hamed
(2020) MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation.
In: Computer Security - ESORICS 2020 - 25th European Symposium on Research in Computer Security, ESORICS 2020, Guildford, UK, September 14-18, 2020, Proceedings, Part II.
Conference: ESORICS European Symposium On Research In Computer Security

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: SAC 2020, Oct 19-23, 2020.
Conference: SAC Selected Areas in Cryptography
(In Press)

Baumeister, Jan and Finkbeiner, Bernd and Kruse, Matthis and Schwenger, Maximilian
(2020) Automatic Optimizations for Stream-based Monitoring Languages.
In: 20th International Conference on Runtime Verification, 06-09 October 2020.
Conference: RV International Conference on Runtime Verification (was workshop pre 2010)
(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.
In: 29th USENIX Security Symposium (USENIX Security 20), August 12–14, 2020.
Conference: USENIX-Security Usenix Security Symposium

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.
In: 33rd IEEE Computer Security Foundations Symposium, June 22-25, 2020.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

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.
In: 29th USENIX Security Symposium (USENIX Security 20), August 12–14, 2020.
Conference: USENIX-Security Usenix Security Symposium

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

Nemati, Hamed and Buiras, Pablo and Lindner, Andreas and Guanciale, Roberto and Jacobs, Swen
(2020) Validation of Abstract Side-Channel Models for Computer Architectures.
In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I.
Conference: CAV Computer Aided Verification

Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana and Tentrup, Leander
(2020) Realizing Omega-regular Hyperproperties.
In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, 21.07.2020 - 24.07.2020, Los Angeles.
Conference: CAV Computer Aided Verification

Cremers, Cas and Fairoze, Jaiden and Kiesl, Benjamin and Naska, Aurora
(2020) Clone Detection in Secure Messaging: Improving Post-Compromise Security in Practice.
In: CCS 2020, November 09-13, 2020.
Conference: CCS ACM Conference on Computer and Communications Security
(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: CAV 2020.
Conference: CAV Computer Aided Verification
(In Press)

Cortiñas, Carlos Tomé and Vassena, Marco and Russo, Alejandro
(2020) Securing Asynchronous Exceptions.
In: Computer Security Foundations Symposium, Hobuken, NJ.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Bonakdarpour, B. and Finkbeiner, B.
(2020) Controller Synthesis for Hyperproperties.
In: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

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.

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.
In: HSCC 2020, April 21-14 2020, Sydney, Australia.
Conference: HSCC ACM International Conference on Hybrid Systems: Computation and Control

Frenkel, Hadar and Grumberg, Orna and Pasareanu, Corina and Sheinvald, Sarai
(2020) Assume, Guarantee or Repair.
In: TACAS 2020.
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

Finkbeiner, Bernd and Schmidt, Jessica and Schwenger, Maximilian
(2020) Simplex Architecture Meets RTLola.
In: 5th Workshop on Monitoring and Testing of Cyber-Physical Systems, April 13-22 2020, Sydney.
Conference: MT-CPS WORKSHOP ON MONITORING AND TESTING OF CYBER-PHYSICAL SYSTEMS

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

Groß, Joschka and Torralba, Àlvaro and Fickert, Maximilian
(2020) Novel Is Not Always Better:On the Relation between Novelty and Dominance Pruning.
In: AAAI 2020.
Conference: AAAI National Conference of the American Association for Artificial Intelligence

Vassena, Marco and Patrignani, Marco
(2020) Memory Safety Preservation for WebAssembly.
UNSPECIFIED
.

Jacobs, Swen and Sakr, Mouhammad and Zimmermann, Martin
(2020) Promptness and Bounded Fairness in Concurrent and Parameterized Systems.
In: VMCAI 2020.
Conference: VMCAI Verification, Model Checking and Abstract Interpretation
(In Press)

Seidl, Helmut and Müller, Christian and Finkbeiner, Bernd
(2020) How to Win First-Order Safety Games.
In: Verification, Model Checking, and Abstract Interpretation.
Conference: VMCAI Verification, Model Checking and Abstract Interpretation

Patrignani, Marco and Wahby, Riad S. and Künnemann, Robert
(2020) Universal Composability is Secure Compilation.
In: PriSC 2020 - co-located with POPL.
Conference: PriSC Workshop on Principles of 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.
In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II.
Conference: CAV Computer Aided Verification

Baumeister, Jan and Finkbeiner, Bernd and Schirmer, Sebastian and Schwenger, Maximilian and Torens, Christoph
(2020) RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft.
In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II.
Conference: CAV Computer Aided Verification

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

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: 26th ACM Conference on Computer and Communications Security, November 11th-15th, 2019, London, UK.
Conference: CCS ACM Conference on Computer and Communications Security
(In Press)

Jacobs, Swen and Sakr, Mouhammad
(2019) A symbolic algorithm for lazy synthesis of eager strategies.
Acta Informatica. ISSN 1432-0525

Bloem, Roderick and Jacobs, Swen and Vizel, Yakir
(2019) Efficient Information-Flow Verification under Speculative Execution.
In: ATVA 2019, International Symposium on Automated Technology for Verification and Analysis, 27-31 Oct 2019, Taipei City, Taiwan.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis
(In Press)

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.

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: 39th International Cryptology Conference (CRYPTO 2019), August 18-22, 2019, Santa Barbara.
Conference: CRYPTO Advances in Cryptology
(In Press)

Beutner, Raven and Finkbeiner, Bernd and Hecking-Harbusch, Jesko
(2019) Translating Asynchronous Games for Distributed Synthesis.
In: 30th International Conference on Concurrency Theory, CONCUR 2019.
Conference: CONCUR International Conference on Concurrency Theory

Cremers, Cas and Jackson, Dennis
(2019) Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman.
In: 32nd IEEE Computer Security Foundations Symposium, June 25-28, 2019, Hoboken, NJ, USA.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Cremers, Cas and Hirschi, Lucca
(2019) Improving Automated Symbolic Analysis of Ballot Secrecy for E-voting Protocols: A Method Based on Sufficient Conditions.
In: 4th IEEE European Symposium on Security and Privacy, June 17-19, 2019, Stockholm.
Conference: EuroS&P IEEE European Symposium on Security and Privacy

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.
In: csf.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Patrignani, Marco and Garg, Deepak
(2019) Robustly Safe Compilation.
In: ESOP.
Conference: ESOP European Symposium on Programming

Faymonville, Peter and Finkbeiner, Bernd and Schledjewski, Malte and Schwenger, Maximilian and Tentrup, Leander and Torfah, Hazem
(2019) Real-time Stream Monitoring with StreamLAB.
In: 4th Workshop on Monitoring and Testing of Cyber-Physical Systems.
Conference: MT-CPS WORKSHOP ON MONITORING AND TESTING OF CYBER-PHYSICAL SYSTEMS

Heule, Marijn J.H. and Kiesl, Benjamin and Biere, Armin
(2019) Encoding Redundancy for Satisfaction-Driven Clause Learning.
In: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019).
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

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.

Cremers, Cas and Dehnel-Wild, Martin
(2019) Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion.
In: Network and Distributed Systems Security (NDSS) Symposium 2019, 24-27 February 2019, San Diego, CA, USA.
Conference: NDSS Network and Distributed System Security Symposium
(In Press)

Dimitrova, Rayna and Finkbeiner, Bernd and Torfah, Hazem
(2019) Approximate Automata for Omega-Regular Languages.
In: Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Künnemann, Robert and Esiyok, Ilkan and Backes, Michael
(2019) Automated Verification of Accountability in Security Protocols.
In: Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)
(In Press)

Steinmetz, Marcel and Torralba, Àlvaro
(2019) Bridging the Gap Between Abstractions and Critical-Path Heuristics via Hypergraphs.
In: Proceedings of the 29th International Conference on Automated Planning and Scheduling (ICAPS'19), Berkeley, CA, USA, 2019..
Conference: ICAPS International Conference on Automated Planning and Scheduling

Finkbeiner, Bernd and Haas, Lennart and Torfah, Hazem
(2019) Canonical Representations of k-Safety Hyperproperties.
In: IEEE Computer Security Foundations Symposium, CSF.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Künnemann, Robert and Garg, Deepak and Backes, Michael
(2019) Causality & Control flow.
In: 4th Workshop on Formal Reasoning about Causation, Responsibility, & Explanations in Science & Technology.
Conference: CREST Workshop on Formal Reasoning about Causation, Responsibility, & Explanations in Science & Technology
(In Press)

Hecking-Harbusch, Jesko and Metzger, Niklas
(2019) Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems.
In: UNSPECIFIED.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Coenen, Norine and Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana
(2019) The Hierarchy of Hyperlogics.
In: IEEE Symposium on Logic in Computer Science, LICS.
Conference: LICS IEEE Symposium on Logic in Computer Science

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: Computer Security Foundations Symposium, Hobuken, NJ.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)
(In Press)

Backes, Michael and Hanzlik, Lucjan and Schneider-Bensch, Jonas
(2019) Membership Privacy for Fully Dynamic Group Signatures.
In: ACM CCS 2019.
Conference: CCS ACM Conference on Computer and Communications Security

Finkbeiner, Bernd and Gieseking, Manuel and Olderog, Ernst-Rüdiger and Hecking-Harbusch, Jesko
(2019) Model Checking Data Flows in Concurrent Network Updates.
In: Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Finkbeiner, Bernd and Hahn, Christopher and Stenger, Marvin and Tentrup, Leander
(2019) Monitoring hyperproperties.
Formal Methods Syst. Des., 54 (3). pp. 336-363.

Bonakdarpour, Borzoo and Finkbeiner, Bernd
(2019) Program Repair for Hyperproperties.
In: Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Kiesl, Benjamin and Seidl, Martina
(2019) QRAT Polynomially Simulates \forall-Exp+Res.
In: International Conference on Theory and Applications of Satisfiability Testing, July 7 - 12, Lisbon.
Conference: SAT International Conference on Theory and Applications of Satisfiability Testing
(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.
In: Computer Aided Verification - 31th International Conference, CAV.
Conference: CAV Computer Aided Verification

Dimitrova, Rayna and Finkbeiner, Bernd and Torfah, Hazem
(2019) Synthesizing Approximate Implementations for Unrealizable Specifications.
In: Computer Aided Verification - 31th International Conference, CAV.
Conference: CAV Computer Aided Verification

Finkbeiner, Bernd and Klein, Felix and Piskac, Ruzica and Santolucito, Mark
(2019) Synthesizing functional reactive programs.
In: Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP.
Conference: HASKELL Haskell Workshop

Geier, Gideon and Heim, Philippe and Klein, Felix and Finkbeiner, Bernd
(2019) Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications.
In: Formal Methods in Computer Aided Design, FMCAD.
Conference: FMCAD Formal Methods in Computer-Aided Design

Finkbeiner, Bernd and Klein, Felix and Piskac, Ruzica and Santolucito, Mark
(2019) Temporal Stream Logic: Synthesis beyond the Bools.
In: Computer Aided Verification - 31th International Conference, CAV.
Conference: CAV Computer Aided Verification

Kiesl, Benjamin and Heule, Marijn J.H. and Biere, Armin
(2019) Truth Assignments as Conditional Autarkies.
In: 17th International Symposium on Automated Technology for Verification and Analysis.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Coenen, Norine and Finkbeiner, Bernd and Sanchez, Cesar and Tentrup, Leander
(2019) Verifying Hyperliveness.
In: Computer Aided Verification - 31th International Conference, CAV.
Conference: CAV Computer Aided Verification

Mirzaie, Nahal and Faghih, Fathiyeh and Jacobs, Swen and Bonakdarpour, Borzoo
(2018) Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings.
In: 22nd International Conference on Principles of Distributed Systems, OPODIS 2018, December 17-19, 2018, Hong Kong, China.
Conference: OPODIS International Conference on Principles of Distributed Systems

Jacobs, Swen and Sakr, Mouhammad
(2018) A Symbolic Algorithm for Lazy Synthesis of Eager Strategies.
In: International Symposium on Automated Technology for Verification and Analysis (ATVA), October 7-10, 2018, Los Angeles.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis
(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.
In: IFIP/IEEE International Conference on Very Large Scale Integration, VLSI-SoC 2018, Verona, Italy, October 8-10, 2018, 8-10 Oct 2018, Verona, Italy.

Jacobs, Swen and Tentrup, Leander and Zimmermann, Martin
(2018) Distributed synthesis for parameterized temporal logics.
Information and Computation, 262 (2). pp. 311-328.

Bonakdarpour, B. and Finkbeiner, Bernd
(2018) The Complexity of Monitoring Hyperproperties.
In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

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.
In: ACM CCS 2018, 15-19 Oct 2018, Toronto, Canada.
Conference: CCS ACM Conference on Computer and Communications Security

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)

Jacobs, Swen and Sakr, Mouhammad
(2018) Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity.
In: Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Proceedings.
Conference: VMCAI Verification, Model Checking and Abstract Interpretation

Thanh Nguyen, Binh and Sprenger, Christoph and Cremers, Cas
(2018) Abstractions for security protocol verification.
Journal of Computer Security.
(In Press)

Gerstacker, Carsten and Klein, Felix and Finkbeiner, Bernd
(2018) Bounded Synthesis of Reactive Programs.
In: Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

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.

Finkbeiner, Bernd and Hahn, Christopher and Hans, Tobias
(2018) MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \exists* \forall* Fragment.
In: Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Finkbeiner, Bernd and Hahn, Christopher and Torfah, Hazem
(2018) Model Checking Quantitative Hyperproperties.
In: Computer Aided Verification.
Conference: CAV Computer Aided Verification

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

Finkbeiner, Bernd and Hahn, Christopher and Stenger, Marvin and Tentrup, Leander
(2018) RVHyper: A Runtime Verification Tool for Temporal Hyperproperties.
In: Tools and Algorithms for the Construction and Analysis of Systems.
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

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.
In: 39th IEEE Symposium on Security and Privacy (SP '18).
Conference: SP IEEE Symposium on Security and Privacy

Backes, Michael and Hanzlik, Lucjan and Kluczniak, Kamil and Schneider, Jonas
(2018) Signatures with Flexible Public Key: Introducing Equivalence Classes for Public Keys.
In: IACR ASIACRYPT 2018.
Conference: ASIACRYPT International Conference on the Theory and Application of Cryptology and Information Security
(In Press)

Finkbeiner, Bernd and Hahn, Christopher and Lukert, Philip and Stenger, Marvin and Tentrup, Leander
(2018) Synthesizing Reactive Systems from Hyperproperties.
In: Computer Aided Verification.
Conference: CAV Computer Aided Verification

Giechaskiel, Ilias and Cremers, Cas and Rasmussen, Kasper B.
(2018) When the Crypto in Cryptocurrencies Breaks: Bitcoin Security under Broken Primitives.
IEEE Security & Privacy.

Devriese, Dominique and Patrignani, Marco and Piessens, Frank
(2017) Parametricity Versus the Universal Type.
In: POPL.

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).
In: 1st Workshop on Principles of Secure Compilation.

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.
In: Proceedings of the 2nd IEEE European Symposium on Security and Privacy (Euro S&P '17).
Conference: EuroS&P IEEE European Symposium on Security and Privacy

Malavolta, Giulio and Moreno-Sanchez, Pedro and Kate, Aniket and Maffei, Matteo
(2017) SilentWhispers: Enforcing Security and Privacy in Decentralized Credit Networks.
In: Proceedings of the 24th Annual Symposium on Network and Distributed System Security (NDSS '17).
Conference: NDSS Network and Distributed System Security Symposium

Çiçek, Ezgi and Barthe, Gilles and Gaboardi, Marco and Garg, Deepak and Hoffmann, Jan
(2017) Relational cost analysis.
In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17).
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages

Canones, Pablo and Köpf, Boris and Reineke, Jan
(2017) Security Analysis of Cache Replacement Policies.
In: Proceedings of the 6th International Conference on Principles of Security and Trust.

Hoenicke, Jochen and Majumdar, Rupak and Podelski, Andreas
(2017) Thread modularity at many levels: a pearl in compositional verification.
In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17).
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages

Kang, Jeehoon and Hur, Chung-Kil and Lahav, Ori and Vafeiadis, Viktor and Dreyer, Derek
(2017) A promising semantics for relaxed-memory concurrency.
In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17).
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages

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.
In: Proceedings Sixth Workshop on Synthesis, SYNT 2017, Heidelberg, Germany, 22nd July 2017..

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.

Cohn-Gordon, Katriel and Cremers, Cas and Dowling, Benjamin and Stebila, Douglas
(2017) A Formal Security Analysis of the Signal Messaging Protocol.
In: 2nd IEEE European Symposium on Security and Privacy.
Conference: EuroS&P IEEE European Symposium on Security and Privacy

Mehta, Aastha and Elnikety, Eslam and Harvey, Katura and Garg, Deepak and Druschel, Peter
(2017) Qapla: Policy compliance for database-backed systems.
In: 26th USENIX Security Symposium (USENIX Security 17).
Conference: USENIX-Security Usenix Security Symposium

Swasey, David and Garg, Deepak and Dreyer, Derek
(2017) Robust and compositional verification of object capability patterns.
OOPSLA, 1. 89:1–89:26.

Cremers, Cas and Dehnel-Wild, Martin and Milner, Kevin
(2017) Secure Authentication in the Grid: A Formal Analysis of DNP3: SAv5.
In: 22nd European Symposium on Research in Computer Security (ESORICS 2017).
Conference: ESORICS European Symposium On Research In Computer Security

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.

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.
In: Proceedings of the 3rd International Workshop on Genome Privacy and Security (GenoPri'16).

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.
In: Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI '16).
Conference: OSDI Usenix Symposium on Operating Systems Design and Implementation

Backes, Michael and Künnemann, Robert and Mohammadi, Esfandiar
(2016) Computational Soundness for Dalvik Bytecode.
In: Proceedings of the 23rd ACM Conference on Computer and Communications Security (CCS'16).
Conference: CCS ACM Conference on Computer and Communications Security

Garg, Deepak and Cheney, James and Perera, Roly
(2016) Causally Consistent Dynamic Slicing.
In: Proceedings of the 27th International Conference on Concurrency Theory (CONCUR '16).
Conference: CONCUR International Conference on Concurrency Theory

Elnikety, Eslam and Mehta, Aastha and Vahldiek-Oberwanger, Anjo and Garg, Deepak and Druschel, Peter
(2016) T3: Comprehensive policy compliance in data retrieval systems.
In: Proceedings of the 25th USENIX Security Symposium (USENIX Security '16).
Conference: USENIX-Security Usenix Security Symposium

Elnikety, Eslam and Mehta, Aastha and Vahldiek-Oberwanger, Anjo and Garg, Deepak and Druschel, Peter
(2016) Thoth: Comprehensive Policy Compliance in Data Retrieval Systems.
In: Proceedings of the 25th USENIX Security Symposium (USENIX Security '16).
Conference: USENIX-Security Usenix Security Symposium

Maffei, Matteo and Grimm, Niklas and Focardi, Riccardo and Calzavara, Stefano
(2016) Micro-Policies for Web Session Security.
In: Proceedings of the 29th Computer Security Foundations Symposium 2016 (CSF '16).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Garg, Deepak and Rezk, Tamara and Rajani, Vineet
(2016) On Access Control, Capabilities, Their Equivalence, and Confused Deputy Attacks.
In: Proceedings of the 29th Computer Security Foundations Symposium 2016 (CSF '16).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Garg, Deepak and Rafnsson, Willard and Sabelfeld, Andrei
(2016) Progress-Sensitive Security for SPARK.
In: Proceedings of the International Symposium on Engineering Secure Software and Systems (ESSoS '16).

Garg, Deepak and Bolosteanu, Iulia
(2016) Asymmetric Secure Multi-execution with Declassification.
In: Proceedings of Principles of Security and Trust - 5th International Conference (POST '16).

Grishchenko, Ilya and Maffei, Matteo and Calzavara, Stefano
(2016) HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving.
In: Proceedings of the 1st IEEE European Symposium on Security and Privacy (Euro S&P '16).
Conference: EuroS&P IEEE European Symposium on Security and Privacy

Chistikov, Dmitry and Majumdar, Rupak and Niksic, Filip
(2016) Hitting Families of Schedules for Asynchronous Programs.
In: Proc. of the 28th International Conference on Computer Aided Verification (CAV 2016).
Conference: CAV Computer Aided Verification

Kang, Jeehoon and Kim, Yoonseung and Hur, Chung-Kil and Dreyer, Derek and Vafeiadis, Viktor
(2016) Lightweight verification of separate compilation.
In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'16).
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages

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.
In: Proceedings of the 53rd Annual Design Automation Conference, DAC 2016, Austin, TX, USA, June 5-9, 2016.

Esparza, Javier and Ganty, Pierre and Leroux, Jérôme and Majumdar, Rupak
(2016) Model Checking Population Protocols.
In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India.

Maiya, Pallavi and Gupta, Rahul and Kanade, Aditya and Majumdar, Rupak
(2016) Partial Order Reduction for Event-Driven Multi-threaded Programs.
In: Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16).
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

Dimitrova, Rayna and Fioriti, Luis María Ferrer and Hermanns, Holger and Majumdar, Rupak
(2016) Probabilistic CTL*: The Deductive Way.
In: Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16).
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

Bonakdarpour, Borzoo and Finkbeiner, Bernd
(2016) Runtime Verification for HyperLTL.
In: Proceedings of the 16th International Conference on Runtime Verification (RV'2016).

Soudjani, Sadegh Esmaeil Zadeh and Majumdar, Rupak and Abate, Alessandro
(2016) Safety Verification of Continuous-Space Pure Jump Markov Processes.
In: Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16).
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

Maffei, Matteo
(2016) Security & Privacy Column.
SIGLOG News.

Finkbeiner, Bernd and Seidl, Helmut and Müller, Christian
(2016) Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents.
In: Proc. of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016).
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Faymonville, Peter and Finkbeiner, Bernd and Schirmer, Sebastian and Torfah, Hazem
(2016) A Stream-Based Specification Language for Network Monitoring.
In: Proceedings of the 16th International Conference on Runtime Verification (RV'2016).

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.

Deininger, David and Dimitrova, Rayna and Majumdar, Rupak
(2016) Symbolic Model Checking for Factored Probabilistic Models.
In: Proc. of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016).
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Paul, Wolfgang J. and Baumann, Christoph and Lutsyk, P. and Schmaltz, Sabine and Oberhauser, J.
(2016) System Architecture as an Ordinary Engineering Discipline.
Springer.

Lahav, Ori and Giannarakis, Nick and Vafeiadis, Viktor
(2016) Taming release-acquire consistency.
In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'16).
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages

Damm, Werner and Finkbeiner, Bernd and Rakow, Astrid
(2016) What You Really Need To Know About Your Neighbor.
In: Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016.
Conference: CAV Computer Aided Verification

Garg, Deepak and Çiçek, Ezgi and Paraskevopoulou, Zoe
(2016) A type theory for incremental computational complexity with control flow changes.
In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP '16).
Conference: ICFP International Conference on Functional Programming

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.
In: Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016..

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.

Jacobs, Swen and Tentrup, Leander and Zimmermann, Martin
(2016) Distributed PROMPT-LTL Synthesis.
In: Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016..

Jacobs, Swen and Klein, Felix and Schirmer, Sebastian
(2016) A High-Level LTL Synthesis Format: TLSF v1.1.
In: Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016..

Jacobs, Swen and Bloem, Roderick
(2016) The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond.
In: Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016..

Bloem, Roderick and Braud-Santoni, Nicolas and Jacobs, Swen
(2016) Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems.
In: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I.
Conference: CAV Computer Aided Verification

Außerlechner, Simon and Jacobs, Swen and Khalimov, Ayrat
(2016) Tight Cutoffs for Guarded Protocols with Fairness.
In: Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings.

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.
In: Proceedings of the 22nd ACM conference on Computer and communications security (ACM CCS 2015).
Conference: CCS ACM Conference on Computer and Communications Security

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.

Bichhawat, Abhishek and Hammer, Christian and Garg, Deepak and Rajani, Vineet
(2015) Information Flow Control for Event Handling and the DOM in Web Browsers.
In: Proceedings of the 28th Computer Security Foundations Symposium (CSF '15).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Datta, Anupam and Garg, Deepak and Jia, Limin and Sen, Shayak
(2015) A Logic of Programs with Interface-Confined Code.
In: Proceedings of the 28th Computer Security Foundations Symposium (CSF '15).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

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.
In: Proceedings of the 28th Computer Security Foundations Symposium (CSF '15).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

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.
In: Proceedings of the 10th European Conference on Computer Systems (EuroSys '15).
Conference: EuroSys Eurosys Conference

Garg, Deepak and Çiçek, Ezgi and Acar, Umut A.
(2015) Refinement Types for Incremental Computational Complexity.
In: Proceedings of the 24th European Symposium on Programming (ESOP '15).
Conference: ESOP European Symposium on Programming

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).

Moreno-Sanchez, Pedro and Kate, Aniket and Maffei, Matteo and Pecina, Kim
(2015) Privacy Preserving Payments in Credit Networks.
In: Proceedings of the 22nd Annual Network and Distributed System Security Symposium (NDSS '15).
Conference: NDSS Network and Distributed System Security Symposium

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.

Finkbeiner, Bernd and Gieseking, Manuel and Olderog, Ernst-Rüdiger
(2015) Adam: Causality-Based Synthesis of Distributed Systems.
In: Proc. of the 27th International Conference on Computer Aided Verification (CAV 2015).
Conference: CAV Computer Aided Verification

Finkbeiner, Bernd and Rabe, Markus N. and Sanchez, Cesar
(2015) Algorithms for Model Checking HyperLTL and HyperCTL ^*.
In: Proc. of the 27th International Conference on Computer Aided Verification (CAV 2015).
Conference: CAV Computer Aided Verification

Chistikov, Dmitry and Dimitrova, Rayna and Majumdar, Rupak
(2015) Approximate Counting in SMT and Value Estimation for Probabilistic Programs.
In: Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 15).
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

Kloos, Johannes and Majumdar, Rupak and Vafeiadis, Viktor
(2015) Asynchronous Liquid Separation Types.
In: Proceedings of the 29th European Conference on Object-Oriented Programming (ECOOP'16).
Conference: ECOOP European Conference on Object-Oriented Programming

Majumdar, Rupak and Wang, Zilong
(2015) Bbs: A Phase-Bounded Model Checker for Asynchronous Programs.
In: Proc. of the 27th International Conference on Computer Aided Verification (CAV 2015).
Conference: CAV Computer Aided Verification

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.

Backes, Michael and Mohammadi, Esfandiar and Ruffing, Tim
(2015) Computational Soundness for Interactive Primitves.
In: Proceedings of the 20th European Symposium on Research in Computer Security (ESORICS'15).
Conference: ESORICS European Symposium On Research In Computer Security

Majumdar, Rupak and Prabhu, Vinayak S.
(2015) Computing the Skorokhod distance between polygonal traces.
In: Proc. of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015).

Saha, Indranil and Baruah, Sanjoy and Majumdar, Rupak
(2015) Dynamic scheduling for networked control systems.
In: Proc. of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015).

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.
In: Proc. 7th NASA Formal Methods Symposium (NFM 2015).

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.
In: Proceedings of the 43nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'15).
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages

Schneider, Sigurd and Smolka, Gert and Hack, Sebastian
(2015) A Linear First-Order Functional Intermediate Language for Verified Compilers.
In: Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings.
Conference: ITP Conference on Interactive Theorem Proving (previously TPHOLs, changed in 2009)

Durand-Gasselin, Antoine and Esparza, Javier and Ganty, Pierre and Majumdar, Rupak
(2015) Model Checking Parameterized Asynchronous Shared-Memory Systems.
In: Proc. of the 27th International Conference on Computer Aided Verification (CAV 2015).
Conference: CAV Computer Aided Verification

Hemed, Nir and Rinetzky, Noam and Vafeiadis, Viktor
(2015) Modular Verification of Concurrency-Aware Linearizability.
In: Distributed Computing - 29th International Symposium, DISC 2015, Tokyo, Japan, October 7-9, 2015, Proceedings.
Conference: DISC International Symposium on Distributed Computing (was WDAG)

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.

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.
In: Proceedings of the 20st ACM SIGPLAN International Conference on Functional Programming (ICFP '15).
Conference: ICFP International Conference on Functional Programming

Deshmukh, Jyotirmoy V. and Majumdar, Rupak and Prabhu, Vinayak S.
(2015) Quantifying Conformance Using the Skorokhod Metric.
In: Proc. of the 27th International Conference on Computer Aided Verification (CAV 2015).
Conference: CAV Computer Aided Verification

Dimitrova, Rayna and Majumdar, Rupak
(2015) Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs.
In: Proceedings of 6th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015).

Gavran, Ivan and Niksic, Filip and Kanade, Aditya and Majumdar, Rupak and Vafeiadis, Viktor
(2015) Rely/Guarantee Reasoning for Asynchronous Programs.
In: Proceedings of the 26th International Conference on Concurrency Theory (CONCUR '15).
Conference: CONCUR International Conference on Concurrency Theory

Cortier, Véronique and Eigner, Fabienne and Kremer, Steve and Maffei, Matteo and Wiedling, Cyrille
(2015) Type-Based Verification of Electronic Voting Protocols.
In: Proceedings of the 4th International Conference on Principles of Security and Trust (POST).

Tassarotti, Joseph and Dreyer, Derek and Vafeiadis, Viktor
(2015) Verifying read-copy-update in a logic for weak memory.
In: Proc. of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015).
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation

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.
In: Proc. of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016).
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation

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.
In: Proceedings of the 23rd International Conference on Real Time Networks and Systems, RTNS 2015, Lille, France, November 4-6, 2015.

Bloem, Roderick and Chatterjee, Krishnendu and Jacobs, Swen and Könighofer, Robert
(2015) Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information.
In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings.
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

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.

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).
In: Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015..

Backes, Michael and Manoharan, Praveen and Mohammadi, Esfandiar
(2014) TUC: Time-sensitive and Modular Analysis of Anonymous Communication.
In: Proceedings of the of the 27th IEEE Computer Security Foundations Symposium (CSF '14).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Datta, Anupam and Garg, Deepak and Jia, Limin and Chowdhury, Omar
(2014) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.
In: Proceedings of the 27th IEEE Computer Security Foundations Symposium (CSF '14).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Reineke, Jan and Doerfert, Johannes
(2014) Architecture-parametric timing analysis.
In: 20th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2014, Berlin, Germany, April 15-17, 2014.

Damm, Werner and Finkbeiner, Bernd
(2014) Automatic Compositional Synthesis of Distributed Systems.
In: Proceedings of the 19th International Symposium on Formal Methods (FM'14).

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.
In: 2014 USENIX Annual Technical Conference, USENIX ATC '14, Philadelphia, PA, USA, June 19-20, 2014..

Reineke, Jan and Tripakis, Stavros
(2014) Basic Problems in Multi-View Modeling.
In: Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 14).
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

Brandenburg, Björn B.
(2014) Blocking Optimality in Distributed Real-Time Locking Protocols.
LITES, 1 (2). 01: 1-01: 22.

Hüchting, Reiner and Majumdar, Rupak and Meyer, Roland
(2014) Bounds on mobility.
In: Proc. of the 25th International Conference on Concurrency Theory (CONCUR 2014).
Conference: CONCUR International Conference on Concurrency Theory

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.

Kupriyanov, Andrey and Finkbeiner, Bernd
(2014) Causal Termination of Multi-threaded Programs.
In: Proc. of the 26th International Conference on Computer Aided Verification (CAV 2014).
Conference: CAV Computer Aided Verification

Reineke, Jan and Maksoud, Mohamed Abdel
(2014) A Compiler Optimization to Increase the Efficiency of WCET Analysis.
In: 22nd International Conference on Real-Time Networks and Systems, RTNS '14, Versaille, France, October 8-10, 2014.

Backes, Michael and Mohammadi, Esfandiar and Ruffing, Tim
(2014) Computational Soundness Results for ProVerif - Bridging the Gap from Trace Properties to Uniformity.
In: Proceedings of the 3rd Conference on Principles of Security and Trust (POST).

Finkbeiner, Bernd and Torfah, Hazem
(2014) Counting Models of Linear-Time Temporal Logic.
In: 8th International Conference on Language and Automata Theory and Applications (LATA 2014).

Carzaniga, Antonio and Goffi, Alberto and Gorla, Alessandra and Mattavelli, Andrea and Pezzè, Mauro
(2014) Cross-checking oracles from intrinsic software redundancy.
In: 36th International Conference on Software Engineering, ICSE '14, Hyderabad, India - May 31 - June 07, 2014.

Dimitrova, Rayna and Majumdar, Rupak
(2014) Deductive control synthesis for alternating-time logics.
In: Proc. of the International Conference on Embedded Software (EMSOFT 2014).
Conference: EMSOFT ACM Conference on Embedded Software

Finkbeiner, Bernd and Tentrup, Leander
(2014) Detecting Unrealizable Specifications of Distributed Systems.
In: Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 14).
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

Eigner, Fabienne and Kate, Aniket and Maffei, Matteo and Pampaloni, Francesca and Pryvalov, Ivan
(2014) Differentially Private Data Aggregation with Optimal Utility.
In: 30th Annual Computer Security Applications Conference (ACSAC).
Conference: ACSAC Annual Computer Security Applications Conference

Esmaeilsabzali, Shahram and Majumdar, Rupak and Wies, Thomas and Zufferey, Damien
(2014) Dynamic package interfaces.
In: Proc. of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014).

Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Majumdar, Rupak
(2014) Edit Distance for Timed Automata.
In: Proc. of the 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014).

Rossberg, Andreas and Russo, Claudio V and Dreyer, Derek
(2014) F-ing modules.
J. Funct. Program., 24 (5). pp. 529-607.

Finkbeiner, Bernd and Tentrup, Leander
(2014) Fast DQBF refutation.
In: Theory and Applications of Satisfiability Testing (SAT 2014).
Conference: SAT International Conference on Theory and Applications of Satisfiability Testing

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.

Turon, Aaron and Vafeiadis, Viktor and Dreyer, Derek
(2014) GPS: navigating weak memory with ghosts, protocols, and separation.
In: Proc. of the 2014 ACM SIGPLAN International Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA 2014).
Conference: OOPSLA ACM Conference on Object Oriented Programming Systems Languages and Applications

Bichhawat, Abhishek and Rajani, Vineet and Garg, Deepak and Hammer, Christian
(2014) Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis.
In: Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security.

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.

Majumdar, Rupak and Tetali, Sai Deep and Wang, Zilong
(2014) Kuai: A model checker for software-defined networks.
In: Proc. of Formal Methods in Computer-Aided Design (FMCAD 2014).

Faymonville, Peter and Finkbeiner, Bernd and Peled, Doron
(2014) Monitoring Parametric Temporal Logic.
In: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'14).

Finkbeiner, Bernd and Olderog, Ernst-Rüdiger
(2014) Petri Games: Synthesis of Distributed Systems with Causal Memory.
In: Proceedings of Fifth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2014).

Kovalev, Mikhail and Müller, Silvia M. and Paul, Wolfgang J.
(2014) A Pipelined Multi-core MIPS Machine -- Hardware Implementation and Correctness Proof.
UNSPECIFIED.

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.
In: Workshop on Usable and Efficient Secure Multiparty Computation -- Satellite Event of ESORICS.

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.
In: Proceedings of the 4th ACM conference on Data and application security and privacy (CODASPY'14).

Maiya, Pallavi and Kanade, Aditya and Majumdar, Rupak
(2014) Race Detection for Android Applications.
In: Proc. of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2014).
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation

Gligoric, Milos and Majumdar, Rupak and Sharma, Rohan and Eloussi, Lamyaa and Marinov, Darko
(2014) Regression Test Selection for Distributed Software Histories.
In: Proc. of the 26th International Conference on Computer Aided Verification (CAV 2014).
Conference: CAV Computer Aided Verification

Abel, Andreas and Reineke, Jan
(2014) Reverse engineering of cache replacement policies in Intel microprocessors and their evaluation.
In: 2014 IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS 2014, Monterey, CA, USA, March 23-25, 2014.

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.
In: Proc. of the 26th International Conference on Computer Aided Verification (CAV 2014).
Conference: CAV Computer Aided Verification

Alvin, Christopher and Gulwani, Sumit and Mukhopadhyay, Supratik and Majumdar, Rupak
(2014) Synthesis of Geometry Proof Problems.
In: Proc. of the 28th Conference of Artificial Intelligence (AAAI 2014).
Conference: AAAI National Conference of the American Association for Artificial Intelligence

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.
In: Proc. of the 3rd Conference on Principles of Security and Trust (POST 2014).

Chowdhury, Omar and Jia, Limin and Garg, Deepak and Datta, Anupam
(2014) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.
In: Proc. 26th International Conference on Computer Aided Verification (CAV 2014).
Conference: CAV Computer Aided Verification

Simkin, Mark and Schröder, Dominique and Bulling, Andreas and Fritz, Mario
(2014) Ubic: Bridging the Gap between Digital Cryptography and the Physical World.
In: Computer Security - ESORICS 2014 - 19th European Symposium on Research in Computer Security, Wroclaw, Poland, September 7-11, 2014. Proceedings, Part I.
Conference: ESORICS European Symposium On Research In Computer Security

Chistikov, Dmitry and Majumdar, Rupak
(2014) Unary Pushdown Automata and Straight-Line Programs.
In: Proc. of the 41st International Colloquium on Automata, Languages and Programming (ICALP 2014).
Conference: ICALP International Colloquium on Automata Languages and Programming

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.

Noschinski, Lars and Rizkallah, Christine and Mehlhorn, Kurt
(2014) Verification of Certifying Computations through AutoCorres and Simpl.
In: Proc. 6th NASA Formal Methods Symposium (NFM 2014).

Finkbeiner, Bernd and Seidl, Helmut and Kovács, Máté
(2013) Relational Abstract Interpretation for the Verification of 2-Hypersafety Properties.
In: Proceedings of the 20th ACM Conference on Computer and Communications Security (CCS '13).
Conference: CCS ACM Conference on Computer and Communications Security

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.
In: Proceedings of the 22nd USENIX Security Symposium (USENIX '13).
Conference: USENIX-Security Usenix Security Symposium

Eigner, Fabienne and Maffei, Matteo
(2013) Differential Privacy by Typing in Security Protocols.
In: Proceedings of the 26th IEEE Computer Security Foundations Symposium (CSF '13).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Maffei, Matteo and Pecina, Kim and Reinert, Manuel
(2013) Security and Privacy by Declarative Design.
In: Proceedings of the IEEE 26th Computer Security Foundations Symposium (CSF '16).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Backes, Michael and Bendun, Fabian and Unruh, Dominique
(2013) Computational Soundness of Symbolic Zero-Knowledge Proofs: Weaker Assumptions and Mechanized Verification.
In: Principles of Security and Trust 2013.

Angius, Alessio and Horváth, András and Wolf, Verena
(2013) Approximate Transient Analysis of Queuing Networks by Quasi Product Forms.
In: Analytical and Stochastic Modelling Techniques and Applications - 20th International Conference, ASMTA 2013, Ghent, Belgium, July 8-10, 2013. Proceedings.

Carzaniga, Antonio and Gorla, Alessandra and Mattavelli, Andrea and Perino, Nicolò and Pezzè, Mauro
(2013) Automatic recovery from runtime failures.
In: 35th International Conference on Software Engineering, ICSE '13, San Francisco, CA, USA, May 18-26, 2013.

Zamani, Majid and Esfahani, Peyman Mohajerin and Majumdar, Rupak and Abate, Alessandro and Lygeros, John
(2013) Bisimilar finite abstractions of stochastic control systems.
In: Proc. of the 52nd IEEE Conference on Decision and Control (CDC 2013).
Conference: CDC IEEE Conference on Decision and Control

Finkbeiner, Bernd and Schewe, Sven
(2013) Bounded synthesis.
In: International Journal on Software Tools for Technology Transfer (STTT'13).

Kupriyanov, Andrey and Finkbeiner, Bernd
(2013) Causality-Based Verification of Multi-threaded Programs.
In: Proc. of the 24th International Conference on Concurrency Theory (CONCUR 2013).
Conference: CONCUR International Conference on Concurrency Theory

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.

Majumdar, Rupak and Saha, Indranil and Ueda, Koichi and Yazarel, Hakan
(2013) Compositional Equivalence Checking for Models and Code of Control Systems.
In: Proc. of the 52nd IEEE Conference on Decision and Control (CDC 2013).
Conference: CDC IEEE Conference on Decision and Control

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

Wieder, Alexander and Brandenburg, Björn B.
(2013) Efficient partitioning of sporadic real-time tasks with shared resources and spin locks.
In: 8th IEEE International Symposium on Industrial Embedded Systems, SIES 2013, Porto, Portugal, June 19-21, 2013.

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.

Majumdar, Rupak and Wang, Zilong
(2013) Expand, Enlarge, and Check for Branching Vector Addition Systems.
In: Proc. of the 24th International Conference on Concurrency Theory (CONCUR 2013).
Conference: CONCUR International Conference on Concurrency Theory

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.

Brandenburg, Björn B.
(2013) A Fully Preemptive Multiprocessor Semaphore Protocol for Latency-Sensitive Real-Time Applications.
In: 25th Euromicro Conference on Real-Time Systems, ECRTS 2013, Paris, France, July 9-12, 2013.
Conference: ECRTS Euromicro Conference on Real-Time Systems

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.
(2013) Improved analysis and evaluation of real-time semaphore protocols for P-FP scheduling.
In: 19th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2013, Philadelphia, PA, USA, April 9-11, 2013.
Conference: RTAS IEEE Real-Time and Embedded Technology and Applications Symposium

Kloos, Johannes and Majumdar, Rupak and Niksic, Filip and Piskac, Ruzica
(2013) Incremental Inductive Coverability.
In: Proc. of the 25th International Conference on Computer Aided Verification (CAV 2013).
Conference: CAV Computer Aided Verification

Bugliesi, Michele and Calzavara, Stefano and Eigner, Fabienne and Maffei, Matteo
(2013) Logical Foundations of Secure Resource Management.
In: Proc. of the 2nd Conference on Principles of Security and Trust (POST 2013).

Dimitrova, Rayna and Finkbeiner, Bernd
(2013) Lossy Channel Games under Incomplete Information.
In: Proceedings 1st International Workshop on Strategic Reasoning (SR'13).

Abel, Andreas and Reineke, Jan
(2013) Measurement-based modeling of the cache replacement policy.
In: 19th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2013, Philadelphia, PA, USA, April 9-11, 2013.
Conference: RTAS IEEE Real-Time and Embedded Technology and Applications Symposium

Gligoric, Milos and Majumdar, Rupak
(2013) Model Checking Database Applications.
In: Proc. of the 20th International Symposium on Static Analysis (SAS 2013).
Conference: SAS Static Analysis Symposium

Tetali, Sai Deep and Lesani, Mohsen and Majumdar, Rupak and Millstein, Todd
(2013) MrCrypt: Static Analysis for Secure Cloud Computations.
In: Proc. of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA 2013).
Conference: OOPSLA ACM Conference on Object Oriented Programming Systems Languages and Applications

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.
In: Proc of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP '13).
Conference: ICFP International Conference on Functional Programming

Baruah, Sanjoy and Brandenburg, Björn B.
(2013) Multiprocessor Feasibility Analysis of Recurrent Task Systems with Specified Processor Affinities.
In: Proceedings of the IEEE 34th Real-Time Systems Symposium, RTSS 2013, Vancouver, BC, Canada, December 3-6, 2013.
Conference: RTSS Real Time Systems Symposium

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.

Wieder, Alexander and Brandenburg, Björn B.
(2013) On Spin Locks in AUTOSAR: Blocking Analysis of FIFO, Unordered, and Priority-Ordered Spin Locks.
In: Proceedings of the IEEE 34th Real-Time Systems Symposium, RTSS 2013, Vancouver, BC, Canada, December 3-6, 2013.
Conference: RTSS Real Time Systems Symposium

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.

Esparza, Javier and Ganty, Pierre and Majumdar, Rupak
(2013) Parameterized verification of asynchronous shared-memory systems.
In: Proc. of the 25th International Conference on Computer Aided Verification (CAV 2013).
Conference: CAV Computer Aided Verification

Andalam, Sidharta and Girault, Alain and Sinha, Roopak and Roop, Partha S. and Reineke, Jan
(2013) Precise timing analysis for direct-mapped caches.
In: The 50th Annual Design Automation Conference 2013, DAC '13, Austin, TX, USA, May 29 - June 07, 2013.
Conference: DAC Design Automation Conf

Zengin, Mustafa and Vafeiadis, Viktor
(2013) A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism.
In: Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, 1-3 July 2013, Birmingham, UK.

Kovács, Máté and Seidl, Helmut and Finkbeiner, Bernd
(2013) Relational abstract interpretation for the verification of 2-hypersafety properties.
In: Proc. of the 20th ACM Conference on Computer and Communication Security (CCS 2013).
Conference: CCS ACM Conference on Computer and Communications Security

Majumdar, Rupak and Meyer, Roland and Wang, Zilong
(2013) Static Provenance Verification for Message Passing Programs.
In: Proc. of the 20th International Symposium on Static Analysis (SAS 2013).
Conference: SAS Static Analysis Symposium

Kloos, Johannes and Majumdar, Rupak
(2013) Supervisor Synthesis for Controller Upgrades.
In: Proc. of the Conference on Design, Automation and Test in Europe (DATE 2013).

Darulova, Eva and Kuncak, Viktor and Majumdar, Rupak and Saha, Indranil
(2013) Synthesis of fixed-point programs.
In: Proc. of the International Conference on Embedded Software (EMSOFT 2013).
Conference: EMSOFT ACM Conference on Embedded Software

Cohen, Ernie and Paul, Wolfgang J. and Schmaltz, Sabine
(2013) Theory of Multi Core Hypervisor Verification.
In: Proc. 39th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2013).

Hüchting, Reiner and Majumdar, Rupak and Meyer, Roland
(2013) A Theory of Name Boundedness.
In: Proc. of the 24th International Conference on Concurrency Theory (CONCUR 2013).
Conference: CONCUR International Conference on Concurrency Theory

Calin, Georgel and Derevenetc, Egor and Majumdar, Rupak and Meyer, Roland
(2013) A Theory of Partitioned Global Address Spaces.
In: Proc. of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013).

Chistikov, Dmitry and Majumdar, Rupak
(2013) A Uniformization Theorem for Nested Word to Word Transductions.
In: Proc. of the 18th International Conference on Implementation and Application of Automata (CIAA 2013).

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.

Backes, Michael and Malik, Ankit and Unruh, Dominique
(2012) Computational Soundness without Protocol Restrictions.
In: Proceedings of the 19th ACM Conference on Computer and Communication Security (CCS '12).
Conference: CCS ACM Conference on Computer and Communications Security

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.
In: Proceedings of the 25th IEEE Computer Security Foundations Symposium - CSF 2012.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Genovese, Valerio and Garg, Deepak and Rispoli, Daniele
(2012) Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction.
In: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF '12).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Backes, Michael and Maffei, Matteo and Pecina, Kim
(2012) Automated Synthesis of Secure Distributed Applications.
In: Proceedings of the 19th Annual Network and Distributed System Security Symposium (NDSS '12).
Conference: NDSS Network and Distributed System Security Symposium

Bugliesi, Michele and Calzavara, Stefano and Eigner, Fabienne and Maffei, Matteo
(2012) Affine Refinement Types for Authentication and Authorization.
In: Proc. 6th International Symposium on Trustworthy Global Computing (TGC 2012).

Ganty, Pierre and Majumdar, Rupak
(2012) Algorithmic Verification of Asynchronous Programs.
ACM Transactions on Programming Languages and Systems, 34 (1). 6:1-6:48.

Majumdar, Rupak and Zamani, Majid
(2012) Approximately Bisimilar Symbolic Models for Digital Control Systems.
In: Proc. of the 24th International Conference on Computer Aided Verification (CAV 2012).
Conference: CAV Computer Aided Verification

Peter, Philip
(2012) Autonomous UAV.
Bachelors thesis, Saarland University.

Majumdar, Rupak and Saha, Indranil and Shashidhar, K C and Wang, Zilong
(2012) CLSE: Closed-Loop Symbolic Execution.
In: Proc. of the 4th International Symposium on NASA Formal Methods (NFM 2012).

Schmidt, Jens M
(2012) Certifying 3-Connectivity in Linear Time.
In: Proc. 39th International Colloquium on Automata, Languages and Programming (ICALP 2012).

Paul, Wolfgang J. and Schmaltz, Sabine and Shadrin, Andrey
(2012) Completing the Automated Verification of a Small Hypervisor - Assembler Code Verification.
In: Proc. 10th International Conference on Software Engineering and Formal Methods (SEFM 2012).

Peter, Hans-Jörg and Finkbeiner, Bernd
(2012) The Complexity of Bounded Synthesis for Timed Control with Partial Observability.
In: Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'12).

Dimitrova, Rayna and Finkbeiner, Bernd
(2012) Counterexample-Guided Synthesis of Observation Predicates.
In: Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'12).

Garg, Deepak and Genovese, Valerio and Negri, Sara
(2012) Countermodels from Sequent Calculi in Multi-Modal Logics.
In: Proc. of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012).
Conference: LICS IEEE Symposium on Logic in Computer Science

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)

Lee, Jonathan K. and Palsberg, Jens and Majumdar, Rupak and Hong, Hong
(2012) Efficient May Happen in Parallel Analysis for Async-finish Parallelism.
In: Proc. of the 19th International Symposium on Static Analysis (SAS 2012).
Conference: SAS Static Analysis Symposium

Kuhtz, Lars and Finkbeiner, Bernd
(2012) Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds.
In: Logical Methods in Computer Science (LMCS'12).

Maksoud, Mohamed Abdel and Reineke, Jan
(2012) An Empirical Evaluation of the Influence of the Load-Store Unit on WCET Analysis.
In: 12th International Workshop on Worst-Case Execution Time Analysis, WCET 2012, July 10, 2012, Pisa, Italy.

Basin, David and Jugé, Vincent and Klaedtke, Felix and Zvalinescu, Eugen
(2012) Enforceable Security Policies Revisited.
In: Proc. 1st Conference on Principles of Security and Trust (POST).

Fischer, Jeffrey and Majumdar, Rupak and Esmaeilsabzali, Shahram
(2012) Engage: A Deployment Management System.
In: Proc. of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2012).
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation

Chatterjee, Krishnendu and Chmelik, Martin and Majumdar, Rupak
(2012) Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games.
In: Proc. of the 10th International Symposium on Automated Technology for Verification and Analysis (ATVA 2012).
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

Tabuada, Paulo and Balkan, Ayca and Caliskan, Sina Yamac and Shoukry, Yasser and Majumdar, Rupak
(2012) Input-Output stability for discrete systems.
In: Proc. of the International Conference on Embedded Software (EMSOFT 2012).
Conference: EMSOFT ACM Conference on Embedded Software

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.
In: Proc. 4th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2012).

Genovese, Valerio and Garg, Deepak and Rispoli, Daniele
(2012) Labeled Goal-Directed Search in Access Control Logic.
In: Proc. of the 8th International Workshop on Security and Trust Management (STM 2012).

Long, Zhenyue and Calin, Georgel and Majumdar, Rupak and Meyer, Roland
(2012) Language-Theoretic Abstraction Refinement.
In: Proc. of the 15th International Conference on Fundamental Approaches to Software Engineering (FASE 2012).

Finkbeiner, Bernd and Jacobs, Swen
(2012) Lazy Synthesis.
In: Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'12).

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.
In: Sicherheit 2012 -- Beiträge der 6-ten Jahrestagung des Fachbereichs Sicherheit der Gesellschaft für Informatik e. V..

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.
In: Proc. 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI).

Lutz, Joachim
(2012) Model-based Monitoring for Sensitive SCADA Systems.
Bachelors thesis, Saarland University.

Ehlers, Rüdiger and Finkbeiner, Bernd
(2012) Monitoring Realizability.
In: Proceedings of the Second International Conference on Runtime Verification (RV'11).

Dimitrova, Rayna and Finkbeiner, Bernd and Rabe, Markus N.
(2012) Monitoring Temporal Information Flow.
In: Proc. 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA).

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.

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.
In: Proc. 4th NASA Formal Methods Symposium (NFM 2012).

Esparza, Javier and Ganty, Pierre and Majumdar, Rupak
(2012) A Perfect Model for Bounded Verification.
In: Proc. of the 27th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS 2012).
Conference: LICS IEEE Symposium on Logic in Computer Science

Reischuk, Raphael M. and Backes, Michael and Gehrke, Johannes
(2012) SAFE Extensibility of Data-Driven Web Applications.
In: WWW~'12: Proceedings of the 21st International World Wide Web Conference.
Conference: WWW The Web Conference (Formerly: International World Wide Web Conference)

Carreira, João Carlos Menezes and Rodrigues, Rodrigo and Candea, George and Majumdar, Rupak
(2012) Scalable Testing of File System Checkers.
In: Proc. of the 7th ACM European Conference on Computer Systems (EuroSys 2012).
Conference: EuroSys Eurosys Conference

Garg, Deepak and Pfenning, Frank
(2012) Stateful authorization logic - Proof theory and a case study.
Journal of Computer Security, 20 (4). pp. 353-391.

Krishnaswami, Neelakantan R. and Turon, Aaron and Dreyer, Derek and Garg, Deepak
(2012) Superficially substructural types.
In: ACM SIGPLAN International Conference on Functional Programming (ICFP 2012).
Conference: ICFP International Conference on Functional Programming

Majumdar, Rupak and Saha, Indranil and Zamani, Majid
(2012) Synthesis of minimal-error control software.
In: Proc. of the International Conference on Embedded Software (EMSOFT 2012).
Conference: EMSOFT ACM Conference on Embedded Software

Finkbeiner, Bernd and Peter, Hans-Jörg
(2012) Template-Based Controller Synthesis for Timed Systems.
In: Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 12).
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

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.

Saha, Indranil and Majumdar, Rupak
(2012) Trigger memoization in self-triggered control.
In: Proc. of the International Conference on Embedded Software (EMSOFT 2012).
Conference: EMSOFT ACM Conference on Embedded Software

Vahldiek, Anjo and Elnikety, Eslam and Post, Ansley and Druschel, Peter and Garg, Deepak and Gehrke, Johannes and Rodrigues, Rodrigo
(2012) Trusted Storage.
In: Presented at USENIX FAST'12 WiP.
Conference: FAST Conference on File and Storage Technologies

Alkassar, Eyad and Cohen, Ernie and Kovalev, Mikhail and Paul, Wolfgang J.
(2012) Verification of TLB Virtualization Implemented in C.
In: Proc. 4th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2012).

Datta, Anupam and Garg, Deepak and Jia, Limin
(2011) Policy auditing over incomplete logs: theory, implementation and applications.
In: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS '11).
Conference: CCS ACM Conference on Computer and Communications Security

Nanevski, Aleksandar and Banerjee, Anindya and Garg, Deepak
(2011) Verification of Information Flow and Access Control Policies with Dependent Types.
In: Proceedings of the 32nd IEEE Symposium on Security and Privacy (S&P '11).
Conference: SP IEEE Symposium on Security and Privacy

Backes, Michael and Maffei, Matteo and Pecina, Kim
(2011) A Security API for Distributed Social Networks.
In: Proceedings of the Network and Distributed System Security Symposium (NDSS '11).
Conference: NDSS Network and Distributed System Security Symposium

Mantel, Heiko and Sands, David and Sudbrock, Henning
(2011) Assumptions and Guarantees for Compositional Noninterference.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Ngo, Long and Boyd, Colin and Nieto, Juan Gonzalez
(2011) Automated proofs for Diffie-Hellman-based key exchanges.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Backes, Michael and Hriţcu, Cătălin and Tarrach, Thorsten
(2011) Automatically Verifying Typing Constraints for a Data Processing Language.
In: Proc. 1st International Conference on Certified Programs and Proofs (CPP 2011).

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.

Jose, Manu and Majumdar, Rupak
(2011) Bug-Assist: Assisting Fault Localization in ANSI-C Programs.
In: Proc. of the 23rd International Conference on Computer Aided Verification (CAV 2011).
Conference: CAV Computer Aided Verification

Herter, Jörg and Backes, Peter and Haupenthal, Florian and Reineke, Jan
(2011) CAMA: A Predictable Cache-Aware Memory Allocator.
In: 23rd Euromicro Conference on Real-Time Systems, ECRTS 2011, Porto, Portugal, 5-8 July, 2011.
Conference: ECRTS Euromicro Conference on Real-Time Systems

Jose, Manu and Majumdar, Rupak
(2011) Cause Clue Clauses: Error Localization Using Maximum Satisfiability.
In: Proc. of the 32rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011).
Conference: PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation

Meiser, Sebastian
(2011) Computational Soundness of Passively Secure Encryption in Presence of Active Adversaries.
In: Seventh Workshop on Formal and Computational Cryptography (FCC 2011).

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.
In: Proceedings of the 9th International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2011, part of ESWeek '11 Seventh Embedded Systems Week, Taipei, Taiwan, 9-14 October, 201.

Damm, Werner and Finkbeiner, Bernd
(2011) Does It Pay to Extend the Perimeter of a World Model?
In: Proceedings of the 17th International Symposium on Formal Methods (FM'11).

Mardziel, Piotr and Magill, Stephen and Hicks, Michael and Srivatsa, Mudhakar
(2011) Dynamic Enforcement of Knowledge-based Security Policies.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Asghar, Muhammad Rizwan and Ion, Mihaela and Russello, Giovanni and Crispo, Bruno
(2011) ESPOON: Enforcing Encrypted Security Policies in Outsourced Environments.
In: The Sixth International Conference on Availability, Reliability and Security.

Mikeev, Linar and Sandmann, Werner and Wolf, Verena
(2011) Efficient calculation of rare event probabilities in Markovian queueing networks.
In: 5th International ICST Conference on Performance Evaluation Methodologies and Tools Communications, VALUETOOLS '11, Paris, France, May 16-20, 2011.

Cheney, James
(2011) A Formal Framework for Provenance Security.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Delaune, Stephanie and Kremer, Steve and Ryan, Mark D. and Steel, Graham
(2011) Formal analysis of protocols based on TPM state registers.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

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.

Backes, Michael and Maffei, Matteo and Pecina, Kim and Reischuk, Raphael M.
(2011) G2C: Cryptographic Protocols from Goal-Driven Specifications.
In: TOSCA'11: Proceedings of the 2011 International Conference on Theory of Security and Applications (now POST), held as part of ETAPS 2011.

Dupressoir, Francois and Gordon, Andrew D. and Jurjens, Jan and Naumann, David A.
(2011) Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Jhala, Ranjit and Majumdar, Rupak and Rybalchenko, Andrey
(2011) HMC: Verifying Functional Programs Using Abstract Interpreters.
In: Proc. of the 23rd International Conference on Computer Aided Verification (CAV 2011).
Conference: CAV Computer Aided Verification

Frau, Simone and Dashti, Mohammad Torabi
(2011) Integrated Specification and Verification of Security Protocols and Policies.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Tombers, Stefan
(2011) Low-Cost Byzantine Fault Tolerant Replication for a Cloud Environment.
Bachelors thesis, Saarland University.

Zamani, Majid and Majumdar, Rupak
(2011) A Lyapunov approach in incremental stability.
In: 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC 2011).
Conference: CDC IEEE Conference on Decision and Control

Chatterjee, Krishnendu and Majumdar, Rupak
(2011) Minimum Attention Controller Synthesis for Omega-regular Objectives.
In: Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11).

Backes, Michael and Berg, Matthias and Köpf, Boris
(2011) Non-Uniform Distributions in Quantitative Information-Flow.
In: Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS).

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.

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.
In: Proceedings of the 9th International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2011, part of ESWeek '11 Seventh Embedded Systems Week, Taipei, Taiwan, 9-14 October, 201.

Majumdar, Rupak and Saha, Indranil and Zamani, Majid
(2011) Performance-aware Scheduler Synthesis for Control Systems.
In: Proc. of the International Conference on Embedded Software (EMSOFT 2011).
Conference: EMSOFT ACM Conference on Embedded Software

Roy, Pritam and Tabuada, Paulo and Majumdar, Rupak
(2011) Pessoa 2.0: A Controller Synthesis Tool for Cyber-physical Systems.
In: Proc. of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC 2011).

Ehlers, Rüdiger and Finkbeiner, Bernd
(2011) Reactive Safety.
In: Proceedings of Second International Symposium on Games, Automata3Logics and Formal Verification (GandALF 2011).

Sevcík, Jaroslav and Vafeiadis, Viktor and Nardelli, Francesco Zappa and Jagannathan, Suresh and Sewell, Peter
(2011) Relaxed-memory concurrency and verified compilation.
In: Proceedings of the 38th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'11).
Conference: POPL ACM-SIGACT Symposium on Principles of Programming Languages

Bugliesi, Michele and Calzavara, Stefano and Eigner, Fabienne and Maffei, Matteo
(2011) Resource-aware Authorization Policies for Statically Typed Cryptographic Protocols.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Majumdar, Rupak and Render, Elaine and Tabuada, Paulo
(2011) Robust Discrete Synthesis Against Unspecified Disturbances.
In: Proc. of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC 2011).

Lapin, Maksim and Mikeev, Linar and Wolf, Verena
(2011) SHAVE: stochastic hybrid analysis of markov population models.
In: Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011.

Moore, Scott and Chong, Stephen
(2011) Static analysis for efficient hybrid information-flow control.
In: Proceedings of the 24th IEEE Computer Security Foundations Symposium.
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

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

Grund, Daniel and Reineke, Jan and Wilhelm, Reinhard
(2011) A Template for Predictability Definitions with Supporting Evidence.
In: Bringing Theory to Practice: Predictability and Performance in Embedded Systems, DATE Workshop PPES 2011, March 18, 2011, Grenoble, France..

Bui, Dai N and Lee, Edward A. and Liu, Isaac and Patel, Hiren D. and Reineke, Jan
(2011) Temporal isolation on multiprocessing architectures.
In: Proceedings of the 48th Design Automation Conference, DAC 2011, San Diego, California, USA, June 5-10, 2011.
Conference: DAC Design Automation Conf

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.
In: Proc. of the 7th International Conference Information Systems Security (ICISS 2011).

Backes, Michael and Hriţcu, Cătălin and Maffei, Matteo
(2011) Union and Intersection Types for Secure Protocol Implementations.
In: Theory of Security and Applications - Joint Workshop, TOSCA 2011, Saarbrücken, Germany, March 31 - April 1, 2011, Revised Selected Papers.

Alkassar, Eyad and Böhme, Sascha and Mehlhorn, Kurt and Rizkallah, Christine
(2011) Verification of Certifying Computations.
In: Proc. of the 23rd International Conference on Computer Aided Verification (CAV 2011).
Conference: CAV Computer Aided Verification

Finkbeiner, Bernd and Kuhtz, Lars
(2011) Weak Kripke Structures and LTL.
In: Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR'11).
Conference: CONCUR International Conference on Concurrency Theory

Backes, Michael and Dürmuth, Markus and Gerling, Sebastian and Pinkal, Manfred and Sporleder, Caroline
(2010) Acoustic Side-Channel Attacks of Printers.
In: Proceedings of 19th USENIX Security Symposium.
Conference: USENIX-Security Usenix Security Symposium

Hammer, Christian
(2010) Experiences with PDG-based IFC.
In: International Symposium on Engineering Secure Software and Systems (ESSoS'10).

Vaziri, Mandana and Tip, Frank and Dolby, Julian and Hammer, Christian and Vitek, Jan
(2010) A Type System for Data-Centric Synchronization.
In: ECOOP '10: Proceedings of the 24th European Conference on Object-Oriented Programming.

Gerling, Sebastian
(2009) Acoustic Side-Channel Attacks on Printers.
Masters thesis, Saarland University.

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.

Hammer, Christian
(2009) Information Flow Control for Java - A Comprehensive Approach based on Path Conditions in Dependence Graphs.
Doctoral thesis, Universit.

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.

Hammer, Christian and Dolby, Julian and Vaziri, Mandana and Tip, Frank
(2008) Dynamic detection of atomic-set-serializability violations.
In: ICSE '08: Proceedings of the 30th international conference on Software engineering.

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)

Giffhorn, Dennis and Hammer, Christian
(2008) Precise Analysis of Java Programs using JOANA (Tool Demonstration).
In: Proc. 8th IEEE International Working Conference on Source Code Analysis and Manipulation.

Hammer, Christian and Schaade, Rüdiger and Snelting, Gregor
(2008) Static path conditions for Java.
In: UNSPECIFIED.

Giffhorn, Dennis and Hammer, Christian
(2007) An Evaluation of Precise Slicing Algorithms for Concurrent Programs.
In: SCAM'07: Seventh IEEE International Working Conference on Source Code Analysis and Manipulation.

Hammer, Christian and Grimme, Martin and Krinke, Jens
(2006) Dynamic path conditions in dependence graphs.
In: PEPM '06: Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation.

Hammer, Christian and Krinke, Jens and Snelting, Gregor
(2006) Information Flow Control for Java Based on Path Conditions in Dependence Graphs.
In: Proc. IEEE International Symposium on Secure Software Engineering (ISSSE'06).

Hammer, Christian and Krinke, Jens and Nodes, Frank
(2006) Intransitive Noninterference in Dependence Graphs.
In: Proc. Second International Symposium on Leveraging Application of Formal Methods, Verification and Validation (ISoLA 2006).

Hammer, Christian and Snelting, Gregor
(2004) An improved slicer for Java.
In: PASTE '04: Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering.

This list was generated on Wed Nov 13 03:32:52 2024 CET.