Publications 2015

Peter Gammie and Andreas Lochbihler
The Stern-Brocot Tree
Archive of Formal Proofs, 2015
[DownloadBIB (BIB, 285 Bytes) | external pageLink]
Andreas Lochbihler and Joshua Schneider
Applicative Lifting
Archive of Formal Proofs, 2015
[DownloadBIB (BIB, 297 Bytes) | external pageLink]
David Basin, Felix Klaedtke, and Eugen Zalinescu
Failure-aware Runtime Verification of Distributed Systems
35th Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTCCS), 2015
[DownloadBIB (BIB, 963 Bytes) | DownloadPDF (PDF, 531 KB) | external pageDOI | external pageURL]
Grgur Petric Maretic, Mohammad Torabi Dashti, David Basin
Semantic Vacuity
22nd International Symposium on Temporal Representation and Reasoning (TIME), 2015.
[DownloadBIB (BIB, 710 Bytes) | PDF | external pageDOI | external pageURL]
Carlos Cotrini Jimenez, Thilo Weghorn, David Basin, Manuel Clavel
Analyzing First-Order Role Based Access Control
IEEE} 28th Computer Security Foundations Symposium, {CSF} 2015, pages 3-17, Verona, Italy, 13-17 July, 2015
[DownloadBIB (BIB, 306 Bytes) | DownloadPDF (PDF, 511 KB) | external pageDOI ]
David Basin, Cas Cremers, Kunihiko Miyazaki, Sasa Radomirovic and Dai Watanabe
Improving the Security of Cryptographic Protocol Standards
IEEE Security & Privacy, 13(3):24-31, 2015.
[DownloadBIB (BIB, 449 Bytes) | DownloadPDF (PDF, 384 KB) | external pageDOI | DownloadIEEE Preprint (PDF, 239 KB)]
Dmitriy Traytel and Tobias Nipkow
Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Journal of Functional Programming, 25, 2015.
[BIB | PDF | external pageDOI]
David Basin, Jannik Dreier, Ralf Sasse
Automated Symbolic Proofs of Observational Equivalence
In Proceedings of the ACM Conference on Computer and Communication Security (CCS)
Pages 1144-1155, 2015.
[DownloadBIB (BIB, 761 Bytes) | DownloadPDF (PDF, 373 KB) | external pageDOI | DownloadExtended version (PDF, 499 KB)]
David Basin, Michel Keller, Sasa Radomirovic, Ralf Sasse
Alice and Bob Meet Equational Theories
Logic, Rewriting, and Concurrency - Festschrift Symposium in Honor of José Meseguer 2015
[DownloadBIB (BIB, 765 Bytes) | DownloadPDF (PDF, 385 KB) | external pageDOI]
Jannik Dreier, Ali Kassem, and Pascal Lafourcade
Formal Analysis of E-Cash Protocols
International Conference on Security and Cryptography (SECRYPT 2015)
[DownloadBIB (BIB, 516 Bytes) | DownloadPDF (PDF, 304 KB) | external pageDOI]
Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, and Gabriele Lenzini
A Framework for Analyzing Verifiability in Traditional and Electronic Exams
11th International Conference on Information Security Practice and Experience (ISPEC 2015)
[BIB | DownloadPDF (PDF, 257 KB) | external pageDOI]
Andreas Lochbihler and Alexandra Maximova
Stream Fusion for Isabelle's Code Generator (Rough Diamond)
Interactive Theorem Proving (ITP 2015), LNCS 9236, pp. 270-277.
[DownloadBIB (BIB, 432 Bytes) | DownloadPDF (PDF, 165 KB) | external pageDOI]
Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel
A Formalised Hierarchy of Probabilistic System Types (Proof Pearl)
Interactive Theorem Proving (ITP 2015), LNCS 9236, pp. 203-220.
[DownloadBIB (BIB, 463 Bytes) | DownloadPDF (PDF, 263 KB) | external pageDOI]
Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel
A Zoo of Probabilistic Systems
Archive of Formal Proofs, 2015.
[DownloadBIB (BIB, 352 Bytes) | external pageLink]
Andreas Lochbihler and Tobias Nipkow
Trie
Archive of Formal Proofs, 2015.
[DownloadBIB (BIB, 284 Bytes) | external pageLink]
Ognjen Marić, Christoph Sprenger and David Basin
Consensus Refined
Dependable Systems and Networks (DSN) 2015, pp. 391-402.
[DownloadBIB (BIB, 408 Bytes) | PDF | external pageDOI ]
Ognjen Marić and Christoph Sprenger
Consensus Refined
Archive of Formal Proofs, 2015.
[DownloadBIB (BIB, 297 Bytes) | external pageLink]
David Basin, Felix Klaedtke, Samuel Müller, and Eugen Zălinescu.
Monitoring Metric First-order Temporal Properties
Journal of the ACM
(62(2):15:1-15:45, 2015.
[DownloadBIB (BIB, 515 Bytes) | PDF | external pageDOI]
David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zălinescu.
Monitoring of Temporal First-order Properties with Aggregations
Formal Methods in System Design, 2015.
[DownloadBIB | PDF | external pageDOI]
David Basin, Felix Klaedtke, and Eugen Zălinescu.
Greedily Computing Associative Aggregations on Sliding Windows
Information Processing Letters, 115(2):186-192, 2015.
[DownloadBIB (BIB, 389 Bytes) | PDF | external pageDOI]
Carlos Cotrini, Thilo Weghorn, David Basin, and Manuel Clavel.
Analyzing First-order Role Based Access Control
In Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF 2015), pages 3-17, IEEE 2015.
[DownloadBIB (BIB, 318 Bytes) | DownloadPDF (PDF, 531 KB) | external pageDOI]
David Basin, Sasa Radomirovic, and Michael Schläpfer.
A Complete Characterization of Secure Human-Server Communication
In Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF)
Pages 199-213, 2015.
[DownloadBIB (BIB, 533 Bytes) | DownloadPDF (PDF, 420 KB) | external pageDOI]
Sjouke Mauw and Sasa Radomirovic.
Generalizing Multi-party Contract Signing
In Principles of Security and Trust (POST 2015), pages 156-175, 2015.
[DownloadBIB (BIB, 484 Bytes) | external pagePDF | external pageDOI]
Laurent Cuennet, Marc Pouly, and Sasa Radomirovic.
Guided Specification and Analysis of a Loyalty Card System
In Workshop on Graphical Models for Security (GraMSec 2015).
[BIB | DownloadPDF (PDF, 255 KB) | DOI]
Thanh Binh Nguyen and Christoph Sprenger.
Abstractions for Security Protocol Verification
In Principles of Security and Trust (POST 2015), pages 196-215, 2015.
[DownloadBIB (BIB, 517 Bytes) | DownloadPDF (PDF, 405 KB) | external pageDOI]
Ravi Jhawar, Barbara Kordy, Sjouke Mauw, Sasa Radomirovic, and Rolando Trujillo-Rasua
Attack Trees with Sequential Conjunction
In IFIP, ICT Systems Security and Privacy Protection
Volume 455, pages 339-353, 2015.
[DownloadBIB (BIB, 594 Bytes) | external pagePDF | external pageDOI]