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) |
BibTeX
Abstract
Preprint PDF
|
| An Interaction Concept for Program Verification
Systems with Explicit Proof Object |
Bernhard Beckert, Sarah Grebing, Mattias Ulbrich |
13th Haifa Verification Conference (HVC 2017) |
BibTeX
Abstract
Preprint PDF
|
| 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) |
BibTeX
Abstract
Preprint PDF
|
| 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) |
BibTeX
Abstract
Preprint PDF
|
| 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) |
BibTeX
Abstract
|
| 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) |
BibTeX
Abstract
|
| 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) |
BibTeX
Abstract
Preprint PDF
|
| 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) |
BibTeX
Abstract
Preprint PDF
|
| An Introduction to Voting Rule Verification |
Bernhard Beckert, Thorsten Bormer, Rajeev Gore,
Michael Kirsten, Carsten Schürmann |
Trends in Computational Social Choice |
BibTeX
Abstract
Preprint PDF
|
| 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) |
BibTeX
Abstract
|
| 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) |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
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 |
BibTeX
Abstract
More info
|
| Dynamic Logic for Java |
Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß |
Deductive Software Verification - The KeY Book, Springer, LNCS 10001,
Springer Link |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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) |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
|
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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| Regression Verification for Programmable Logic Controller Software |
Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexander Weigl |
Karlsruhe Reports in Informatics, Vol. 2015-6 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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) |
BibTeX
Abstract
PDF
|
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 |
BibTeX
Abstract
Preprint PDF
|
| Reasoning and Verification: State of the Art and Current Trends |
Bernhard Beckert and Reiner Hähnle |
IEEE Intelligent Systems, IEEEXplore |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
|
| 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 |
BibTeX
Abstract
PDF
|
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 |
BibTeX
Abstract
PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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) |
BibTeX
Abstract
PDF
|
| Privacy Preserving Surveillance and the Tracking Paradox |
Simon Greiner, Pascal Birnstill, Erik Krempel, Bernhard Beckert,
and Jürgen Beyerer |
Future Security Conference 2013 |
BibTeX
Abstract
Preprint PDF
|
| Heuristically Increasing the Axiomatization Coverage of
Program Verification Systems |
Bernhard Beckert, Thorsten Bormer, and Markus Wagner |
10th Metaheuristics International Conference |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| Dynamic Logic with Trace Semantics |
Bernhard Beckert and Daniel Bruns |
24th International Conference on Automated Deduction, LNCS 7898. Springer Link |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| A Dynamic Logic for Deductive Verification of Multi-threaded Programs |
Bernhard Beckert and Vladimir Klebanov |
Formal Aspects of Computing,
Springer Link |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
|
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) |
BibTeX
Abstract
PDF
|
| Lessons Learned From Microkernel Verification |
Bernhard Beckert and Thorsten Bormer |
AVOCS 2012: International Workshop on Automated Verification of Critical Systems |
BibTeX
Abstract
Preprint PDF
|
| Formal Semantics of Model Fields in Annotation-based
Specifications |
Bernhard Beckert and Daniel Bruns |
KI 2012: Advances in Artificial Intelligence
Springer-Verlag, LNCS 7526 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
Preprint PDF
|
| 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 |
BibTeX
Abstract
|
| Evaluating the Usability of Interactive Verification Systems |
Bernhard Beckert and Sarah Grebing |
1st International Workshop,
COMPARE 2012 |
BibTeX
Abstract
PDF
|
| Comparative Empirical Evaluation of Reasoning Systems |
Vladimir Klebanov, Bernhard Beckert, Armin Biere, and Geoff Sutcliffe (eds.) |
1st International Workshop,
COMPARE 2012 |
BibTeX
PDF
|
| Dynamic Trace Logic: Definition and Proofs |
Bernhard Beckert and Daniel Bruns |
Karlsruhe Institute of Technology, Technical Report Vol. 2012-10 |
BibTeX
Abstract
PDF
|
| 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 |
BibTeX
Abstract
PDF
|
| 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. |
BibTeX
Abstract
Preprint PDF
|
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 |
BibTeX
|
| 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 |
BibTeX
Draft PDF
|
| 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 |
BibTeX
Draft PDF
|
| 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 |
PDF
BibTeX
Abstract
|
| 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
|
Abstract
Online PDF
Bibtex
|
| 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 |
BibTeX
Abstract
|
 |
2010
| Titel |
Autor |
Quelle |
|
| Special Issue on Tests and Proofs |
Bernhard Beckert, Reiner Hähnle (eds.) |
Journal of Automated Reasoning,
Springer-Verlag, JAR |
Draft PDF (Preface)
BibTeX
Abstract
|
| 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 |
PDF
BibTeX
Abstract
|
|
Deduktion: Von der Theorie zur Anwendung |
Franz Baader, Bernhard Beckert, Tobias Nipkow |
Informatik-Spektrum, Volume 33, Issue 5 (2010)
SpringerLink
|
Draft PDF
BibTeX
|
| Formal Verification of Object-Oriented Software |
Bernhard Beckert, Claude Marché (eds.) |
Papers Presented at the International Conference, June 28-30, 2010, Paris, France |
PDF
BibTeX
Abstract
|
|
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)
|
Draft PDF
BibTeX
Abstract |
| Ingredients of Operating System Correctness |
Christoph Baumann, Bernhard Beckert, Holger Blasum,
Thorsten Bormer |
embedded world 2010 Conference,
Nuremberg, Germany |
Draft PDF
BibTeX
Abstract
|
| Deductive Verification of System Software in the VerisoftXT Project |
Bernhard Beckert, Michal Moskal |
KI Journal,
SpringerLink |
Draft PDF
BibTeX
Abstract
|
| Practical Aspects of Automated Deduction for Program Verification |
Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer |
KI Journal,
SpringerLink |
Draft PDF
BibTeX
Abstract |
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) |
PDF (preliminary version)
BibTeX
Abstract |
| 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) |
PDF
BibTeX
Abstract |
| 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) |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract
|
| 4th International Verification Workshop |
Bernhard Beckert (ed.) |
Proceedings (VERIFY 2007) |
Online at CEUR-WS.org
PDF (table of contents)
BibTeX
Abstract |
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 |
PDF (preliminary version)
BibTeX
Abstract |
| Special Issue on Automated Reasoning with Tableaux and Related Methods |
Bernhard Beckert, Lawrence Paulson (eds.) |
Journal of Automated Reasoning,
Springer-Verlag, JAR |
BibTeX
Abstract |
| 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 |
Table of Contents (PDF)
BibTeX
Book Website
|
 |
| 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 |
PDF
BibTeX
|
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 |
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
BibTeX
Abstract |
| Guaranteeing Consistency in Text-Based Human-Computer Interaction |
Bernhard Beckert, Gerd Beuster |
International Workshop on Formal Methods for Interactive Systems (FMIS 2006) |
PDF
BibTeX
Abstract |
| Must Program Verification Systems and Calculi be Verified? |
Bernhard Beckert, Vladimir Klebanov |
3rd International Verification Workshop (Verify 2006) |
PDF
BibTeX
Abstract |
2005
| Titel |
Autor |
Quelle |
|
| Refinement and Retrenchment for Programming Language Data Types |
Bernhard Beckert, Steffen Schlager |
Formal Aspects of Computing (Springer Journal) |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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. |
PDF
BibTeX
Abstract |
| Automated Reasoning with Analytic Tableaux and Related Methods |
Bernhard Beckert (ed.) |
Proceedings of the International Conference (TABLEAUX 2005) ,
Springer Verlag, LNCS 3702 |
BibTeX
Abstract |
 |
| Software Engineering and Formal Methods |
Bernhard Aichernig, Bernhard Beckert (eds.) |
Proceedings of the 3rd IEEE International Conference (SEFM 2005),
IEEE CS Digital Library |
BibTeX
Abstract
|
 |
| 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) |
PDF
BibTeX
Abstract
Online First issue |
| 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. |
PDF
BibTeX |
| Email Client Verification Goals |
Bernhard Beckert, Gerd Beuster |
Verisoft Project, Internal Technical Report #46, 2005 |
BibTeX |
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) |
PDF (Preliminary Version)
BibTeX
Abstract |
| Proof Reuse for Deductive Program Verification |
Bernhard Beckert and Vladimir Klebanov |
Software Engineering and Formal Methods (SEFM 2004) |
PDF (Preliminary Version)
BibTeX
Abstract |
| Software Verification with Integrated Data Type Refinement for Integer Arithmetic |
Bernhard Beckert and Steffen Schlager |
International Confrence on Integrated Formal Methods (IFM 2004) |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
Abstract
PDF
BibTeX |
| 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 |
Abstract
PDF
BibTeX |
| Email Client Specification |
Bernhard Beckert, Gerd Beuster, and Pia Breuer |
Verisoft Project, Internal Technical Report #6, 2004 |
BibTeX |
2003
| Titel |
Autor |
Quelle |
|
| Program Verification Using Change Information |
Bernhard Beckert and Peter H. Schmitt |
Software Engineering and Formal Methods (SEFM 2003) |
PDF
BibTeX
Abstract |
| Depth-first Proof Search without Backtracking for Free-variable Clausal Tableaux |
Bernhard Beckert |
Journal of Symbolic Computation |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
Abstract
PDF
BibTeX |
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 |
PDF
Appendix (PDF)
BibTeX
Abstract
|
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
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 |
PDF
BibTeX
Abstract |
| Free-variable Tableaux for Propositional Modal Logics |
Bernhard Beckert & Rajeev Goré |
Studia Logica |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX |
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 |
PDF
BibTeX
Abstract |
| Depth-first Proof Search without Backtracking for Free-variable Clausal Tableaux |
Bernhard Beckert |
International Workshop on First-Order Theorem Proving (FTP 2000)
|
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| Chapter on The SAT Problem of Signed CNF Formulas |
Bernhard Beckert, Reiner Hähnle, & Felip Manya |
Springer Verlag, Applied Logic Series 17 |
PDF (preliminary version)
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| A Dynamic Logic for Java Card |
Bernhard Beckert |
2nd ECOOP Workshop on Formal Techniques for Java Programs, Cannes, France |
PDF
BibTeX
Abstract |
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 |
Abstract
PDF
PDF, plain text, and graphical version
BibTeX |
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 |
|
PDF
BibTeX
PDF, plain text, and graphical (official German version) |
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 |
|
PDF
BibTeX
PDF, plain text, and graphical (official German version) |
|
| Chapter on Equality and Other Theories |
Bernhard Beckert |
Handbook of Tableau Methods
Springer Verlag |
PDF (draft version)
BibTeX
Abstract |
| Transformations between Signed and Classical Clause Logic |
Bernhard Beckert, Reiner Hähnle, Felip Manya |
International Symposium on Multiple-valued Logic (ISMVL 1999) |
PDF
BibTeX
Abstract |
| Proof Transformations from Search-oriented into Interaction-oriented Tableau Calculi |
Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckert |
Journal of Universal Computer Science |
PDF
BibTeX
Abstract |
| 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 |
BibTeX |
| 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 |
BibTeX
This is a preliminary version of my FTP 2000 paper (PDF) and the paper that apeared in the Journal of Symbolic Computation 2003 (PDF) |
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 |
PDF
BibTeX
More information on the tutorial |
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 |
PDF
BibTeX
Abstract |
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 |
PDF (draft version)
BibTeX
Abstract |
| 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 |
PDF (draft version)
BibTeX
Abstract |
|
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 |
PDF (preliminary version)
BibTeX
Abstract |
| System Description: leanK 2.0 |
Bernhard Beckert & Rajeev Goré |
International Conference on Automated Deduction (CADE), Lindau, Germany
Springer Verlag, LNCS 1421 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| 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 |
PDF
BibTeX
Abstract |
| Transformations between Signed and Classical Clause Logic |
Bernhard Beckert, Reiner Hähnle, & Felip Manya |
First International Workshop on Labelled Deduction, Freiburg, Germany |
PDF
BibTeX |
| 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 |
BibTeX |
| 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 |
PDF
BibTeX |
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 |
PDF
BibTeX
Abstract
An extended version of this paper including proofs is available as technical report.
PDF
BibTeX
|
| Semantic Tableaux with Equality |
Bernhard Beckert |
Journal of Logic and Computation, Vol. 7, No. 1, pages 38-58 |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
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 |
BibTeX |
| 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. |
PDF
BibTeX |
| 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. |
PDF
BibTeX |
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 |
PDF (draft version)
BibTeX |
| 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 |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
| Proving Compiler Correctness with Evolving Algebra Specifications |
Bernhard Beckert & Reiner Hähnle |
University of Karlsruhe, Department of Computer Science, TR 4/96 |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
1995
| Titel |
Autor |
Quelle |
|
| leanTAP: Lean Tableau-based Deduction |
Bernhard Beckert & Joachim Posegga |
Journal of Automated Reasoning, Vol. 15, No. 3, pages 339-358 |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
| leanEA: A lean Evolving Algebra Compiler |
Bernhard Beckert & Joachim Posegga |
Annual Conference of the European Association for Computer Science Logic (CSL 1995), Paderborn, Germany |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
| leanEA: A Lean Evolving Algebra Compiler |
Bernhard Beckert & Joachim Posegga |
11th Logic Programming Workshop, Wien, Austria |
PDF
BibTeX |
| 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. |
PDF
BibTeX |
| 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. |
PDF
BibTeX |
| 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.
|
PDF
BibTeX |
| 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 |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
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 |
PDF
BibTeX |
| leanTAP: Lean Tableau-Based Theorem Proving |
Bernhard Beckert & Joachim Posegga |
12th International Conference on Automated Deduction (CADE), Nancy, France |
PDF
BibTeX |
| Adding Equality to Semantic Tableaux |
Bernhard Beckert |
3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1994), Abingdon, UK |
PDF
BibTeX |
| On Anti-Links |
Bernhard Beckert, Reiner Hähnle, Neil Murray, & Anavai Ramesh |
5th International Conference on Logic Programming and Automated Reasoning (LPAR), Kiev, Ukraine |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
| Using E-Unification to Handle Equality in Universal Formula Semantic Tableaux |
Bernhard Beckert |
Theory Reasoning in Automated Deduction, Workshop at CADE-12, Nancy, France |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
| 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. |
PDF
BibTeX |
The lean -FAQ: Frequently Asked Quesiton about lean |
Bernhard Beckert & Joachim Posegga |
|
PDF |
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 |
PDF
BibTeX |
| 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 |
PDF
BibTeX |
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 |
PDF
BibTeX |
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. |
PDF
BibTeX |
