| Title |
Author(s) |
Source |
| Towards AI-assisted Correctness-by-Construction
Software Development | Maximilian Kodetzki, Tabea Bordis, Michael Kirsten, and Ina Schaefer | 12th International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation (ISoLA 2024) |
| SoK: Mechanisms Used in Practice for Verifiable
Internet Voting | Florian Moser, Michael Kirsten, and Felix Dörre | 9th International Joint Conference on Electronic
Voting (E-Vote-ID 2024) |
| Formal Foundations of Consistency in Model-Driven
Development | Romain Pascual, Bernhard Beckert, Mattias Ulbrich, Michael Kirsten, and Wolfram Pfeifer | 12th International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation (ISoLA 2024) |
| Recommendations for Implementing Independent Individual
Verifiability in Internet Voting | Florian Moser, Rüdiger Grimm, Tobias Hilt, Michael Kirsten, Christoph Niederbudde, and Melanie Volkamer | 9th International Joint Conference on Electronic
Voting (E-Vote-ID 2024) |
| The Java Verification Tool KeY: A Tutorial | Bernhard Beckert, Richard Bubel, Daniel Drodt, Reiner Hähnle, Florian Lanzinger, Wolfram Pfeifer, Mattias Ulbrich, and Alexander Weigl | 26th International Symposium on Formal Methods (FM 2024) |
| Quantifying Software Correctness by Combining Architecture Modeling
and Formal Program Analysis | Florian Lanzinger, Christian Martin, Frederik Reiche, Samuel Teuber, Robert Heinrich, and Alexander Weigl | Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing,
SAC 2024 |
| Formally Verifying an Efficient Sorter | Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Sascha Witt, and Julian Wiesler | International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2024 |
| Scalable and Precise Refinement Types for Imperative Languages | Florian Lanzinger, Joshua Bachmeier, Mattias Ulbrich, and Werner Dietl | iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands,
November 13-15, 2023, Proceedings |
| The 'Choc-Machine' - an Introduction to Algorithmic Thinking Using Finite State Machines | Annika Vielsack, Miriam Klein, Thomas Niesenhaus, and Mattias Ulbrich | Proceedings of the 18th WiPSCE Conference on Primary and Secondary Computing Education Research |
| A SAT-Benchmark Set from the Approximation of
Trigonometric Functions for SAT-based Verification | Kai Hiller and Alexander Weigl | Proceedings of SAT Competition 2023: Solver, Benchmark
and Proof Checker Descriptions |
| Neue Einblicke in den Berufswahlprozess von Informatiklehrkräften | Claudia Hildebrandt, Barbara Pampel, Bernhard Standl, Franz J. Hauck, Mattias Ulbrich, and Barbara Paech | Informatikunterricht zwischen Aktualität und Zeitlosigkeit:
20. GI-Fachtagung Informatik und Schule, INFOS 2023, Volume P-336 |
| A Refactoring for Data Minimisation Using Formal
Verification | Florian Lanzinger, Mattias Ulbrich, and Alexander Weigl | 11th International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation. Software
Engineering (ISoLA 2022) |
| Why is Online Voting Still Largely a Black Box? | Michael Kirsten, Melanie Volkamer, and Bernhard Beckert | First International Workshop on Election Infrastructure
Security (EIS 2022) in conjunction with ESORICS 2022:
European Symposium on Research in Computer Security |
| Optimized Symbolic Interval Propagation for Neural
Network Verification | Philipp Kern, Marko Kleine Büning, and Carsten Sinz | 1st Workshop on Formal Verification of Machine
Learning (WFVML 2022) colocated
with ICML 2022: International Conference on
Machine Learning |
| Algorithmic Fairness and Secure Information
Flow (Extended Abstract) | Bernhard Beckert, Michael Kirsten, and Michael Schefczyk | European Workshop on Algorithmic Fairness (EWAF '22),
Lightning round track |
| Formal Specification and Verification of JDK’s Identity Hash Map Implementation | Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, and Alexander Weigl | 17th International Conference on integrated Formal Methods (iFM 2022) |
| Certified Verification of Relational Properties | Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, and Pascale Le Gall | 17th International Conference on integrated Formal Methods (iFM 2022) |
| Inferring Interval-Valued Floating-Point Preconditions | Jonas Krämer, Lionel Blatter, Eva Darulova, and Mattias Ulbrich | 28th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS 2022),
held as part of ETAPS 2022: European Joint Conferences
on Theory and Practice of Software, Part I |
| Towards a Formal Approach for Data Minimization in Programs | Florian Lanzinger and Alexander Weigl | Data Privacy Management, Cryptocurrencies and Blockchain Technology |
| Generalized Test Tables: A Domain-Specific Specification Language
for Automated Production Systems | Bernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander Weigl | Theoretical Aspects of Computing - ICTAC 2022 |
| SpecifyThis - Bridging Gaps Between Program Specification Paradigms | Wolfgang Ahrendt, Paula Herber, Marieke Huisman, and Mattias Ulbrich | Leveraging Applications of Formal Methods, Verification and Validation.
Verification Principles (ISoLA) 2022 |
| Towards a Usable and Sustainable Deductive Verification Tool | Bernhard Beckert, Richard Bubel, Reiner Hähnle, and Mattias Ulbrich | Leveraging Applications of Formal Methods, Verification and Validation.
Software Engineering (ISoLA) 2022 |
| Upper Bound Computation of Information Leakages for
Unbounded Recursion | Johannes Bechberger and Alexander Weigl | 19th International Conference on Software Engineering
and Formal Methods (SEFM 2021) |
| Geometric Path Enumeration for Equivalence
Verification of Neural Networks | Samuel Teuber, Marko Kleine Büning, Philipp Kern, and Carsten Sinz | 33rd IEEE International Conference on Tools
with Artificial Intelligence (ICTAI 2021) |
| Quantifying Software Reliability via Model-Counting | Samuel Teuber and Alexander Weigl | 18th International Conference on Quantitative
Evaluation of Systems (QEST 2021) |
| Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control | Jonas Schiffl, Matthias Grundmann, Marc Leinweber, Oliver Stengele, Sebastian Friebe, and Bernhard Beckert | SACMAT '21: Proceedings of the 26th ACM Symposium on
Access Control Models and Technologies |
| Runtime Verification of Generalized Test Tables | Alexander Weigl, Mattias Ulbrich, Shmuel S. Tyszberowicz, and Jonas Klamroth | NASA Formal Methods - 13th International Symposium, NFM 2021,
Virtual Event, May 24-28, 2021, Proceedings |
| Deductive Verification of Floating-Point Java Programs in KeY | Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, and Wolfgang Ahrendt | 27th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2021), held as part
of ETAPS 2021: European Joint Conferences on Theory and Practice
of Software, Part II |
| Reconstructing Z3 proofs in KeY: There and back again | Wolfram Pfeifer, Jonas Schiffl, and Mattias Ulbrich | Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like
Programs (FTfJP 2021), co-located with ECOOP/ISSTA 2021, Online, 13 July 2021 |
| Design- and Evaluation-Concept for Teaching and Learning Laboratories
in Informatics Teacher Education | Bernhard Standl, Anette Bentz, Mattias Ulbrich, Annika Vielsack, and Ingo Wagner | Informatics in Schools. Engaging Learners in Computational Thinking
- 13th International Conference, ISSEP 2020, Tallinn, Estonia, November
16-18, 2020, Proceedings |
| Modular Verification of JML Contracts Using Bounded Model Checking | Bernhard Beckert, Michael Kirsten, Jonas Klamroth, and Mattias Ulbrich | 9th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation (ISoLA 2020), Part I: Verification Principles |
| Modular Regression Verification for Reactive Systems | Alexander Weigl, Mattias Ulbrich, and Daniel Lentzsch | 9th International Symposium on
Leveraging Applications of Formal Methods,
Verification and Validation (ISoLA 2020), Part II: Engineering Principles |
| Specifying Framing Conditions for Smart Contracts | Bernhard Beckert and Jonas Schiffl | ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation |
| Verifying Equivalence Properties of Neural Networks with
ReLU Activation Functions | Marko Kleine Büning, Philipp Kern, and Carsten Sinz | 26th International Conference on Principles and Practice
of Constraint Programming (CP 2020) |
| Verified Construction of Fair Voting Rules | Karsten Diekhoff, Michael Kirsten, and Jonas Krämer | 29th International Symposium on Logic-Based Program
Synthesis and Transformation (LOPSTR 2019),
Revised Selected Papers |
| Relational Test Tables: A Practical Specification Language for Evolution
and Security | Alexander Weigl, Mattias Ulbrich, Suhyun Cha, Bernhard Beckert, and Birgit Vogel‑Heuser | FormaliSE@ICSE 2020: 8th International Conference on Formal Methods
in Software Engineering, Seoul, Republic of Korea, July 13, 2020 |
| On the Preservation of the Trust by Regression Verification of PLC
software for Cyber-Physical Systems of Systems | Suhyun Cha, Mattias Ulbrich, Alexander Weigl, Bernhard Beckert, Kathrin Land, and Birgit Vogel‑Heuser | 17th IEEE International Conference on Industrial Informatics (INDIN 2019) |
| Card-Based Cryptography Meets Formal Verification | Alexander Koch, Michael Schrempp, and Michael Kirsten | 25th International Conference on the Theory and
Application of Cryptology and Information Security
(ASIACRYPT 2019), Part I |
| Formal Property-Oriented Design of
Voting Rules Using Composable Modules | Karsten Diekhoff, Michael Kirsten, and Jonas Krämer | 6th International Conference on Algorithmic
Decision Theory (ADT 2019), Part Short Papers |
| Smart Contracts: Application Scenarios for Deductive Program Verification | Bernhard Beckert, Jonas Schiffl, and Mattias Ulbrich | 1st Workshop on Formal Methods for Blockchains (FMBC 2019)
hosted by the 3rd Formal Methods World Congress (FM’19) |
| GI Elections with POLYAS: a Road to End-to-End
Verifiable Elections | Bernhard Beckert, Achim Brelle, Rüdiger Grimm, Nicolas Huber, Michael Kirsten, Ralf Küsters, Jörn Müller‑Quade, Maximilian Noppel, Kai Reinhard, Jonas Schwab, Rebecca Schwerdt, Tomasz Truderung, Melanie Volkamer, and Cornelia Winter | Fourth International Joint Conference on Electronic
Voting (E-Vote-ID 2019) |
| Using Relational Verification for Program Slicing | Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich | 17th International Conference on Software Engineering and
Formal Methods (SEFM 2019) |
| Understanding Counterexamples for Relational Properties with DIbugger | Mihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, and Bernhard Beckert | Sixth Workshop on Horn Clauses for Verification and Synthesis and
Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019) |
| Seamless Interactive Program Verification | Sarah Grebing, Jonas Klamroth, and Mattias Ulbrich | 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019) |
| VerifyThis – Verification Competition with a Human Factor | Gidon Ernst, Marieke Huisman, Wojciech Mostowski, and Mattias Ulbrich | 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019) |
| Verification-based Test Case Generation for Information-Flow Properties | Mihai Herda, Shmuel Tyszberowicz, Joachim Müssig, and Bernhard Beckert | 34rd Annual ACM Symposium on Applied Computing (SAC 2019) |
| Formal Specification and Verification of Hyperledger Fabric Chaincode | Bernhard Beckert, Mihai Herda, Michael Kirsten, and Jonas Schiffl | 3rd Symposium on Distributed Ledger Technology (SDLT-2018)
co-located with ICFEM 2018: the 20th International Conference
on Formal Engineering Methods |
| A Uniform Information-Flow-Security Benchmark Suite for Source Code and Bytecode | Tobias Hamann, Mihai Herda, Heiko Mantel, Martin Mohr, David Schneider, and Markus Tasch | 23rd Nordic Conference on Secure IT Systems (NordSec 2018) |
| Using Theorem Provers to Increase the Precision of
Dependence Analysis for Information Flow Control | Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning | 20th International Conference on Formal Engineering
Methods - Formal Methods and Software Engineering
(ICFEM 2018) |
| Towards a Notion of Coverage for Incomplete Program-Correctness Proofs | Bernhard Beckert, Mihai Herda, Stefan Kobischke, and Mattias Ulbrich | 8th International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation (ISoLA 2018), Part II: A Broader View on Verification: From Static to Runtime and Back |
| Achieving delta description for the system software of an automated production evolution based on partially inferenced model | Suhyun Cha, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert, and Birgit Vogel‑Heuser | 14th IEEE International Conference on Automation Science and Engineering (CASE 2018) |
| Towards automatic argumentation about voting rules | Michael Kirsten and Olivier Cailloux | 4ème conférence sur les
Applications Pratiques de l'Intelligence
Artificielle (APIA 2018) |
| Adding Text-Based Interaction to a Direct-Manipulation Interface for
Program Verification – Lessons Learned | Sarah Grebing, An Thuy Tien Luong, and Alexander Weigl | 13th International Workshop on User Interfaces for Theorem Provers (UITP 2018) |
| Relational Equivalence Proofs Between Imperative and MapReduce Algorithms | Bernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich, and Alexander Weigl | 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018) |
| Static and Dynamic Verification of Relational Properties
on Self-composed C Code | Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, and Guillaume Petiot | 12th International Conference on Tests and Proofs (TAP 2018) held
as part of STAF 2018: Software Technologies - Applications and
Foundations |
| Using Dependence Graphs to Assist Verification and Testing of Information-Flow Properties | Mihai Herda, Shmuel Tyszberowicz, and Bernhard Beckert | 12th International Conference on Tests and Proofs (TAP 2018) |
| Proving Equivalence Between Imperative and MapReduce
Implementations Using Program Transformations | Bernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich, and Alexander Weigl | Third Workshop on Models for Formal Analysis of Real Systems and
Sixth International Workshop on Verification and Program Transformation
(MARS/VPT@ETAPS 2018) |
| An Interaction Concept for Program Verification
Systems with Explicit Proof Object | Bernhard Beckert, Sarah Grebing, and Mattias Ulbrich | Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017) |
| SemSlice: Exploiting Relational Verification for
Automatic Program Slicing | Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich | 13th International Conference on integrated Formal
Methods (iFM 2017) |
| Modular Verification of Information Flow Security in Component-Based
Systems | Simon Greiner, Martin Mohr, and Bernhard Beckert | 15th International Conference on Software Engineering and Formal Methods
(SEFM 2017) |
| Generalised Test Tables: A Practical Specification Language for Reactive Systems | Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander Weigl | 13th International Conference on integrated Formal Methods (iFM 2017) |
| Formal Fairness Properties in Network Routing
Based on a Resource Allocation Model | Almut Demel and Michael Kirsten | 9th Workshop on Logical Aspects of
Multi-Agent Systems (LAMAS 2017)
affiliated with CSL 2017: the 26th EACSL
Annual Conference on Computer Science Logic |
| A Mechanizable First-Order Theory of Ordinals | Peter H. Schmitt | 26th International Conference on Automated
Reasoning with Analytic Tableaux and Related
Methods (TABLEAUX 2017) |
| Generation of Monitoring Functions in Production
Automation Using Test Specifications | Suhyun Cha, Sebastian Ulewicz, Birgit Vogel‑Heuser, Alexander Weigl, Mattias Ulbrich, and Bernhard Beckert | 15th IEEE International Conference on
Industrial Informatics (INDIN 2017) |
| Proving JDK's Dual Pivot Quicksort Correct | Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt, and Mattias Ulbrich | 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017) |
| Generalized Test Tables: A Powerful and Intuitive
Specification Language for Reactive Systems | Alexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert, and Birgit Vogel‑Heuser | 15th IEEE International Conference on Industrial
Informatics (INDIN 2017) |
| Combining Graph-Based and Deduction-Based Information-Flow Analysis | Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning | 5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017)
affiliated with ETAPS 2017: European Joint Conferences on Theory and
Practice of Software |
| RPP: Automatic Proof of Relational Properties by
Self-composition | Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, and Virgile Prevosto | 23rd International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS 2017)
held as part of ETAPS 2017: European Joint Conferences on
Theory and Practice of Software, Part I |
| Natural Language User Interface For Software Engineering Tasks | Alexander Wachtel, Jonas Klamroth, and Walter F. Tichy | The Tenth International Conference on Advances in
Computer-Human Interactions (ACHI 2016) |
| Computing Exact Loop Bounds for Bounded Program Verification | Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert, and Mana Taghdiri | International Symposium on Dependable Software Engineering:
Theories, Tools, and Applications (SETTA 2017) |
| Automatic Margin Computation for Risk-Limiting Audits | Bernhard Beckert, Michael Kirsten, Vladimir Klebanov, and Carsten Schürmann | First International Joint Conference on Electronic Voting
– formerly known as EVOTE and VoteID (E-Vote-ID 2016) |
| Computing Specification-Sensitive Abstractions for Program Verification | Tianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, and Mana Taghdiri | Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016) |
| Relational Program Reasoning Using Compiler IR | Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich | 8th Working Conference on Verified Software: Theories, Tools, and Experiments
(VSTTE 2016), Revised Selected Papers |
| Deductive Verification of Legacy Code | Bernhard Beckert, Thorsten Bormer, and Daniel Grahl | 7th International Symposium on Leveraging
Applications of Formal Methods, Verification and Validation
(ISoLA 2016), Volume I: Foundational Techniques |
| Sound Probabilistic #SAT with Projection | Vladimir Klebanov, Alexander Weigl, and Jörg Weisbarth | 14th International Workshop on
Quantitative Aspects of Programming Languages and Systems
(QAPL 2016) |
| Practical Detection of Entropy Loss in Pseudo-Random Number Generators | Felix Dörre and Vladimir Klebanov | 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS 2016) |
| Efficient SAT-based Pre-image Enumeration for Quantitative Information Flow in Programs | Alexander Weigl | 5th International Workshop on Quantitative Aspects of Security Assurance (QASA 2016) |
| A Verification-Supported Evolution Approach to Assist
Software Application Engineers in Industrial Factory Automation | Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten, Franziska Wiebe, Bernhard Beckert, and Birgit Vogel‑Heuser | IEEE International Symposium on Assembly and
Manufacturing (ISAM 2016) |
| Automated Verification for Functional and Relational
Properties of Voting Rules | Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and Mattias Ulbrich | Sixth International Workshop on Computational Social Choice (COMSOC 2016) |
| Non-Interference with What-Declassification in Component-Based Systems | Simon Greiner and Daniel Grahl | 29th IEEE Computer Security Foundations Symposium (CSF 2016) |
| A Natural Language Dialog System Based on Active Ontologies | Alexander Wachtel, Jonas Klamroth, and Walter F. Tichy | The Ninth International Conference on Advances in
Computer-Human Interactions (ACHI 2016) |
| A Concept for Multi-Phase Incremental Formal
Verification in Robotic Guided Surgery | Mattias Ulbrich, Luzie Schreiter, Sarah Grebing, Jörg Raczkowsky, Heinz Wörn, and Bernhard Beckert | 4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2015) |
| Regression Verification for Programmable Logic Controller Software | Bernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander Weigl | 17th International Conference on Formal Engineering Methods (ICFEM 2015) |
| Proving Equivalence between Control Software Variants for Programmable Logic Controllers -
Using Regression Verification to Reduce Unneeded Variant Diversity | Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Bernhard Beckert, and Birgit Vogel‑Heuser | 20th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2015) |
| Interactive Theorem Proving - Modelling the User in the Proof Process | Bernhard Beckert and Sarah Grebing | Workshop on Bridging the Gap between Human and Automated Reasoning -
A workshop of the 25th International Conference on Automated Deduction (CADE-25) |
| Selected Challenges of Software Evolution for Automated Production Systems | Birgit Vogel‑Heuser, Stefan Feldmann, Jens Folmer, Matthias Kowal, Ina Schaefer, Jan Ladiges, Alexander Fay, Christopher Haubeck, Winfried Lamersdorf, Sascha Lity, Timo Kehrer, Matthias Tichy, Sinem Getir, Mattias Ulbrich, Vladimir Klebanov, and Bernhard Beckert | 13th IEEE International Conference on Industrial Informatics (INDIN 2015) |
| Regression Verification for Java Using a Secure Information Flow Calculus | Bernhard Beckert, Vladimir Klebanov, and Mattias Ulbrich | 17th Workshop on Formal Techniques for
Java-like Programs (FTfJP 2015) |
| A Hybrid Approach for Proving Noninterference of Java Programs | Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr | 28th IEEE Computer Security Foundations Symposium (CSF 2015) |
| A Theorem Proving Approach to Secure Information Flow in
Concurrent Programs (extended abstract) | Daniel Bruns | Workshop on Foundations of Computer Security (FCS 2015) |
| Pseudo-Random Number Generator Verification: A Case Study | Felix Dörre and Vladimir Klebanov | 7th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2015) |
| Axiomatization of Typed First-Order Logic | Peter H. Schmitt and Mattias Ulbrich | 20th International Symposium on Formal Methods (FM 2015) |
| Poster: Security in E-Voting | Daniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel, and Richard Gay | 36th IEEE Symposium on Security and Privacy (S&P 2015),
Poster Session |
| First-Order Transitive Closure Axiomatization via Iterative Invariant Injections | Aboubakr Achraf El Ghazi, Mana Taghdiri, and Mihai Herda | 7th NASA Formal Methods Symposium (NFM 2015) |
| Automating Regression Verification | Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich | Multikonferenz Software Engineering und Management 2015:
Fachtagung Software Engineering (SE 2015) |
| Dynamic Dispatch for Method Contracts through Abstract Predicates | Wojciech Mostowski and Mattias Ulbrich | 14th International Conference on Modularity (Modularity'15) |
| Generating JML Specifications from Alloy Expressions | Daniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, and Shmuel Tyszberowicz | 10th International Haifa Verification Conference on
Hardware and Software: Verification and Testing (HVC 2014) |
| The KeY Platform for Verification and Analysis of
Java Programs | Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich | 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014) |
| Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender | Florian Böhl, Simon Greiner, and Patrik Scheidecker | 13th International Conference on Cryptology and Network Security (CANS 2014) |
| A Usability Evaluation of Interactive Theorem Provers Using Focus Groups | Bernhard Beckert, Sarah Grebing, and Florian Böhl | 12th International Conference on Software Engineering and Formal Methods
(SEFM 2014) – Collocated Workshops: Human-Oriented Formal Methods (HOFM 2014) |
| Automating Regression Verification | Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich | 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014) |
| How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of
Interactive Theorem Provers | Bernhard Beckert, Sarah Grebing, and Florian Böhl | Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014) |
| Reasoning About Vote Counting Schemes Using
Light-Weight and Heavy-Weight Methods | Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Thomas Meumann | 8th International Verification Workshop (VERIFY 2014)
in connection with IJCAR 2014: International Joint
Conference on Automated Reasoning |
| Poster: Specification and Verification of
Confidentiality in Component-Based Systems | Max E. Kramer, Anton Hergenröder, Martin Hecker, Simon Greiner, and Kaibin Bao | 35th IEEE Symposium on Security
and Privacy, Poster Reception |
| JKelloy: A Proof Assistant for Relational Specifications of Java
Programs | Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, and Mana Taghdiri | 6th NASA Formal Methods Symposium (NFM 2014) |
| A Comparative Study of Incremental Constraint Solving Approaches in
Symbolic Execution | Tianhai Liu, Mateus Araújo, Marcelo d'Amorim, and Mana Taghdiri | 10th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC 2014) |
| Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking | Christoph Gladisch and Shmuel Tyszberowicz | Brazilian Symposium on Formal Methods (SBMF 2013) |
| Privacy Preserving Surveillance and the Tracking-Paradox | Simon Greiner, Pascal Birnstill, Erik Krempel, Bernhard Beckert, and Jürgen Beyerer | 8th Security Research Conference on Future Security |
| Information Flow in Object-Oriented Software | Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich | 23rd International Symposium on Logic-Based Program
Synthesis and Transformation (LOPSTR 2013), Revised
Selected Papers |
| Refinement-based Testing of Delta-oriented Product Lines | Ferruccio Damiani, Christoph Gladisch, and Shmuel Tyszberowicz | International Conference on Principles and Practices of
Programming on the Java Platform: Virtual Machines, Languages,
and Tools (PPPJ 2013) |
| Heuristically Creating Test Cases for Program Verification
Systems | Bernhard Beckert, Thorsten Bormer, and Markus Wagner | 10th Metaheuristics International Conference (MIC 2013) |
| SAT-based Analysis and Quantification of Information Flow in Programs | Vladimir Klebanov, Norbert Manthey, and Christian Muise | 10th International Conference on Quantitative Evaluation of Systems
(QEST 2013) |
| On the Specification and Verification of Voting Schemes | Bernhard Beckert, Rajeev Goré, and Carsten Schürmann | 4th International Conference on E-Voting and Identity (Vote-ID 2013) |
| Reducing the Complexity of Quantified Formulas via Variable Elimination | Aboubakr Achraf El Ghazi, Mattias Ulbrich, Mana Taghdiri, and Mihai Herda | 11th International Workshop on Satisfiability Modulo Theories (SMT 2013) |
| Analysing Vote Counting Algorithms Via Logic -
And its Application to the CADE Election System | Bernhard Beckert, Rajeev Goré, and Carsten Schürmann | 24th International Conference on Automated
Deduction (CADE-24) |
| A Metric for Testing Program Verification Systems | Bernhard Beckert, Thorsten Bormer, and Markus Wagner | Seventh International Conference on Tests and Proofs
(TAP 2013) |
| Dynamic Logic with Trace Semantics | Bernhard Beckert and Daniel Bruns | 24th International Conference on Automated Deduction
(CADE-24) |
| A Hybrid Approach for Proving Noninterference and
Applications to the Cryptographic Verification of Java
Programs | Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Jürgen Graf, and Christoph Scheben | Grande Region Security and Reliability Day (GRSRD 2013) |
| Lessons Learned From Microkernel Verification:
Specification is the New Bottleneck | Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer | Seventh Conference on Systems Software Verification (SSV 2012) |
| Integration of Bounded Model Checking and Deductive Verification | Bernhard Beckert, Thorsten Bormer, Florian Merz, and Carsten Sinz | Formal Verification of Object-Oriented Software
International Conference (FoVeOOS 2011),
Revised Selected Papers |
| Lessons Learned From Microkernel Verification | Bernhard Beckert and Thorsten Bormer | 12th International Workshop on Automated Verification
of Critical Systems (AVOCS 2012) |
| Formal Semantics of Model Fields in Annotation-based
Specifications | Bernhard Beckert and Daniel Bruns | KI 2012: Advances in Artificial Intelligence |
| Precise Quantitative Information Flow Analysis Using Symbolic Model Counting | Vladimir Klebanov | International Workshop on Quantitative Aspects in Security Assurance (QASA 2012) |
| Mind the Gap: Formal Verification and the Common
Criteria | Bernhard Beckert, Daniel Bruns, and Sarah Grebing | 6th International Verification Workshop (VERIFY-2010) |
| Evaluating the Usability of Interactive Verification Systems | Bernhard Beckert and Sarah Grebing | 1st International Workshop on Comparative Empirical
Evaluation of Reasoning Systems (COMPARE 2012) |
| On the Organisation of Program Verification Competitions | Marieke Huisman, Vladimir Klebanov, and Rosemary Monahan | 1st International Workshop on Comparative Empirical Evaluation
of Reasoning Systems (COMPARE 2012) |
| A Proof Assistant for Alloy Specifications | Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, and Mana Taghdiri | 18th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS 2012) |
| Bounded Program Verification Using an SMT Solver: A Case Study | Tianhai Liu, Michael Nagel, and Mana Taghdiri | Fifth IEEE International Conference on Software Testing, Verification
and Validation (ICST 2012) |
| Verlässliche Software fur kritische Infrastrukturen - Preface | Bernhard Beckert and Gregor Snelting | INFORMATIK 2011 Informatik schafft Communities – Beiträge der
41. Jahrestagung der Gesellschaft für Informatik e.V. (GI), Volume P-192 |
| Specification of Red-black Trees: Showcasing Dynamic
Frames, Model Fields and Sequences | Daniel Bruns | 10th KeY Symposium |
| Formal Semantics of Model Fields Inspired by a
Generalization of Hilbert's ε Terms | Bernhard Beckert and Daniel Bruns | 10th KeY Symposium |
| A Dual-Engine for Early Analysis of Critical Systems | Aboubakr Achraf El Ghazi, Ulrich Geilmann, Mattias Ulbrich, and Mana Taghdiri | Workshop on Dependable Software for Critical Infrastructures (DSCI 2011) |
| The 1st Verified Software Competition: Experience Report | Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiß | 17th International Symposium on Formal Methods (FM 2011) |
| A Dynamic Logic for Unstructured Programs with Embedded Assertions | Mattias Ulbrich | International Conference on Formal Verification
of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers |
| Dynamic Frames in Java Dynamic Logic | Peter H. Schmitt, Mattias Ulbrich, and Benjamin Weiß | International Conference on Formal Verification
of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers |
| Proving Memory Separation in a Microkernel by Code Level Verification | Christoph Baumann, Holger Blasum, Thorsten Bormer, and Sergey Tverdyshev | 1st International Workshop on Architectures and Applications for Mixed-Criticality Systems (AMICS 2011) |
| Improving the Usability of Specification Languages and Methods
for Annotation-based Verification | Bernhard Beckert, Thorsten Bormer, and Vladimir Klebanov | 9th International Symposium on Formal Methods for Components and
Objects (FMCO 2010), State-of-the-Art Survey |
| Test Data Generation for Programs with Quantified First-Order
Logic Specifications | Christoph Gladisch | 22nd IFIP WG 6.1 International Conference on Testing Software
and Systems (ICTSS 2010) |
| Towards Testing a Verifying Compiler | Thorsten Bormer and Markus Wagner | Formal Verification of Object-Oriented Software,
Papers presented at the International Conference, Volume KIT-INFO-TR 2010-13 |
| Generating Regression Unit Tests using a Combination of
Verification and Capture & Replay | Bernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz, and Amiram Yehudai | Fourth International Conference on Tests and Proofs (TAP 2010) |
| Verification of Software Product Lines with Delta-Oriented
Slicing | Daniel Bruns, Vladimir Klebanov, and Ina Schaefer | Formal Verification of Object-Oriented Software
(FoVeOOS 2010), Revised Selected Papers |
| Ingredients of Operating System Correctness | Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer | embedded world 2010 Conference |
| Formal Semantics for the Java Modeling Language | Daniel Bruns | Informatiktage 2010, Volume S-9 |
| Satisfiability Solving and Model Generation for Quantified
First-Order Logic Formulas | Christoph Gladisch | International Conference on Formal Verification of Object-Oriented
Software (FoVeOOS 2010), Revised Selected Papers |
| Mind the Gap: Formal Verification and the Common
Criteria | Bernhard Beckert, Daniel Bruns, and Sarah Grebing | 6th International Verification Workshop (VERIFY 2010) |
| On Essential Program Annotations and
Completeness of Verifying Compilers | Bernhard Beckert, Thorsten Bormer, and Vladimir Klebanov | 16th Workshop on Verified Software: Theory, Tools,
and Experiments (VSTTE 2009) |
| Probabilistic Models for the Verification of
Human-Computer Interaction | Bernhard Beckert and Markus Wagner | KI 2009: Advances in Artificial Intelligence, 32nd Annual
German Conference on AI |
| Formal Verification of a Microkernel Used in
Dependable Software Systems | Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer | 28th International Conference on
Computer Safety, Reliability and Security |
| Could we have chosen a better Loop Invariant or Method Contract? | Christoph Gladisch | Third International Conference on Tests and Proofs (TAP 2009) |
| Verifying the PikeOS Microkernel: First Results in the Verisoft XT Avionics Project | Christoph Baumann and Thorsten Bormer | Doctoral Symposium on Systems Software Verification (DS SSV'09) |
| Better Avionics Software Reliability by
Code Verification | Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer | embedded world Conference |
| Verification-based Testing for Full Feasible Branch Coverage | Christoph Gladisch | 6th IEEE International Conference on Software Engineering and Formal Methods (SEFM 08) |
| Privacy Protection in an Electronic Chronicle System | Simon Greiner and Jie Yang | 34th Annual IEEE Northeast Bioengineering Conference (NEBEC 2008) |
| Integrating Verification and Testing of Object-Oriented Software | Christian Engel, Christoph Gladisch, Vladimir Klebanov, and Philipp Rümmer | Second International Conference on Tests and Proofs (TAP 2008) |
| A Dynamic Logic for Deductive Verification of
Concurrent Programs | Bernhard Beckert and Vladimir Klebanov | 5th IEEE International Conference on Software Engineering
and Formal Methods (SEFM 2007) |
| The KeY System 1.0 (Deduction Component) | Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt | 21st International Conference on Automated Deduction (CADE-21) |
| How C differs from Java for Symbolic Program Execution | Christoph Gladisch | C/C++ Verification Workshop |
| White-box Testing by Combining Deduction-based Specification Extraction and
Black-box Testing | Bernhard Beckert and Christoph Gladisch | First International Conference on Tests and Proofs (TAP 2007), Revised Papers |
| KeY: A Formal Method for Object-Oriented Systems | Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt | IFIP International Conference on Formal Methods for
Open Object-Based Distributed Systems (FMOODS 2007) |
| A Dynamic Logic for Deductive Verification of Concurrent Java
Programs With Condition Variables | Bernhard Beckert and Vladimir Klebanov | 1st International Workshop on Verification
and Analysis of Multi-threaded Java-like Programs (VAMP 2007),
Satellite Workshop of CONCUR 2007: the 18th International
Conference on Concurrency Theory |
| Verifying Object-Oriented Programs with KeY: A Tutorial | Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, and Peter H. Schmitt | 5th International Symposium on Formal Methods for Components
and Objects (FMCO 2006), Revised Lectures |
| Integrating Object-oriented Design and Deductive Verification of Software, Tutorial Abstract | Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt | 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006) |
| Dynamic Logic with Non-rigid Functions:
A Basis for Object-oriented Program Verification | Bernhard Beckert and André Platzer | Third International Joint Conference on
Automated Reasoning (IJCAR 2006) |
| A Method for Formalizing, Analyzing, and
Verifying Secure User Interfaces | Bernhard Beckert and Gerd Beuster | Eight International Conference on
Formal Engineering Methods (ICFEM 2006) |
| Must Program Verification Systems and Calculi be Verified? | Bernhard Beckert and Vladimir Klebanov | 3rd International Verification Workshop (VERIFY 2006),
Workshop at Federated Logic Conferences (FLoC) |
| Guaranteeing Consistency in Text-Based Human-Computer Interaction | Bernhard Beckert and Gerd Beuster | International Workshop on Formal Methods
for Interactive Systems (FMIS 2006) |
| An Improved Rule for While Loops in Deductive Program Verification | Bernhard Beckert, Steffen Schlager, and Peter H. Schmitt | Seventh International Conference on
Formal Engineering Methods (ICFEM 2005) |
| Second-Order Principles in Specification Languages
for Object-Oriented Programs | Bernhard Beckert and Kerry Trentelman | 12th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning |
| Reusing Proofs when Program Verification Systems are Modified | Bernhard Beckert, Thorsten Bormer, and Vladimir Klebanov | Software Certificate Management Workshop (SoftCeMent 2005) |
| Verification of JCSP Programs | Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt | 28th WoTUG Conference on Communicating Process Architectures (CPA 2005) |
| Software Verification with Integrated Data Type Refinement
for Integer Arithmetic | Bernhard Beckert and Steffen Schlager | 4th International Conference on Integrated Formal Methods (IFM 2004) |
| Proof Reuse for Deductive Program Verification | Bernhard Beckert and Vladimir Klebanov | 2nd International Conference on Software
Engineering and Formal Methods (SEFM 2004) |
| Formal Specification of Security-relevant Properties
of User Interfaces | Bernhard Beckert and Gerd Beuster | 3rd International Workshop on
Critical Systems Development with UML |
| A JMM-Faithful Non-interference Calculus for Java | Vladimir Klebanov | 4th International Workshop on Scientific Engineering of
Distributed Java Applications (FIDJI 2004) |
| A Program Logic for Handling JAVA CARD's Transaction
Mechanism | Bernhard Beckert and Wojciech Mostowski | 6th International Conference on Fundamental Approaches
to Software Engineering (FASE 2003), held as part of
ETAPS 2003: the Joint European Conferences on Theory
and Practice of Software |
| Program Verification Using Change Information | Bernhard Beckert and Peter H. Schmitt | 1st International Conference on
Software Engineering and Formal Methods (SEFM 2003) |
| The KeY System: Integrating Object-Oriented Design and
Formal Methods | Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, and Peter H. Schmitt | 5th International Conference on Fundamental Approaches to
Software Engineering (FASE 2002) held as part of ETAPS 2002:
the Joint European Conferences on Theory and Practice of
Software |
| Integer Arithmetic in the Specification and
Verification of Java Programs | Bernhard Beckert and Steffen Schlager | Workshop on Tools for System Design and
Verification (FM-TOOLS 2002) |
| Translating the Object Constraint Language into First-order
Predicate Logic | Bernhard Beckert, Uwe Keller, and Peter H. Schmitt | VERIFY Workshop (VERIFY 2002) at FLoC 2002: Federated Logic
Conferences |
| A Sequent Calculus for First-order Dynamic Logic with
Trace Modalities | Bernhard Beckert and Steffen Schlager | First International Joint Conference on
Automated Reasoning (IJCAR 2001) |
| Handling Java's Abrupt Termination in a Sequent Calculus
for Dynamic Logic | Bernhard Beckert and Bettina Sasse | IJCAR Workshop on Precise Modelling and
Deduction for Object-oriented Software Development (PMD '01) |
| A Dynamic Logic for the Formal Verification of
Java Card Programs | Bernhard Beckert | International Workshop on Java on Smart Cards:
Programming and Security (Java Card 2000),
Revised Papers |
| An Extension of Dynamic Logic for Modelling
OCL's @pre Operator | Thomas Baar, Bernhard Beckert, and Peter H. Schmitt | Fourth Andrei Ershov International
Conference on Perspectives of System Informatics |
| The KeY Approach: Integrating Object Oriented
Design and Formal Verification | Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. Schmitt | European Workshop on Logics in Artificial Intelligence
(JELIA 2000) |
| The 2-SAT Problem of Regular Signed CNF Formulas | Bernhard Beckert, Reiner Hähnle, and Felip Manyà | 30th IEEE International Symposium on Multiple-Valued
Logic (ISMVL 2000) |
| The KeY Approach: Integrating Object Oriented
Design and Formal Verification | Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. Schmitt | 4th Workshop on Tools for System Design and
Verification (FM-TOOLS 2000) |
| Depth-first Proof Search without Backtracking for
Free-variable Clausal Tableaux | Bernhard Beckert | Third International Workshop on First-Order Theorem
Proving (FTP 2000) |
| The KeY Approach: Integrating
Design and Formal Verification of Java Card Programs | Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. Schmitt | Java Card Workshop (JCW 2000) |
| A Dynamic Logic for Java Card | Bernhard Beckert | 2nd ECOOP Workshop on Formal Techniques for
Java Programs |
