Search for my publications at: DBLP - Google Scholar

To appear
Titel Autor Quelle


2017
Titel Autor Quelle
Automatic Margin Computation for Risk-Limiting Audits

Bernhard Beckert, Michael Kirsten, Vladimir Klebanov, Carsten Schürmann

12th International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
An Interaction Concept for Program Verification Systems with Explicit Proof Object

Bernhard Beckert, Sarah Grebing, Mattias Ulbrich

13th Haifa Verification Conference (HVC 2017)
Generalised Test Tables: A Practical Specification Language for Reactive Systems

Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl

International Conference on Integrated Formal Methods (iFM 2017)
SemSlice: Exploiting Relational Verification for Automatic Program Slicing

Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, Mattias Ulbrich

International Conference on Integrated Formal Methods (iFM 2017)
Generation of Monitoring Functions in Production Automation Using Test Specifications

Suhyun Cha, Sebastian Ulewicz, Birgit Vogel-Heuser, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert

15th IEEE International Conference on Industrial Informatics (INDIN 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, Birgit Vogel-Heuser

15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Modular Verification of Information Flow Security in Component-Based Systems

Simon Greiner, Martin Mohr, Bernhard Beckert

15th International Conference on Software Engineering and Formal Methods (SEFM 2017)
Computing Exact Loop Bounds for Bounded Program Verification

Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert, Mana Taghdiri

International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017)
An Introduction to Voting Rule Verification

Bernhard Beckert, Thorsten Bormer, Rajeev Gore, Michael Kirsten, Carsten Schürmann

Trends in Computational Social Choice
Proving JDK's Dual Pivot Quicksort Correct

Bernhard Beckert, Jonas Schiffl, Peter H. Schmitt, Mattias Ulbrich

9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)
Combining Graph-Based and Deduction-Based Information-Flow Analysis

Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, Marko Kleine Büning

5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017)
Modular Verification of Information Flow Security in Component-Based Systems: Proofs and Proof of Concept

Simon Greiner, Martin Mohr, Bernhard Beckert

Karlsruhe Reports in Informatics


2016
Titel Autor Quelle
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 (eds.)

Springer, LNCS 10001, Springer Link
Dynamic Logic for Java

Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß

Deductive Software Verification - The KeY Book, Springer, LNCS 10001, Springer Link
Formal Verification with KeY: A Tutorial

Bernhard Beckert, Reiner Hähnle, Martin Hentschel, and Peter H. Schmitt

Deductive Software Verification - The KeY Book, Springer, LNCS 10001, Springer Link
Computing Specification-Sensitive Abstractions for Program Verification

Tianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, Mana Taghdiri

Symposium on Dependable Software Engineering (SETTA 2016), LNCS 9984. Springer Link
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), LNCS 9952. Springer Link
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, Birgit Vogel-Heuser

IEEE International Symposium on Assembly and Manufacturing (ISAM 2016), IEEEXplore
Automated Verification for Functional and Relational Properties of Voting Rules

Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, Mattias Ulbrich

Sixth International Workshop on Computational Social Choice (COMSOC 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


2015
Titel Autor Quelle
Regression Verification for Programmable Logic Controller Software

Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl

17th International Conference on Formal Engineering Methods (ICFEM 2015), LNCS 9407. Springer Link
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), IEEEXplore
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. CEUR Workshop Proceedings, Vol. 1412
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, Bernhard Beckert

13th IEEE International Conference on Industrial Informatics (INDIN 2015), IEEEXplore
Regression Verification for Programmable Logic Controller Software

Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexander Weigl

Karlsruhe Reports in Informatics, Vol. 2015-6
Security in E-Voting (Poster)

Daniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel, Richard Gay

36th IEEE Symposium on Security and Privacy, 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

28th IEEE Computer Security Foundations Symposium (CSF 2015), IEEEXplore
A Hybrid Approach for Proving Noninterference of Java Programs

Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr

Cryptology ePrint Archive, Report 2015/438
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), ACM Digital Library
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)


2014
Titel Autor Quelle
Verifying Voting Schemes

Bernhard Beckert, Rajeev Goré, Carsten Schürmann, Thorsten Bormer, and Jian Wang

Journal of Information Security and Applications
Reasoning and Verification: State of the Art and Current Trends

Bernhard Beckert and Reiner Hähnle

IEEE Intelligent Systems, IEEEXplore
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, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich

6th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2014
A Usability Evaluation of Interactive Theorem Provers Using Focus Groups

Bernhard Beckert, Sarah Grebing, and Florian Böhl

Workshop on Human-Oriented Formal Methods, HOFM 2014. Revised Selected Papers, LNCS 8938. Springer Link
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

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
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, LNCS 8901. Springer Link


2013
Titel Autor Quelle
Information Flow in Object-Oriented Software. Extended Version

Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich

Karlsruhe Reports in Informatics, Vol. 2013-14
On the Specification and Verification of Voting Schemes

Bernhard Beckert, Rajeev Gore, and Carsten Schürmann

4th International Conference on E-Voting and Identity, Vote-ID 2013, LNCS 7985. Springer Link
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)
Privacy Preserving Surveillance and the Tracking Paradox

Simon Greiner, Pascal Birnstill, Erik Krempel, Bernhard Beckert, and Jürgen Beyerer

Future Security Conference 2013
Heuristically Increasing the Axiomatization Coverage of Program Verification Systems

Bernhard Beckert, Thorsten Bormer, and Markus Wagner

10th Metaheuristics International Conference
Analysing Vote Counting Algorithms Via Logic. And its Application to the CADE Election System

Bernhard Beckert, Rajeev Gore, and Carsten Schürmann

24th International Conference on Automated Deduction, LNCS 7898. Springer Link
Dynamic Logic with Trace Semantics

Bernhard Beckert and Daniel Bruns

24th International Conference on Automated Deduction, LNCS 7898. Springer Link
A Metric for Testing Program Verification Systems

Bernhard Beckert, Thorsten Bormer, and Markus Wagner

7th International Conference on Tests and Proofs, TAP 2013, LNCS 7985. Springer Link
A Dynamic Logic for Deductive Verification of Multi-threaded Programs

Bernhard Beckert and Vladimir Klebanov

Formal Aspects of Computing, Springer Link
Formal Methods for Components and Objects

Bernhard Beckert, Feruccio Damiani, Frank de Boer, and Marcello Bonsangue (eds.)

10th International Symposium on Formal Methods for Components and Objects, FMCO 2011. State-of-the-Art Survey
Springer-Verlag, LNCS 7542


2012
Titel Autor Quelle
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)
Lessons Learned From Microkernel Verification

Bernhard Beckert and Thorsten Bormer

AVOCS 2012: International Workshop on Automated Verification of Critical Systems
Formal Semantics of Model Fields in Annotation-based Specifications

Bernhard Beckert and Daniel Bruns

KI 2012: Advances in Artificial Intelligence
Springer-Verlag, LNCS 7526
Integration of Bounded Model Checking and Deductive Verification

Bernhard Beckert, Thorsten Bormer, Florian Merz, and Carsten Sinz

Revised Selected Papers, Formal Verification of Object-Oriented Programs (FoVeOOS 2011)
Springer-Verlag, LNCS 7421
Formal Verification of Object-Oriented Software

Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov (eds.)

International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011.
Revised Selected Papers
Springer-Verlag, LNCS 7421
Evaluating the Usability of Interactive Verification Systems

Bernhard Beckert and Sarah Grebing

1st International Workshop, COMPARE 2012
Comparative Empirical Evaluation of Reasoning Systems

Vladimir Klebanov, Bernhard Beckert, Armin Biere, and Geoff Sutcliffe (eds.)

1st International Workshop, COMPARE 2012
Dynamic Trace Logic: Definition and Proofs

Bernhard Beckert and Daniel Bruns

Karlsruhe Institute of Technology, Technical Report Vol. 2012-10
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

Karlsruhe Institute of Technology, Technical Report Vol. 2012-8
Mind the Gap: Formal Verification and the Common Criteria

Bernhard Beckert, Daniel Bruns, Sarah Grebing

6th International Verification Workshop, VERIFY-2010, Edinburgh, United Kingdom, July 20-21 2010. Discussion paper.


2011
Titel Autor Quelle
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)
Lecture Notes in Informatics (LNI) P-192
KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit Testing

Bernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz, Amiram Yehudai

International Journal of Systems Assurance Engineering and Management (IJSAEM)
SpringerLink
Improving the Usability of Specification Languages and Methods for Annotation-based Verification

Bernhard Beckert, Thorsten Bormer, Vladimir Klebanov

9th International Symposium on Formal Methods for Components and Objects, FMCO 2010 – "State-of-the-Art Survey"
Springer Verlag, LNCS 6957
Formal Verification of Object-Oriented Software

Bernhard Beckert, Ferruccio Damiani, Dilian Gurov (eds.)

Papers Presented at the 2nd International Conference, October 5-7, 2011, Turin, Italy
Software Security in Virtualized Infrastructures – The Smart Meter Example

Bernhard Beckert, Dennis Hofheinz, Jörn Müller-Quade, Alexander Pretschner, Gregor Snelting

it - Information Technology
Formal Verification of Object-Oriented Software

Bernhard Beckert, Claude Marché (eds.)

International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010.
Revised Selected Papers
Springer-Verlag, LNCS 6528
LNCS 6528 Cover


2010
Titel Autor Quelle
Special Issue on Tests and Proofs

Bernhard Beckert, Reiner Hähnle (eds.)

Journal of Automated Reasoning,
Springer-Verlag, JAR
Software Security in Virtualized Infrastructures - The Smart Meter Example Bernhard Beckert, Dennis Hofheinz, Jörn Müller-Quade, Alexander Pretschner, Gregor Snelting Karlsruhe Institute of Technology, Technical Report Vol. 2010-20
Deduktion: Von der Theorie zur Anwendung

Franz Baader, Bernhard Beckert, Tobias Nipkow

Informatik-Spektrum, Volume 33, Issue 5 (2010)
SpringerLink
Formal Verification of Object-Oriented Software

Bernhard Beckert, Claude Marché (eds.)

Papers Presented at the International Conference, June 28-30, 2010, Paris, France
Generating Regression Unit Tests using a Combination of Verification and Capture & Replay

Bernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz, Amiram Yehudai

International Conference on Tests and Proofs (TAP 2010)
Ingredients of Operating System Correctness Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer embedded world 2010 Conference, Nuremberg, Germany
Deductive Verification of System Software in the VerisoftXT Project Bernhard Beckert, Michal Moskal KI Journal,
SpringerLink
Practical Aspects of Automated Deduction for Program Verification Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer KI Journal,
SpringerLink


2009
Titel Autor Quelle
Formal Verification of a Microkernel Used in Dependable Software Systems Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer 28th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2009)
Probabilistic Models for the Verification of Human-Computer Interaction Bernhard Beckert, Markus Wagner 32nd Annual German Conference on AI (KI 2009)
Better Avionics Software Reliability by Code Verification Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer embedded world Conference 2009


2008
Titel Autor Quelle
5th International Verification Workshop Bernhard Beckert, Gerwin Klein (eds.) Proceedings VERIFY 2008
Special Section on Software Engineering and Formal Methods Bernhard Aichernig, Bernhard Beckert (eds.) Software and System Modelling (Springer Journal),
Springer-Verlag, SoSyM
Tests and Proofs Bernhard Beckert, Reiner Hähnle (eds.) Proceedings of the Second International Conference (TAP 2008),
Springer Verlag, LNCS 4966
LNCS 4966 Cover
Tests and Proofs Bernhard Beckert, Reiner Hähnle (eds.) Papers presented at the Second International Conference that were not included in the main proceedings


2007
Titel Autor Quelle
A Dynamic Logic for Deductive Verification of Concurrent Programs Bernhard Beckert, Vladimir Klebanov 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007)
A Dynamic Logic for Deductive Verification of Concurrent Java Programs with Condition Variables Bernhard Beckert, Vladimir Klebanov 1st International Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP 2007)
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 (post proceedings)
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 International Conference on Automated Deduction (CADE 2007), Springer-Verlag, LNCS 4603
White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing Bernhard Beckert, Christoph Gladisch International Conference on Tests and Proofs (TAP 2007),
Springer-Verlag, LNCS 4454
4th International Verification Workshop Bernhard Beckert (ed.) Proceedings (VERIFY 2007)
KeY: A Formal Method for Object-Oriented Systems
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt 9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS 2007),
Springer-Verlag, LNCS 4468
Special Issue on Automated Reasoning with Tableaux and Related Methods Bernhard Beckert, Lawrence Paulson (eds.) Journal of Automated Reasoning,
Springer-Verlag, JAR
Verification of Object-Oriented Software: The KeY Approach Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (eds.) 15 chapters and 2 appendices, xxix + 658pp,
Springer-Verlag, LNCS 4334
LNAI 4334 Cover
The KeY Book, Chapter 3, Dynamic Logic Bernhard Beckert, Vladimir Klebanov, Steffen Schlager In: Verification of Object-Oriented Software: The KeY Approach,
Springer-Verlag, LNCS 4334


2006
Titel Autor Quelle
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, Sriram K. Rajamani IEEE Intelligent Systems,
IEEE Intelligent Systems
A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces Bernhard Beckert, Gerd Beuster International Conference on Formal Engineering Methods (ICFEM 2006),
Springer Verlag, LNCS 4260
Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program Verification Bernhard Beckert, Andre Platzer International Joint Conference on Automated Reasoning (IJCAR 2006),
Springer Verlag, LNCS 4130
Integrating Object-Oriented Design and Deductive Verification of Software Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt Abstract of a Tutorial held at SEFM 2006, Pune, India, 11-15 September 2006 Proceedings, 4th IEEE International Conference on Software Engineering and Formal Methods
Guaranteeing Consistency in Text-Based Human-Computer Interaction Bernhard Beckert, Gerd Beuster International Workshop on Formal Methods for Interactive Systems (FMIS 2006)
Must Program Verification Systems and Calculi be Verified? Bernhard Beckert, Vladimir Klebanov 3rd International Verification Workshop (Verify 2006)


2005
Titel Autor Quelle
Refinement and Retrenchment for Programming Language Data Types Bernhard Beckert, Steffen Schlager Formal Aspects of Computing (Springer Journal)
Second-Order Principles in Specification Languages for Object-Oriented Programs Bernhard Beckert, Kerry Trentelman 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning(LPAR 2005),
Springer Verlag, LNCS 3835
An Improved Rule for While Loops in Deductive Program Verification Bernhard Beckert, Steffen Schlager, Peter H. Schmitt Seventh International Conference on Formal Engineering Methods (ICFEM 2005),
Springer Verlag, LNCS 3785
Reusing Proofs when Program Verification Systems are Modified Bernhard Beckert, Thorsten Bormer, and Vladimir Klebanov Software Certificate Management Workshop (SoftCeMent 2005), Long Beach, CA, USA.
Automated Reasoning with Analytic Tableaux and Related Methods Bernhard Beckert (ed.) Proceedings of the International Conference (TABLEAUX 2005) ,
Springer Verlag, LNCS 3702
LNAI 3702 Cover
Software Engineering and Formal Methods Bernhard Aichernig, Bernhard Beckert (eds.) Proceedings of the 3rd IEEE International Conference (SEFM 2005),
IEEE CS Digital Library
SEFM 2005 Proceedings Cover
The KeY Tool Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, Peter H. Schmitt Software and System Modeling (Springer Journal)
TABLEAUX 2005: Position Papers and Tutorial Descriptions Bernhard Beckert (ed.) Department of Computer Science, University of Koblenz, Technical Report in Computer Science (Fachberichte Informatik) No. 12-2005, September 2005.
Email Client Verification Goals Bernhard Beckert, Gerd Beuster Verisoft Project, Internal Technical Report #46, 2005


2004
Titel Autor Quelle
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 (RACSAM Journal)
Proof Reuse for Deductive Program Verification Bernhard Beckert and Vladimir Klebanov Software Engineering and Formal Methods (SEFM 2004)
Software Verification with Integrated Data Type Refinement for Integer Arithmetic Bernhard Beckert and Steffen Schlager International Confrence on Integrated Formal Methods (IFM 2004)
Formal Specification of Security-relevant Properties of User Interfaces Bernhard Beckert and Gerd Beuster 3rd International Workshop on Critical Systems Development with UML (CSD-UML 2004), Lisbon, Portugal
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, Technical Report in Computer Science (Fachberichte Informatik) No. 9-2004, September 2004
Formal Specification of Security-relevant Properties of User-Interfaces Bernhard Beckert and Gerd Beuster Department of Computer Science, University of Koblenz, Technical Report in Computer Science (Fachberichte Informatik) No. 10-2004, September 2004
Email Client Specification Bernhard Beckert, Gerd Beuster, and Pia Breuer Verisoft Project, Internal Technical Report #6, 2004


2003
Titel Autor Quelle
Program Verification Using Change Information Bernhard Beckert and Peter H. Schmitt Software Engineering and Formal Methods (SEFM 2003)
Depth-first Proof Search without Backtracking for Free-variable Clausal Tableaux Bernhard Beckert Journal of Symbolic Computation
A Program Logic for Handling Java Card's Transaction Mechanism Bernhard Beckert and Wojciech Mostowski Fundamental Approaches to Software Engineering (FASE 2003),
Springer-Verlag, LNCS 2621
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, Technical Report in Computing Science No. 2003-5, February 2003


2002
Titel Autor Quelle
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 Fundamental Approaches to Software Engineering (FASE 2002),
Springer Verlag, LNCS 2306
Translating the Object Constraint Language into First-order Predicate Logic Bernhard Beckert, Uwe Keller, and Peter H. Schmitt VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen, Denmark
Integer Arithmetic in the Specification and Verification of Java Programs Bernhard Beckert and Steffen Schlager 5th Workshop on Tools for System Design and Verification (FM-TOOLS 2002), Günzburg, Germany


2001
Titel Autor Quelle
An Extension of Dynamic Logic for Modelling OCL's @pre Operator Thomas Baar, Bernhard Beckert, and Peter H. Schmitt Fourth Andrei Ershov International Conference, Perspectives of System Informatics (PSI 2001),
Springer Verlag, LNCS 2244
Free-variable Tableaux for Propositional Modal Logics Bernhard Beckert & Rajeev Goré Studia Logica
A Sequent Calculus for First-order Dynamic Logic with Trace Modalities Bernhard Beckert and Steffen Schlager International Joint Conference on Automated Reasoning (IJCAR 2001),
Springer Verlag, LNCS 2083
A Dynamic Logic for the Formal Verification of Java Card Programs Bernhard Beckert Java on Smart Cards: Programming and Security. Revised Papers, Java Card 2000, International Workshop, Cannes, 2000,
Springer Verlag, LNCS 2041
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 2001), Siena, Italy
Precise Modelling and Deduction for Object-oriented Software Development Bernhard Beckert, Robert France, Reiner Hähnle, and Bart Jacobs (eds.) Proceedings of the PMD Workshop at IJCAR, Siena, Italy


2000
Titel Autor Quelle
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 Logics in Artificial Intelligence (JELIA 2000),
Springer Verlag, LNCS 1919
Depth-first Proof Search without Backtracking for Free-variable Clausal Tableaux Bernhard Beckert International Workshop on First-Order Theorem Proving (FTP 2000)
The 2-SAT Problem of Regular Signed CNF Formulas Bernhard Beckert, Reiner Hähnle, Felip Manya International Symposium on Multiple-valued Logic (ISMVL 2000),
IEEE Press
Chapter on The SAT Problem of Signed CNF Formulas Bernhard Beckert, Reiner Hähnle, & Felip Manya Springer Verlag, Applied Logic Series 17
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), Cannes, France
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 (FMTOOLS 2000), Reisensburg, Germany
A Dynamic Logic for Java Card Bernhard Beckert 2nd ECOOP Workshop on Formal Techniques for Java Programs, Cannes, France
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, Peter H. Schmitt University of Karlsruhe, Department of Computer Science, Technical Report 2000/4, January 2000


1999
Titel Autor Quelle
PhD Thesis (Dissertation)
English title:
Tableau-based Theorem Proving: A Univied View. Integrating and Unifying Methods of Tableau-based Theorem Proving
Bernhard Beckert
German title:
Integration und Uniformierung von Methoden des tableaubasierten Theorembeweisens

Note: My PhD thesis was originally written in English (completed in 1998) but its German translation is the official version submitted to the university. If you are interested in Chapter 5 on deterministic proof procedures, you should better read my paper that was published in 2003 in the Journal of Symbolic Computation (PDF).

Bernhard Beckert
Chapter on Equality and Other Theories Bernhard Beckert Handbook of Tableau Methods
Springer Verlag
Transformations between Signed and Classical Clause Logic Bernhard Beckert, Reiner Hähnle, Felip Manya International Symposium on Multiple-valued Logic (ISMVL 1999)
Proof Transformations from Search-oriented into Interaction-oriented Tableau Calculi Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckert Journal of Universal Computer Science
A Survey of Signed CNF Formulas Bernhard Beckert, Reiner Hähnle, & Felip Manya Many-valued Logics for Computer Science Applications, Symposium affiliated with International Congress of Logic, Methodology and Philosophy of Science, Cracow, Poland
Depth-first Proof Search without Backtracking for Free Variable Semantic Tableaux Bernhard Beckert Position Papers, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Saratoga Spring, USA
Proof Confluent Tableau Calculi Reiner Hähnle & Bernhard Beckert Abstract of a Tutorial. Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Saratoga Spring, USA
Springer Verlag, LNCS 1617


1998
Titel Autor Quelle
Simplification of Many-valued Logic Formulas Using Anti-Links Bernhard Beckert, Reiner Hähnle, Gonzalo Excalada-Imaz Journal of Logic and Computation
Analytic Tableaux
Bernhard Beckert & Reiner Hähnle Chapter 1 in volume I. of Automated Deduction - A Basis for Applications
Editors: Wolfgang Bibel and Peter H. Schmitt,
Springer Verlag, Applied Logic Series , Vol. 8/9/10
Rigid E-Unification Bernhard Beckert Chapter 8 in volume I. of Automated Deduction - A Basis for Applications
Editors: Wolfgang Bibel and Peter H. Schmitt
Springer Verlag, Applied Logic Series , Vol. 8/9/10
Integrating Automated and Interactive Theorem Proving Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, & Peter H. Schmitt Chapter 4 in volume II. of Automated Deduction - A Basis for Applications
Editors: Wolfgang Bibel and Peter H. Schmitt.
Springer Verlag, Applied Logic Series , Vol. 8/9/10
System Description: leanK 2.0 Bernhard Beckert & Rajeev Goré International Conference on Automated Deduction (CADE), Lindau, Germany
Springer Verlag, LNCS 1421
A Tableau Calculus for Quantifier-free Set Theoretic Formulae Bernhard Beckert & Ulrike Hartmer International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, Springer Verlag, LNCS 1397
Fibring Semantic Tableaux Bernhard Beckert & Dov Gabbay International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, Springer Verlag, LNCS 1397
leanK 2.0: Description for the Comparison of Theorem Provers for Modal Logics Bernhard Beckert & Rajeev Goré International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, Springer Verlag, LNCS 1397
Transformations between Signed and Classical Clause Logic Bernhard Beckert, Reiner Hähnle, & Felip Manya First International Workshop on Labelled Deduction, Freiburg, Germany
Transformations between Signed and Classical Clause Logic Bernhard Beckert, Reiner Hähnle, & Felip Manya Many-valued Logics for Computer Applications 1998, Workshop/Conference of COST Action 15, Middle East Technical University, Anakara, Turkey
Integrating Automated and Interactive Theorem Proving Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, & Peter H. Schmitt Workshop on Integration of Deductive Systems at CADE-15, Lindau, Germany, 1998


1997
Titel Autor Quelle
Free Variable Tableaux for Propositional Modal Logics Bernhard Beckert & Rajeev Goré International Conference on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1997), Pont-a-Mousson, France
Springer Verlag, LNCS 1227
Semantic Tableaux with Equality Bernhard Beckert Journal of Logic and Computation, Vol. 7, No. 1, pages 38-58
Fast Subsumption Checks Using Anti-Links Anavai Ramesh, Neil Murray, Bernhard Beckert & Reiner Hähnle Journal of Automated Reasoning, Vol. 18, No. 1, pages 47-83
Simplification of many-valued logic formulas using anti-links Bernhard Beckert, Reiner Hähnle, & Gonzalo Escalada-Imaz Many-valued Logics for Computer Applications 1997, Workshop of Working Group 2, COST Action 15, Department of Mathematics, University of Malaga, Malaga, Spain
Simplification of Many-Valued Logic Formulas Using Anti-Links Bernhard Beckert, Reiner Hähnle, & Gonzalo Escalada-Imaz Technical Report
University of Karlsruhe, Department of Computer Science, TR 11/97.
Also available as: Spanish Scientific Research Council, Institut d'Investigacio en Intelligencia Artificial, Technical Report IIIA-98/03.
Free Variable Tableaux for Propositional Modal Logics Bernhard Beckert & Rajeev Goré Long version of paper at TABLEAUX'97, Technical Report,
University of Karlsruhe, Department of Computer Science, TR 41/96.
Also available as: Australian National University, Automated Reasoning Project, TR-ARP-2-97.


1996
Titel Autor Quelle
Logic Programming as a Basis for Lean Automated Deduction Bernhard Beckert & Joachim Posegga Journal of Logic Programming, Vol. 28, No. 3, pages 231-236
The Tableau-based Theorem Prover 3TAP, Version 4.0 Bernhard Beckert, Reiner Hähnle, Peter Oel & Martin Sulzmann 13th International Conference on Automated Deduction (CADE), New Brunswick, NJ, USA
Incremental Theory Reasoning Methods for Semantic Tableaux Bernhard Beckert & Christian Pape 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1996), Terrasini, Palermo, Italy
Extending Hyper Tableaux with Rigid E-Unification Peter Baumgartner, Bernhard Beckert & Michael Kühn Workshop Deduktion, 20. Jahrestagung für künstliche Intelligenz (KI), Dresden, Germany. Internal Report, TU Dresden
Proving Compiler Correctness with Evolving Algebra Specifications Bernhard Beckert & Reiner Hähnle University of Karlsruhe, Department of Computer Science, TR 4/96
Incremental Theory Reasoning Methods for Semantic Tableaux Bernhard Beckert & Christian Pape Preliminary version of paper at TABLEAUX'96, Technical Report,
University of Karlsruhe, Department of Computer Science, TR 2/96


1995
Titel Autor Quelle
leanTAP: Lean Tableau-based Deduction Bernhard Beckert & Joachim Posegga Journal of Automated Reasoning, Vol. 15, No. 3, pages 339-358
Deduction by Combining Semantic Tableaux and Integer Programming Bernhard Beckert & Reiner Hähnle Annual Conference of the European Association for Computer Science Logic (CSL 1995), Paderborn, Germany
leanEA: A lean Evolving Algebra Compiler Bernhard Beckert & Joachim Posegga Annual Conference of the European Association for Computer Science Logic (CSL 1995), Paderborn, Germany
leanEA: A Poor Man's Evolving Algebra Compiler Bernhard Beckert, Joachim Posegga Logik in der Informatik, 3. Jahrestagung der GI-Fachgruppe, Karlsruhe, Germany. Internal Report, University of Karlsruhe
Proceeedings
leanEA: A Lean Evolving Algebra Compiler Bernhard Beckert & Joachim Posegga 11th Logic Programming Workshop, Wien, Austria
Anti-Links for Boolean Function Manipulation Bernhard Beckert, Reiner Hänle, Neil Murray & Anavai Ramesh KI-95 Activities: Workshops, Posters, Demos. Workshop "Computational and Propositional Logic" at KI-95, Bielefeld. Gesellschaft für Informatik.
Propositional Non Clausal Deduction and Diagnosis Anavai Ramesh, Neil Murray, Bernhard Beckert & Reiner Hänle KI-95 Activities: Workshops, Posters, Demos. Workshop "Computational and Propositional Logic" at KI-95, Bielefeld. Gesellschaft für Informatik.
leanEA: A Poor Man's Evolving Algebra Compiler Bernhard Beckert & Joachim Posegga Logik in der Informatik - 3. Jahrestagung der GI-Fachgruppe 0.1.6, Karlsruhe.
leanEA: A Poor Man's Evolving Algebra Compiler Bernhard Beckert & Joachim Posegga Long version of paper at CSL'95, Technical Report,
University of Karlsruhe, Department of Computer Science, TR 25/95
Fast Subsumption Checks Using Anti-Links Anavai Ramesh. Neil Murray. Bernhard Beckert & Reiner Hähnle Preliminary version of paper in JAR, Technical Report,
University of Karlsruhe, Department of Computer Science, TR 24/95


1994
Titel Autor Quelle
A Completion-Based Method for Mixed Universal and Rigid E-Unification Bernhard Beckert 12th International Conference on Automated Deduction(CADE), Nancy, France
leanTAP: Lean Tableau-Based Theorem Proving Bernhard Beckert & Joachim Posegga 12th International Conference on Automated Deduction (CADE), Nancy, France
Adding Equality to Semantic Tableaux Bernhard Beckert 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1994), Abingdon, UK
On Anti-Links Bernhard Beckert, Reiner Hähnle, Neil Murray, & Anavai Ramesh 5th International Conference on Logic Programming and Automated Reasoning (LPAR), Kiev, Ukraine
Using Mixed Universal and Rigid E-Unification to Handle Equality in Universal Formula Semantic Tableaux Bernhard Beckert Adding Equality to Theorem Provers, Workshop of the DFG-Schwerpunkt "Deduktion", Leipzig
Logic Programming as a Basis for Lean Deduction: Achieving Maximal Efficiency from Minimal Means Bernhard Beckert & Joachim Posegga 10th Logic Programming Workshop, Zürich, Switzerland
Using E-Unification to Handle Equality in Universal Formula Semantic Tableaux Bernhard Beckert Theory Reasoning in Automated Deduction, Workshop at CADE-12, Nancy, France
Lean Theorem Proving: Maximal Efficiency from Minimal Means (Position Paper) Bernhard Beckert & Joachim Posegga Working Notes, AISB Workshop "Automated Reasoning: Closing the Gap between Theory and Practice", Leeds, UK
Tableaubasiertes prädikatenlogisches Beweisen mit Mixed integer programming Bernhard Beckert, Reiner Hähnle, Klaus Ries, & Peter H. Schmitt Beiträge zum DFG-Kolloquium im Rahmen des Schwerpunktprogramms "Deduktion".
In German.
The lean-FAQ: Frequently Asked Quesiton about lean Bernhard Beckert & Joachim Posegga


1993
Titel Autor Quelle
The Even More Liberalized Delta-Rule in Free Variable Semantic Tableaux Bernhard Beckert, Reiner Hähnle, & Peter H. Schmitt 3rd Kurt Goedel Colloquium (KGC), Brno, Czech Republic
A Completion-Based Method for Adding Equality to Free Variable Semantic Tableaux Bernhard Beckert 2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1993), Marseille, France
The Many-Valued Tableau-Based Theorem Prover Reiner Hähnle, Bernhard Beckert, & Stefan Gerberding Handbook
University of Karlsruhe, Department of Computer Science, TR 30/94; 3rd edition
Diploma Thesis:
Ein vervollständigungsbasiertes Verfahren zur Behandlung von Gleichheit im Tableaukalkül mit freien Variablen
Bernhard Beckert Diplomarbeit, Fakultät für Informatik, Universität Karlsruhe.
In German.


1992
Titel Autor Quelle
An Improved Method for Adding Equality to Free Variable Semantic Tableaux Bernhard Beckert & Reiner Hähnle 11th International Conference on Automated Deduction (CADE 1992), Albany/NY, USA.
The Many-Valued Tableau-Based Theorem Prover 3TAP (System Abstract) Bernhard Beckert, Stefan Gerberding, Reiner Hähnle, & Werner Kernig 11th International Conference on Automated Deduction (CADE), Albany/NY, USA.


1991
Titel Autor Quelle
Konzeption und Implementierung von Gleichheit für einen tableau-basierten Theorembeweiser Bernhard Beckert Science Center, Institute for Knowledge Based Systems, IBM Germany (IKBS Technical Report)
In German.


1990
Titel Autor Quelle
Gedicht-Generator - Ein Anwendungsbeispiel für natürlichsprachliche Texterzeugung Bernhard Beckert, Alexander Bell, & Peter Sanders Aus Neugier wird Wissenschaft, Illustrierte Teilnehmerbeiträge aus 25 Jahren Jugend forscht