KIT - Application-oriented Formal Verification

Institute of Information Security and Dependability (KASTEL) – Application-oriented Formal Verification

Rather group by categories.

2025
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). Software Engineering Methodologies
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). Specification and Verification

2024
Title	Author(s)	Source
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)
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	Karlsruher Institut für Technologie (KIT)
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
A Delta-Oracle for Fast Model Merge Conflict Estimation using Sketch-Based Critical Pair Analysis	Karl Kegel, Andreas Domanowski, Kevin Feichtinger, Romain Pascual, and Uwe Aßmann	Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems
Towards Formalizing and Relating Different Notions of Consistency in Cyber-Physical Systems Engineering	Kevin Feichtinger, Karl Kegel, Romain Pascual, Uwe Aßmann, Bernhard Beckert, and Ralf Reussner	Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems

2023
Title	Author(s)	Source
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
Transformations de graphes décorés	Pascale Le Gall and Romain Pascual	Informatique Mathématique Une photographie en 2023
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
Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY	Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, and Wolfgang Ahrendt	Int. J. Softw. Tools Technol. Transf. 25(2)
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	Formal Aspects Comput. 35(3)
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

2022
Title	Author(s)	Source
Inference of graph transformation rules for the design of geometric modeling operations	Romain Pascual	Université Paris-Saclay
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
The Karlsruhe Java Verification Suite	Jonas Klamroth, Florian Lanzinger, Wolfram Pfeifer, and Mattias Ulbrich	The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday
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 topological operations on generalized maps: Application to subdivision schemes	Romain Pascual, Hakim Belhaouari, Agnès Arnould, and Pascale Le Gall	Graphics and Visual Computing 6
Formal Specification and Verification of JDK’s Identity Hash Map Implementation (Long Version)	Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, and Alexander Weigl	Karlsruhe Institute of Technology (KIT) 1000145727
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
Preserving consistency in geometric modeling with graph transformations	Agnès Arnould, Hakim Belhaouari, Thomas Bellet, Pascale Le Gall, and Romain Pascual	Mathematical Structures in Computer Science 32(3)
Topological consistency preservation with graph transformation schemes	Romain Pascual, Pascale Le Gall, Agnès Arnould, and Hakim Belhaouari	Science of Computer Programming 214
The counterSharp Model Counting Benchmark	Samuel Teuber and Alexander Weigl	Karlsruhe Institute of Technology 2022-02
Formal Methods for Trustworthy Voting Systems	Michael Kirsten	Karlsruhe Institute of Technology (KIT) (January 2022)
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

2021
Title	Author(s)	Source
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)
Formal Specification and Verification for Automated Production Systems	Alexander Sebastian Weigl	Karlsruhe Institute of Technology (KIT) (December 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)
Scalability and Precision by Combining Expressive Type Systems and Deductive Verification	Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, and Werner Dietl	Proceedings of the ACM on programming languages 5(OOPSLA)
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
Table-based formal specification approaches for control engineers—empirical studies of usability	Suhyun Cha, Birgit Vogel‑Heuser, Alexander Weigl, Mattias Ulbrich, and Bernhard Beckert	IET Cyber-Physical Systems: Theory and Applications
Card-Based Cryptography Meets Formal Verification	Alexander Koch, Michael Schrempp, and Michael Kirsten	New Generation Computing 39(1)
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
Property Types in Java: Combining Type Systems and Deductive Verification	Florian Lanzinger	Karlsruher Institut für Technologie (February 2021)
Modeling and Verifying Access Control for Ethereum Smart Contracts	Frederik Reiche, Jonas Schiffl, Bernhard Beckert, Robert Heinrich, and Ralf Reussner	Karlsruher Institut für Technologie (KIT) 1000129607
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
Reconstructing Z3 Proofs With KeY	Wolfram Pfeifer	Karlsruhe Institute of Technology (January 2021)

2020
Title	Author(s)	Source
Integration of Static and Dynamic Analysis Techniques for Checking Noninterference	Bernhard Beckert, Mihai Herda, Michael Kirsten, and Shmuel Tyszberowicz	Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Part V: Integration of Verification Techniques
Usability Recommendations for User Guidance in Deductive Program Verification	Sarah Grebing and Mattias Ulbrich	Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Part IV: Feasibility and Usability
Formal Analysis of Smart Contracts: Applying the KeY System	Jonas Schiffl, Wolfgang Ahrendt, Bernhard Beckert, and Richard Bubel	Deductive Software Verification: Future Perspectives
Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY	Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, and Mattias Ulbrich	Lecture Notes in Computer Science 12345 (Springer 2020)
The VerifyThis Collaborative Long Term Challenge	Marieke Huisman, Raúl Monti, Mattias Ulbrich, and Alexander Weigl	Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY, Part IV: Feasibility and Usability
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
Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der Informatik	Michael Kirsten, Robert Bauer, Andreas Fried, Bernhard Beckert, Michael Beigl, Gregor Snelting, and Martina Zitterbart	Campustage 2020 „Lehre^Forschung-PLUS“
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)
An Incremental Abstraction Scheme for Solving Hard SMT-Instances over Bit-Vectors	Samuel Teuber, Marko Kleine Büning, and Carsten Sinz	CoRR abs/2008.10061
VerifyThis Long-term Challenge 2020: Proceedings of the Online-Event	Marieke Huisman, Raúl E. Monti, Mattias Ulbrich, and Alexander Weigl	Institut für Theoretische Informatik (ITI), KIT 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)
Combining Static and Dynamic Program Analysis Techniques for Checking Relational Properties	Mihai Herda	Karlsruhe Institute of Technology (KIT) (January 2020)

2019
Title	Author(s)	Source
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
Card-Based Cryptography Meets Formal Verification	Alexander Koch, Michael Schrempp, and Michael Kirsten	IACR Cryptology ePrint Archive 2019(1037)
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
KASTEL Industry 4.0 Demonstrator: Provably Forgetting Information in PLC software	Alexander Weigl	Presentation in the KASTEL Seminar, Karlsruhe, Germany, October 10
User Interaction in Deductive Interactive Program Verification	Sarah Caecilia Grebing	Karlsruhe Institute of Technology (October 2019)
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)
Relational properties for specification and verification of C programs in Frama-C	Lionel Blatter	Université Paris-Saclay (September 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)
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning	Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos, and Mattias Ulbrich	abs/1907.03523 2019
Seamless Interactive Program Verification	Sarah Grebing, Jonas Klamroth, and Mattias Ulbrich	11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)
Formal Verification of Evolutionary Changes	Bernhard Beckert, Jakob Mund, Mattias Ulbrich, and Alexander Weigl	Managed Software Evolution
Using Relational Verification for Program Slicing	Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich	Department of Informatics, Karlsruhe Institute of Technology 2019,5
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)
Modular Verification of JML Contracts Using Bounded Model Checking	Jonas Klamroth	Karlsruhe Institute of Technology (March 2019)
Efficient unpacking of required software from CERNVM-FS	Samuel Teuber	Zenodo 2019-02
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)
Learning from Evolution for Evolution	Stefan Kögel, Matthias Tichy, Abhishek Chakraborty, Alexander Fay, Birgit Vogel‑Heuser, Christopher Haubeck, Gabriele Taentzer, Timo Kehrer, Jan Ladiges, Lars Grunske, Mattias Ulbrich, Safa Bougouffa, Sinem Getir, Suhyun Cha, Udo Kelter, Winfried Lamersdorf, Kiana Busch, Robert Heinrich, and Sandro Koch	Managed Software Evolution
Addressed Challenges	Reiner Jung, Lukas Märtin, Jan Ole Johanssen, Barbara Paech, Malte Lochau, Thomas Thüm, Kurt Schneider, Matthias Tichy, and Mattias Ulbrich	Managed Software Evolution

2018
Title	Author(s)	Source
Specification and Verification of Hyperledger Fabric Chaincode	Jonas Schiffl	Karlsruhe Institute of Technology (December 2018)
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)
Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPU	Suhyun Cha, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert, and Birgit Vogel‑Heuser	Automatisierungstechnik Special Issue
Trends in Relational Program Verification	Bernhard Beckert and Mattias Ulbrich	Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday
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)
Efficient Verification of Programs with Complex Data Structures Using SMT Solvers	Tianhai Liu	Karlsruhe Institute of Technology (July 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)
Automating Regression Verification of Pointer Programs by Predicate Abstraction	Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich	Formal Methods in System Design 52(3)
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)
Debugging Program Verification Proof Scripts (Tool Paper)	Bernhard Beckert, Sarah Grebing, and Alexander Weigl	CoRR abs/1804.04402
A Framework for Non-Interference in Component-Based Systems	Simon Greiner	Karlsruhe Institute of Technology (April 2018)
A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification	Florian Lanzinger	Karlsruher Institut für Technologie (April 2018)
Program Equivalence (Dagstuhl Seminar 18151)	Shuvendu K. Lahiri, Andrzej Murawski, Ofer Strichman, and Mattias Ulbrich	Dagstuhl Reports 8(4)
Experience Report: Formal Methods in Material Science	Bernhard Beckert, Britta Nestler, Moritz Kiefer, Michael Selzer, and Mattias Ulbrich	CoRR abs/1802.02374
Self-composition to Prove Relational Properties in Annotated C Program	Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, and Virgile Prevosto	CoRR abs/1801.06876
Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPU	Suhyun Cha, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert, and Birgit Vogel‑Heuser	Automatisierungstechnik 66(10)

2017
Title	Author(s)	Source
Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems	Max E. Kramer, Martin Hecker, Simon Greiner, Kaibin Bao, and Kateryna Yurchenko	Department of Informatics, Karlsruhe Institute of Technology 2017,12
VerifyThis 2017: A Program Verification Competition	Marieke Huisman, Rosemary Monahan, Wojciech Mostowski, Peter Müller, and Mattias Ulbrich	Karlsruhe Institute of Technology 2017,10
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)
An Introduction to Voting Rule Verification	Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Carsten Schürmann	Trends in Computational Social Choice, Part II: Techniques
A novel model-based testing approach for software product lines	Ferruccio Damiani, David Faitelson, Christoph Gladisch, and Shmuel Tyszberowicz	Software and System Modeling 16(4)
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)
Relational Program Reasoning Using Compiler IR – Combining Static Verification and Dynamic Analysis	Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich	Journal of Automated Reasoning 60(3)
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
RIFL 1.1: A Common Specification Language for Information-Flow Requirements	Thomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider, and Markus Tasch	TU Darmstadt TUD-CS-2017-0225
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)
Modular Verification of Information Flow Security in Component-Based Systems – Proofs and Proof of Concept	Simon Greiner, Martin Mohr, and Bernhard Beckert	Department of Informatics, Karlsruhe Institute of Technology 2017,9
Specifying and Verifying Real-World Java Code with KeY - Case Study java.math.BigInteger	Wolfram Pfeifer	Karlsruhe Institute of Technology (May 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
CoCoME with Security	Simon Greiner and Mihai Herda	Department of Informatics, Karlsruhe Institute of Technology 2017,2
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)

2016
Title	Author(s)	Source
Dynamic Logic for Java	Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß	Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations
Deductive Software Verification - The KeY Book: From Theory to Practice	Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich	Lecture Notes in Computer Science 10001 (Springer 2016)
Formal Verification with KeY: A Tutorial	Bernhard Beckert, Reiner Hähnle, Martin Hentschel, and Peter H. Schmitt	Deductive Software Verification - The KeY Book: From Theory to Practice, Part IV: The KeY System in Action
Proof-based Test Case Generation	Wolfgang Ahrendt, Christoph Gladisch, and Mihai Herda	Deductive Software Verification - The KeY Book: From Theory to Practice, Part III: From Verification to Analysis
First-Order Logic	Peter H. Schmitt	Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations
Theories	Peter H. Schmitt and Richard Bubel	Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations
Formal Specification with the Java Modeling Language	Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, and Martin Hentschel	Deductive Software Verification - The KeY Book: From Theory to Practice, Part II: Specification and Verification
Functional Verification and Information Flow Analysis of an Electronic Voting System	Daniel Grahl and Christoph Scheben	Deductive Software Verification - The KeY Book: From Theory to Practice, Part V: Case Studies
Information Flow Analysis	Christoph Scheben and Simon Greiner	Deductive Software Verification - The KeY Book: From Theory to Practice, Part III: From Verification to Analysis
Using the KeY Prover	Wolfgang Ahrendt and Sarah Grebing	Deductive Software Verification - The KeY Book: From Theory to Practice, Part IV: The KeY System in Action
From Specification to Proof Obligations	Daniel Grahl and Mattias Ulbrich	Deductive Software Verification - The KeY Book: From Theory to Practice, Part II: Specification and Verification
Modular Specification and Verification	Daniel Grahl, Richard Bubel, Wojciech Mostowski, Peter H. Schmitt, Mattias Ulbrich, and Benjamin Weiß	Deductive Software Verification - The KeY Book: From Theory to Practice, Part II: Specification and Verification
Proof Search with Taclets	Philipp Rümmer and Mattias Ulbrich	Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations
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: Extended Version	Felix Dörre and Vladimir Klebanov	Department of Informatics, Karlsruhe Institute of Technology 2016,12
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)
Dynamic Dispatch for Method Contracts through Abstract Predicates	Wojciech Mostowski and Mattias Ulbrich	Transactions on Modularity and Composition 1
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)
Deductive Verification with Relational Properties	Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, and Virgile Prevosto	CoRR abs/1606.00678
Non-Interference with What-Declassification in Component-Based Systems	Simon Greiner and Daniel Grahl	29th IEEE Computer Security Foundations Symposium (CSF 2016)
Dual Pivot Quicksort: Specification and Verification Using KeY	Jonas Schiffl	Karlsruhe Institute of Technology (May 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)
Praxis der Forschung: Eine Lehrveranstaltung des forschungsnahen Lehrens und Lernens in der Informatik am KIT	Matthias Budde, Sarah Grebing, Erik Burger, Max Kramer, Bernhard Beckert, Michael Beigl, and Ralf Reussner	Neues Handbuch Hochschullehre 74, Volume A: Lehren und Lernen, Part 3: Neue Lehr- und Lernkonzepte
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	Poster at the 25th USENIX Security Symposium

2015
Title	Author(s)	Source
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)
Non-Interference with What-Declassification in Component-Based Systems	Daniel Grahl and Simon Greiner	Department of Informatics, Karlsruhe Institute of Technology 2015,10
Deductive Verification of Concurrent Programs and its Application to Secure Information Flow for Java	Daniel Grahl	Karlsruhe Institute of Technology (October 2015)
Relational Reasoning - Constraint Solving, Deduction, and Program Verification	Aboubakr Achraf El Ghazi	Karlsruhe Institute of Technology (October 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)
Privacy Preserving Surveillance: An Interdisciplinary Approach	Pascal Birnstill, Sebastian Bretthauer, Simon Greiner, and Erik Krempel	International Data Privacy Law 5(4)
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)
Regression Verification for Programmable Logic Controller Software	Bernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander Weigl	Karlsruhe Institute of Technology, Department of Informatics 2015-06
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
A Hybrid Approach for Proving Noninterference of Java Programs	Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr	IACR Cryptology ePrint Archive 2015(438)
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)
Specifying linked data structures in JML for combining formal verification and testing	Christoph Gladisch and Shmuel Tyszberowicz	Science of Computer Programming 107–108
Deductive Verification of Concurrent Programs	Daniel Bruns	Department of Informatics, Karlsruhe Institute of Technology 2015-3
Regression Verification for Programmable Logic Controller Software	Alexander Sebastian Weigl	Karlsruhe Institute of Technology (January 2015)

2014
Title	Author(s)	Source
Formal Verification of Voting Schemes	Michael Kirsten	ITI Beckert, Karlsruhe Institute of Technology (December 2014)
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)
Advancing Deductive Program-Level Verification for Real-World Application: Lessons Learned from an Industrial Case Study	Thorsten Bormer	Karlsruhe Institute of Technology (October 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)
Bedrohungsanalyse eines Smart-Home-Szenarios zur Visualisierung von Energieverbrauchsdaten im Vorfeld einer Steuerentscheidung	Anton Hergenröder, Christian Haas, Roland Bless, Denise Dudek, Martina Zitterbart, Thomas Bräuchle, Oliver Raabe, Simon Greiner, Bernhard Beckert, Kaibin Bao, and Hartmut Schmeck	Institute of Telematics, Karlsruhe Institute of Technology TM-2014-1
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)
Formal Verification of an Electronic Voting System	Daniel Bruns	Department of Informatics, Karlsruhe Institute of Technology 2014-11
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
Formal Specification with JML	Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel	Department of Informatics, Karlsruhe Institute of Technology 2014-10
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)
Verifying Voting Schemes	Bernhard Beckert, Rajeev Goré, Carsten Schürmann, Thorsten Bormer, and Jian Wang	Journal of Information Security and Applications (JISA) 19(2)
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	Universität Trier
Precise Quantitative Information Flow Analysis – A Symbolic Approach	Vladimir Klebanov	Theoretical Computer Science 538(0)
On Verifying Relational Specifications of Java Programs with JKelloy	Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, and Mana Taghdiri	Department of Informatics, Karlsruhe Institute of Technology 2014,3
Towards Specification and Verification of Information Flow in Concurrent Java-like Programs	Daniel Bruns	Department of Informatics, Karlsruhe Institute of Technology 2014-5
Reasoning and Verification: State of the Art and Current Trends	Bernhard Beckert and Reiner Hähnle	Intelligent Systems, IEEE 29(1)
Generating Bounded Counterexamples for KeY Proof Obligations	Mihai Herda	Karlsruhe Institute of Technology (January 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)

2013
Title	Author(s)	Source
Information Flow in Object-Oriented Software – Extended Version –	Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich	Department of Informatics, Karlsruhe Institute of Technology 2013-14
Proving Well-Definedness of JML Specifications with KeY	Michael Kirsten	ITI Schmitt, Karlsruhe Institute of Technology (November 2013)
Implementation-level verification of algorithms with KeY	Daniel Bruns, Wojciech Mostowski, and Mattias Ulbrich	International Journal on Software Tools for Technology Transfer (STTT) 17(6)
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)
Secure Information Flow for Java – A Dynamic Logic Approach: Extended Version	Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich	Department of Informatics, Karlsruhe Institute of Technology 2013-10
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)
Dynamic Logic for an Intermediate Language: Verification, Interaction and Refinement	Mattias Ulbrich	Karlsruhe Institute of Technology (June 2013)
A Dynamic Logic for Deductive Verification of Multi-Threaded Programs	Bernhard Beckert and Vladimir Klebanov	Formal Aspects of Computing 25(3)
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)
VerifyThis Verification Competition 2012 – Organizer's Report	Marieke Huisman, Vladimir Klebanov, and Rosemary Monahan	Department of Informatics, Karlsruhe Institute of Technology 2013-01

2012
Title	Author(s)	Source
Wirtschaftlichkeit bei der Verbesserung von Systemspezifikationen durch UML-Modellierung	Thomas Lauscher and Simon Greiner	Signal und Draht 104(12)
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
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected Papers	Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov	Lecture Notes in Computer Science 7421 (Springer 2012)
Dynamic Trace Logic: Definition and Proofs	Bernhard Beckert and Daniel Bruns	Department of Informatics, Karlsruhe Institute of Technology 2012-10
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)
The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study	Bernhard Beckert, Daniel Bruns, Ralf Küsters, Christoph Scheben, Peter H. Schmitt, and Tomasz Truderung	Department of Informatics, Karlsruhe Institute of Technology 2012-8
Evaluating and Improving the Usability of Interactive Verification Systems	Sarah Grebing	Universität Koblenz-Landau (August 2012)
Mind the Gap: Formal Verification and the Common Criteria	Bernhard Beckert, Daniel Bruns, and Sarah Grebing	6th International Verification Workshop (VERIFY-2010)
1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012)	Vladimir Klebanov, Bernhard Beckert, Armin Biere, and Geoff Sutcliffe	CEUR Workshop Proceedings 873 (CEUR-WS.org 2012)
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)
Model generation for quantified formulas with application to test data generation	Christoph Gladisch	International Journal on Software Tools for Technology Transfer (STTT) 14(4)
Eine formale Semantik für die Java Modeling Language	Daniel Bruns	Informatik-Spektrum 35(1)
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)
10th International Symposium on Formal Methods for Components and Objects (FMCO 2011), State-of-the-Art Survey	Bernhard Beckert, Ferruccio Damiani, Frank de Boer, and Marcello Bonsangue	Lecture Notes in Computer Science 7542 (Springer 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)

2011
Title	Author(s)	Source
On Proving Alloy Specifications using KeY	Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, and Mana Taghdiri	Department of Informatics, Karlsruhe Institute of Technology 2011,37
Papers Presented at the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011)	Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov	Karlsruhe Institute of Technology, Department of Informatics 2011-26
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
KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit Testing	Bernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz, and Amiram Yehudai	International Journal of Systems Assurance Engineering and Management 2(2)
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
Software Security in Virtualized Infrastructures – The Smart Meter Example (Software-Sicherheit in virtualisierten Infrastrukturen – Das Beispiel der intelligenten Stromzähler)	Bernhard Beckert, Dennis Hofheinz, Jörn Müller‑Quade, Alexander Pretschner, and Gregor Snelting	it - Information Technology 53(3)
Verification-based software-fault detection	Christoph David Gladisch	Karlsruhe Institute of Technology (May 2011)
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)
Verification-based Software-fault Detection	Christoph Gladisch	Karlsruhe Institute of Technology (February 2011)
International Conference on Formal Verification of Object-Oriented Software International Conference (FoVeOOS 2010), Revised Selected Papers	Bernhard Beckert and Claude Marché	Lecture Notes in Computer Science 6528 (Springer 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

2010
Title	Author(s)	Source
Software Security in Virtualized Infrastructures – The Smart Meter Example	Bernhard Beckert, Dennis Hofheinz, Jörn Müller‑Quade, Alexander Pretschner, and Gregor Snelting	Karlsruhe Institute of Technology 2010-20
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)
Dynamic Frames in Java Dynamic Logic: Formalisation and Proofs	Peter H. Schmitt, Mattias Ulbrich, and Benjamin Weiß	Department of Computer Science, Karlsruhe Institute of Technology 2010-11
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
Deduktion: Von der Theorie zur Anwendung	Franz Baader, Bernhard Beckert, and Tobias Nipkow	Informatik-Spektrum 33(5)
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)
Satisfiability Solving and Model Generation for Quantified First-order Logic Formulas	Christoph Gladisch	Fakultät für Informatik, Institut für Theoretische Informatik, ITI
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
Verification of Software Product Lines: Reducing the Effort with Delta-oriented Slicing and Proof Reuse	Daniel Bruns, Vladimir Klebanov, and Ina Schaefer	Department of Informatics, Karlsruhe Institute of Technology 2010-13
Special Issue on Tests and Proofs	Bernhard Beckert and Reiner Hähnle	Journal of Automated Reasoning 45(4)
Deductive Verification of a Byzantine Agreement Protocol	Roman Krenický and Mattias Ulbrich	Karlsruhe Institute of Technology, Department of Informatics 2010-7
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
Deductive Verification of System Software in the Verisoft XT Project	Bernhard Beckert and Michal Moskal	KI 24(1)
Papers Presented at the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)	Bernhard Beckert and Claude Marché	Karlsruhe Institute of Technology, Department of Informatics 2010-13
Practical Aspects of Automated Deduction for Program Verification	Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, and Philipp Rümmer	KI 24(1)
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)

2009
Title	Author(s)	Source
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)
Formal Semantics for the Java Modeling Language	Daniel Bruns	Universität Karlsruhe (June 2009)
Extending the Reach and Power of Deductive Program Verification	Vladimir Klebanov	Universität Koblenz-Landau (June 2009)
Better Avionics Software Reliability by Code Verification	Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer	embedded world Conference

2008
Title	Author(s)	Source
Verification-based Testing for Full Feasible Branch Coverage	Christoph Gladisch	6th IEEE International Conference on Software Engineering and Formal Methods (SEFM 08)
Elektronische Wahlen: Theoretisch möglich, praktisch undemokratisch	Daniel Bruns	FIfF-Kommunikation 25(3)
Verification-based Test Case Generation with Loop Invariants and Method Specifications	Christoph Gladisch	University of Koblenz-Landau
Extending KeY for the Verification of C Programs	Christoph Gladisch	VDM Verlag 2008
Second International Conference on Tests and Proofs (TAP 2008)	Bernhard Beckert and Reiner Hähnle	Lecture Notes in Computer Science 4966 (Springer 2008)
5th International Verification Workshop (VERIFY '08) co-located with IJCAR 2008: the 4th International Joint Conference on Automated Reasoning	Bernhard Beckert and Gerwin Klein	CEUR Workshop Proceedings 372 (CEUR-WS.org 2008)
Editorial: Special Section on Software Engineering and Formal Methods	Bernhard K. Aichernig and Bernhard Beckert	Software and System Modeling 7(3)
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)

2007
Title	Author(s)	Source
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
A Fixpoint-based Rule for Loop Verification	Daniel Bruns	Universität Karlsruhe (June 2007)
Preface: Special Issue on Automated Reasoning with Analytic Tableaux and Related Methods	Bernhard Beckert and Lawrence C. Paulson	Journal of Automated Reasoning 38(1-3)
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)
4th International Verification Workshop (VERIFY '07) co-located with CADE-21: the 21st Conference on Automated Deduction	Bernhard Beckert	CEUR Workshop Proceedings 259 (CEUR-WS.org 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
Verification of Object-Oriented Software: The KeY Approach	Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt	Lecture Notes in Computer Science 4334 (Springer 2007)
Dynamic Logic	Bernhard Beckert, Vladimir Klebanov, and Steffen Schlager	Verification of Object-Oriented Software: The KeY Approach, Part I: Foundations
Formal Specification	Andreas Roth and Peter H. Schmitt	Verification of Object-Oriented Software: The KeY Approach, Part II: Expressing and Formalising Requirements
Proof Reuse	Vladimir Klebanov	Verification of Object-Oriented Software: The KeY Approach, Part III: Using the KeY System
Software Verification for Java 5	Mattias Ulbrich	Fakultät für Informatik, Universität Karlsruhe (January 2007)

2006
Title	Author(s)	Source
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)
Intelligent Systems and Formal Methods in Software Engineering	Bernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, and Sriram K. Rajamani	IEEE Intelligent Systems 21(6)
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)

2005
Title	Author(s)	Source
14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2005)	Bernhard Beckert	Lecture Notes in Computer Science 3702 (Springer 2005)
Third International Conference on Software Engineering and Formal Methods (SEFM 2005)	Bernhard K. Aichernig and Bernhard Beckert	IEEE Computer Society 2005
The KeY Tool	Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt	Software and System Modeling 4(1)
Email Client Verification Goals	Bernhard Beckert and Gerd Beuster	Verisoft Project #46
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
Refinement and Retrenchment for Programming Language Data Types	Bernhard Beckert and Steffen Schlager	Formal Aspects of Computing 17(4)
Reusing Proofs when Program Verification Systems are Modified	Bernhard Beckert, Thorsten Bormer, and Vladimir Klebanov	Software Certificate Management Workshop (SoftCeMent 2005)
TABLEAUX 2005: Position Papers and Tutorial Descriptions	Bernhard Beckert	Universität Koblenz-Landau 12–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)
Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen Synthese	Mattias Ulbrich	Fakultät für Informatik, Universität Karlsruhe (January 2005)

2004
Title	Author(s)	Source
Software Verification with Integrated Data Type Refinement for Integer Arithmetic	Bernhard Beckert and Steffen Schlager	4th International Conference on Integrated Formal Methods (IFM 2004)
Taclets: A New Paradigm for Constructing Interactive Theorem Provers	Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen Schlager	Department of Computer Science, University of Koblenz 9-2004
Email Client Specification	Bernhard Beckert, Gerd Beuster, and Pia Breuer	Verisoft Project #6
Taclets: A New Paradigm for Constructing Interactive Theorem Provers	Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen Schlager	Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales, Serie A: Matemáticas (RACSAM) 98(1)
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	Department of Computer Science, University of Koblenz 10-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)

2003
Title	Author(s)	Source
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
The KeY Tool	Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt	Department of Computing Science, Chalmers University and Göteborg University, Göteborg, Sweden No. 2003-5
Depth-first Proof Search without Backtracking for Free-variable Clausal Tableaux	Bernhard Beckert	Journal of Symbolic Computation 36(1-2)
Program Verification Using Change Information	Bernhard Beckert and Peter H. Schmitt	1st International Conference on Software Engineering and Formal Methods (SEFM 2003)

2002
Title	Author(s)	Source
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

2001
Title	Author(s)	Source
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)
Free-variable Tableaux for Propositional Modal Logics	Bernhard Beckert and Rajeev Goré	Studia Logica 69(1)
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
IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development (PMD '01)	Bernhard Beckert, Robert France, Reiner Hähnle, and Bart Jacobs	Technical Report DII 07/01, Dipartimento di Ingegneria dell'Informazione, Università degli Studi di Siena 2001
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

2000
Title	Author(s)	Source
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)
The SAT Problem of Signed CNF Formulas	Bernhard Beckert, Reiner Hähnle, and Felip Manya	Labelled Deduction
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
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	University of Karlsruhe, Department of Computer Science 2000/4

Publications

Rather group by categories.