Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Selected PublicationsBack to Reiner's Home Page
Selected Publications
My personal bibliography containing BiBTeX entries for the following
(and many more) papers is here (800kB, over
2000 entries). This bibliography is also part of the The
Collection of Computer Science Bibliographies.
To appear
VERIFY'07 Workshop
Symbolic Fault Injection Daniel Larsson and Reiner Hähnle
VERIFY'07, colocated with Conference on Automated
Deduction (CADE), Bremen, Germany
Preliminary version (PDF)
FMCO 2006
Verifying Object-Oriented Programs with KeY: A Tutorial Wolfgang Ahrendt and Bernhard Beckert and Reiner Hähnle
and Philipp Rümmer and Peter H. Schmitt
Post Conf. Proceedings 5th Intl. Symposium on
Formal Methods for Components and Objects, Springer-Verlag LNCS
Preliminary version (PDF,
303K)
C/C++ Verification Workshop
Deductive Verifiction of C Programs with KeY-C Oleg Mürk and Daniel Larsson and Reiner Hähnle
C/C++ Verification Workshop, colocated with Integrated
Formal Methods (IFM), Oxford, UK
Preliminary version (PDF,
172K)
Algebraic and Proof-theoretic Aspects of Non-classical
Logics Essays in honour of Professor Daniele Mundici on occasion of his 60th birthday
Verification by Parallelization of Parametric Code Tobias Gedell and Reiner Hähnle
Algebraic and Proof-theoretic Aspects of Non-classical
Logics Essays in honour of Professor Daniele Mundici on occasion of his 60th birthday, Springer-Verlag LNCS
Preprint (PDF,
201K)
2007
Trustworthy Global Computing (TGC) 2006
Integration of a Security Type System into a Program
Logic Reiner Hähnle, Jing Pan, Philipp Rümmer and Dennis Walter
Proc. 2nd Symposium on Trustworthy Global Computing,
Lucca, Italy, Springer-Verlag LNCS 4661, pp 116-131
Preliminary Version (PDF,
239K)
Tests and Proofs (TAP) 2007
Generating Unit Tests from Formal Proofs Christian Engel and Reiner Hähnle
Proc. Tests and Proofs (TAP),
Zürich, Switzerland, Springer-Verlag LNCS 4454
Preliminary version (PDF,
157K)
CADE 2007
KeY-C: A Tool for Verification of C Programs Oleg Mürk and Daniel Larsson and Reiner Hähnle
Proc. 21st Conference on Automated
Deduction (CADE), Bremen, Germany, Springer-Verlag
LNCS 4603, pp 385-390
Preliminary version (PDF,
149K)
CADE 2007
The KeY System 1.0 (Deduction Component) Bernhard Beckert and Martin Giese and Reiner Hähnle
and Vladimir Klebanov and Philipp Rümmer and
Steffen Schlager and Peter H. Schmitt
Proc. 21st Conference on Automated
Deduction (CADE), Bremen, Germany, Springer-Verlag
LNCS 4603
Preliminary version (PDF,
114K)
FMOODS 2007
KeY: A Formal Method for Object-Oriented Systems Wolfgang Ahrendt and Bernhard Beckert and Reiner
Hähnle and Peter H. Schmitt Proc. 9th IFIP
Intl. Conf. on Formal Methods for Open Object-based
Distributed Systems (FMOODS), Cyprus, Springer-Verlag
LNCS 4468, pp 32--43 (PDF,
171K)
Edited by: Bernhard Beckert, Reiner Hähnle and Peter
H. Schmitt
With a Foreword by K. Rustan M. Leino
15 Chapters with 2 Appendices, XXIX + 658p,
Springer-Verlag, LNCS 4334
Table of Contents (PDF,
94K)
Chapter 6: Pattern-Driven Formal Specification Richard Bubel and Reiner Hähnle
Edited by: Bernhard Beckert, Reiner Hähnle and Peter
H. Schmitt, Springer-Verlag, LNCS 4334, pp 295-315
Preliminary version (PDF,
394K)
IEEE Intelligent Systems
Intelligent Systems and Formal Methods in
Software Engineering Bernhard Beckert, Reiner Hähnle, Tony Hoare, Douglas
R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli,
Thomas Ball, and Sriram K. Rajamani
IEEE Intelligent Systems 21(6):71-81, Nov/Dec 2006, Article
home page
LPAR 2006
Automating Verification of Loops by Parallelization Tobias Gedell and Reiner Hähnle
Proc. 13th International Conference on
Logic for Programming, Artificial Intelligence and
Reasoning, Phnom Penh,
Cambodia, Springer-Verlag LNCS 4246, pp 332-346
Preprint (PDF,
189K), Final
version
2005
Software Tools for Technology Transfer
Integration of informal and formal development of object-oriented safety-critical software Richard Bubel and Reiner Hähnle
Springer-Verlag, 7(3), 197-211, June 2005
Preprint (PDF), Final
version
Logic Journal of the IPGL
Many-Valued Logic, Partiality, and Abstraction in Formal
Specification Languages Reiner Hähnle Logic Journal of the IGPL, Oxford University Press, 13(4),
415-433, July 2005 Preprint (PDF),
Final version (PDF)
ISMIS 2005
Normal Forms for Knowledge Compilation Reiner Hähnle, Neil Murray, Erik Rosenthal
Proceedings ISMIS'05, Saratoga Springs/NY, USA
Springer-Verlag, LNCS 3488 pp 304--313, 2005, Preprint (PDF) , Online First
2nd International Conference on Security in Pervasive Computing
A Theorem Proving Approach to Analysis of Secure Information Flow Ádám Darvas, Reiner Hähnle, Dave Sands
Boppard, Germany, April 2005
Springer-Verlag, LNCS 3362 pp 151-171, 2005, preprint
Preprint (PDF), Springer
Online
Software and System Modeling
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
Springer-Verlag, 4(1):32-54, 2005 Springer Online
CASSIS'04
Verification of Safety Properties in the Presence of Transactions Reiner Hähnle and Wojciech Mostowski
Post Conference Proceedings, CASSIS: Construction and
Analysis of Safe, Secure and Interoperable Smart devices,
Marseille
Springer-Verlag, LNCS 3362 pp 151-171, 2005, preprint
(PDF), Springer
Online
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, (PDF)
Volume 98(1), pp 17-54
UML 2004 workshop on OCL and Model Driven Engineering
Rule-Based Simplification of OCL Constraints Martin Giese, Reiner Hähnle, and Daniel Larsson
Workshop Proceedings
(PDF)
2003
FATES 2003
Using a software testing technique to improve theorem
proving Reiner Hähnle and Angela Wallenburg
Post Conference Proceedings,
3rd International Workshop on Formal Approaches
to Testing of Software (FATES), Montréal, Canada
(PDF)
Tableaux 2003
Tableaux and Constraints Martin Giese and Reiner Hähnle
Position papers, Tableaux 2003, Rome, Italy
(gzipped
PS)
Fair Constraint Merging Tableaux in Lazy Functional Programming Style Reiner Hähnle and Niklas Sörensson System
Description, Automated Reasoning with Analytic
Tableaux and Related Methods: International
Conference, Tableaux 2003, Rome, Italy,
Springer-Verlag, LNAI 2796. (PDF),
Extended
Version (PDF),
(Springer LINK)
Workshop on Formal Methods for Industrial Critical Systems (FMICS 03)
Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software: A Case Study with the KeY System Richard Bubel and Reiner Hähnle
Invited Paper, FMICS 2003, Røros, Norway
(PDF), ENTCS Vol 80
Workshop on Issues in the Theory of Security (WITS'03)
A Theorem Proving Approach to Analysis of Secure Information Flow Ádám Darvas, Reiner Hähnle, Dave Sands
Affiliated to ETAPS 2003, Warsaw, Poland
(PDF)
2002
Journal of the Information Processing Society of Japan
Model Generation Theorem Proving with Finite
Interval Constraints Reiner Hähnle and Ryuzo Hasegawa and Yasuyuki Shirai
Volume 43, number 12.
Chapter on Complexity of Many-Valued Logics Reiner Hähnle
Edited by: Melvin Fitting and Ewa Orlowska
Volume 114 of Studies in Fuzziness and Soft Computing,
Physica Verlag.
Tableaux 2002
Unit Preference for Ordered Resolution
and for Connection Graph Resolution Reiner Hähnle, Neil Murray, Erik Rosenthal
Position papers, Tableaux 2002, Copenhagen, Denmark
(PDF)
Workshop on Problems and Problem Sets (affiliated to
CADE-18), Copenhagen, Denmark
Verification of Hardware Systems with First-Order Logic Koen Claessen, Reiner Hähnle, Johan Mårtensson (pdf, 134K)
FASE 2002
An Authoring Tool for Informal and Formal Requirements Specifications Reiner Hähnle and Kristofer Johannisson and Aarne Ranta
Proceedings Fundamental Approaches to Software Engineering (FASE),
Part of Joint European Conferences on Theory and Practice
of Software, ETAPS, Grenoble.
2002. Springer-Verlag LNAI.
(pdf, 362K)
FASE 2002
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
Proceedings Fundamental Approaches to Software Engineering (FASE),
Part of Joint European Conferences on Theory and Practice
of Software, ETAPS, Grenoble.
2002. Springer-Verlag LNAI.
(pdf, 117K)
Edited by: J. Alan Robinson and Andrei Voronkov
May 2001, Elsevier Publishers.
Please see also Andrei Voronkov's HBAR
web page
(PDF, 640K)
IJCAR 2001
Ordered Resolution vs. Connection Graph Resolution Reiner Hähnle, Neil Murray, Erik Rosenthal
Proceedings International Joint Conference on
Automated Reasoning, Siena, Italy
2001. Springer-Verlag LNAI.
(gzipped Postscript, 83K)
Computational Intelligence in Theory and Practice
Chapter on Proof Theory of Many-Valued
Logic and Linear Optimization Reiner Hähnle
Edited by: Bernd Reusch and Karl-Heinz Temme
Advances in Soft Computing Series, Physica-Verlag, Heidelberg.
ISMVL 2001
A Modular Reduction of Regular Logic to Classical Logic Ramon Bejar, Reiner Hähnle and Felip Manya
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'2001, Warsaw, Poland, IEEE CS Press. (gzipped Postscript, 47K)
ISMVL 2001
Complexity of Many-Valued Logics (Invited Tutorial) Reiner Hähnle
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'2001, Warsaw, Poland, IEEE CS Press. (gzipped Postscript, 83K)
ETAPS 2001 Workshop on Transformations in UML (WTUML),
Genova, Italy
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 (gzipped
Postscript, 144K)
Java Card Workshop, Cannes
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 (gzipped
Postscript, 40K)
Softwaretechnik 2000, Berlin
Entwurfsmustergesteuerte Erzeugung von OCL-Constraints Thomas Baar and Reiner Hähnle and Theo Sattler
and Peter H. Schmitt (gzipped
Postscript, 95K)
First International Conference on Computational Logic,
CL 2000, Stream on Logic Programming:
Theory and Extensions, London, UK
Model Generation Theorem Proving with Finite
Interval Constraints Reiner Hähnle and Ryuzo Hasegawa and Yasuyuki Shirai (gzipped
Postscript, 85K)
Chapter on The SAT Problem of Signed CNF Formulas Bernhard Beckert, Reiner Hähnle and Felip Manyà
Edited by: Marcello D'Agostino, David Basin, Dov Gabbay, Séan Matthews, Luca Viganó
Volume 17 of Applied Logic Series, Kluwer.
ISMVL 2000
On the Regular 2-SAT Problem Bernhard Beckert, Reiner Hähnle and Felip Manya
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'2000, Portland/OR, USA, IEEE CS Press.
(gzipped Postscript, 45K)
Transformations between Signed and Classical Clause Logic Bernhard Beckert, Reiner Hähnle and Felip Manya
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'99, Freiburg, Germany
(gzipped Postscript, 61K)
1998
KI - Künstliche Intelligenz
Integrierter Deduktiver Software-Entwurf Reiner Hähnle, Wolfram Menzel, Peter Schmitt
Issue 4/98 (December), pp. 40-41, 1998.
Journal of Logic and Computation
Simplification of Many-Valued Logic Formulas Using
Anti-Links Bernhard Beckert, Reiner Hähnle, Gonzalo Escalada-Imaz
Volume 8(4), pp. 569-588, 1998.
(gzipped Postscript, 79K)
Studia Logica. Special Issue on Many-Valued Logics,
their Proof Theory and Algebras, edited by D. Mundici.
Commodious Axiomatization of Quantifiers in Multiple-Valued Logic Reiner Hähnle
Volume 61(1), pp. 101-121, 1998.
(Postscript, 77K)
Edited by: Wolfgang Bibel and Peter Schmitt
Volume I-III, Kluwer Publishing Company 1998.
Chapter I.1: Analytic Tableaux Bernhard Beckert and Reiner Hähnle
Chapter II.4: Integrating Automated and Interactive Theorem Proving Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel,
Wolfgang Reif, Gerhard Schellhorn, Peter Schmitt
Tableaux 1998
Some Remarks on Completeness, Connection
Graph Resolution and Link Deletion Reiner Hähnle, Neil Murray, Erik Rosenthal
Proceedings Tableaux 1998, Tilburg, Netherlands
(Postscript, 56K)
1997
Mathware and Soft Computing
Deduction in Many-Valued Logics: a Survey Reiner Hähnle and Gonzalo Escalada-Imaz
Vol. IV, Number 2, pp. 69-97
(Postscript, 91K)
Soft Computing: A Fusion of Foundations, Methodologies and Applications
Proof Theory of Many-Valued
Logic - Linear Optimization - Logic Design:
Connections and Interactions Reiner Hähnle
Vol. 1, Number 3, pp. 107-119
Kurt-Gödel-Colloquium 1997
Restart Tableaux with Selection Function Christian Pape and Reiner Hähnle Proceedings
Computational Logic and Proof Theory: 5th Kurt Gödel
Colloquium, KGC'97, Vienna, Austria, Springer-Verlag,
LNCS 1289 (Postscript,
82K) , (Springer
LINK)
ISMIS 1997
Completeness for Linear Regular Negation
Normal Form Inference Systems Reiner Hähnle, Neil Murray, Erik Rosenthal
Proceedings Foundations of Intelligent Systems: 10th
International Symposium ISMIS'97, Charlotte/NC, USA,
Springer-Verlag, LNCS 1325, (Postscript,
61K) , (Springer
LINK)
Journal of Automated Reasoning
Fast Subsumption Checks Using Anti-Links Anavai Ramesh and Neil V. Murray and Bernhard Beckert and Reiner Hähnle
Vol. 18, Number 1, pp. 47-84
(Postscript, 109K)
Tableaux 1997
Ordered Tableaux: Extensions and Applications Reiner Hähnle and Christian Pape Proceedings
Automated Reasoning with Analytic Tableaux and
Related Methods: International Conference,
TABLEAUX'97, Pont-a-Mousson, France, Springer-Verlag,
LNCS 1227 (Postscript,
66K), (Springer
LINK)
1996
Journal of Logic and Computation
A-Ordered Tableaux Reiner Hähnle and Stefan Klingenbeck Vol. 6, Number 6, pp. 819-834
(Postscript, 123K)
CADE-13 1996
The Many-Valued Tableau-Based Theorem Prover 3TAP:
Version 4.0 (System Abstract) Bernhard Beckert, Reiner Hähnle, Peter Oel and Martin
Sulzmann Proc. 13th Conference on Automated
Deduction CADE, New Brunswick/NJ, USA,
Springer-Verlag, LNCS 1104 (Postscript,
30K), (Springer
LINK)
ISMVL 1996
Commodious Axiomatization of Quantifiers in Multiple-Valued Logic Reiner Hähnle
Proc. International Symposium on Multiple-Valued Logics,
ISMVL'96, Santiago de Compostela, Spain
(Postscript, 63K)
Journal of Applied Non-Classical Logics
Exploiting Data Dependencies in Many-Valued Logics Reiner Hähnle Vol. 6, Number 1, pp. 49-69
(Postscript, 68K)
1995
Post ILPS Workshop on Interval Constraints 1995, Portland/OR, USA
Model Generation Theorem Proving with Interval Constraints Reiner Hähnle and Ryuzo Hasegawa and Yasuyuki Shirai (Postscript, 89K)
Computer Science Logic 1995, Paderborn/Germany
Deduction by Combining Semantic Tableaux and Integer Programming Bernhard Beckert and Reiner Hähnle
Springer-Verlag, LNCS 1092 (Postscript,
54K), (Springer LINK)
Collegium Logicum. Annals of the Kurt-Goedel-Society
Automated Deduction and Integer Programming Reiner Hähnle
Vol. 1, pp. 67-86, Springer-Verlag
Proceedings of: Theorem Proving with Analytic Tableaux
and Related Methods, 4th International Workshop, St. Goar,
Germany
Peter Baumgartner, Reiner Hähnle and Joachim Posegga
LNAI 918, Springer-Verlag
1994
Journal of Automated Reasoning
The liberalized delta-rule in free variable semantic tableaux Reiner Hähnle and Peter H. Schmitt
Vol. 13, Number 2, pp. 211-222
(DVI, 30K)
Annals of Math and AI
Many-Valued Logic and Mixed Integer Programming Reiner Hähnle
Vol. 12, Numbers 3-4, pp. 231-264
(DVI, 53K)
Journal of Logic and Computation
Short Conjunctive Normal Forms in Finitely-Valued Logics Reiner Hähnle
Vol. 4, Number 6, pp. 905-927
(DVI, 76K)
ICTL 1994
Improving Temporal Logic Tableaux Using Integer Constraints Reiner Hähnle and Ortrun Ibens Proc.~First
International Conference on Temporal Logic, Bonn,
Germany, Springer-Verlag, LNCS 827, (postscript,
38K) , (Springer
LINK)
Reiner Hähnle
International Series of Monographs on Computer Science 10,
Oxford University
Press
Reviewed in Computing Reviews, August 1995,
pp. 409-410, #9508-0571; Notre Dame Journal Formal Logic, 37(4),
Fall 1996; Mathematical Reviews 1996, #96a:68107
The book is out of print now. You can download a copy for your
personal use from here
(with permission from Oxford University
Press).
CADE-12 1994
Semantic Tableaux with Ordering Restrictions Stefan Klingenbeck and Reiner Hähnle
Proc. 12th Conference on Automated Deduction CADE,
Nancy, France, Springer-Verlag LNCS 814 (postscript,
76K), (Springer
LINK)
LPAR 1994
On Anti-Links Bernhard Beckert, Reiner Hähnle, Neil Murray, Anavai
Ramesh Proc. 5th International Conference on
Logic Programming and Automated Reasoning, Kiev,
Ukraine, Springer-Verlag LNCS 822 (postscript,
54K), (Springer
LINK)
ISMVL 1994
Efficient Deduction in Many-Valued Logics Reiner Hähnle
Proc. International Symposium on Multiple-Valued Logics, ISMVL'94, Boston/MA, USA
(postscript, 103K)
1993
KGC 1993
The even more
liberalized delta-rule in free variable semantic tableaux Bernhard Beckert, Reiner Hähnle, Peter
H. Schmitt Proceedings of the third Kurt
Goedel Colloquium KGC'93, Brno, Czech Republic,
Springer-Verlag LNCS 713 (DVI,
25K), (Springer
LINK)
ISMIS 1993
Short CNF in Finitely-Valued Logics Reiner Hähnle Proceedings ISMIS'93,
Trondheim, Norway, Springer-Verlag LNCS 689 (DVI,
32K), (Springer
LINK)
LPAR 1993
Verification of Switch Level
Designs with Many-Valued Logic Reiner Hähnle and Werner Kernig
Proc.~{LPAR}'93, St.~Petersburg, Russia,
Springer-Verlag LNCS 698 (DVI,
30K), (Springer
LINK)
1992
CADE-11 1992
An Improved Method for Adding Equality to Free Variable Semantic Tableaux Bernhard Beckert and Reiner Hähnle Proc. 11th
Conference on Automated Deduction CADE, Albany/NY,
USA, Springer LNCS 607 (DVI,
45K), (Springer
LINK)
CADE-11 1992
The Many-Valued Tableau-Based Theorem Prover 3TAP (System Abstract) Bernhard Beckert, Stefan Gerberding, Reiner Hähnle,
Werner Kernig Proc. 11th Conference on
Automated Deduction CADE, Albany/NY, USA, Springer
LNCS 607 (DVI,
7K), (Springer
LINK)
AISMC-1
A New Translation from
Deduction into Integer Programming Reiner Hähnle Proc. Int. Conf. on Artificial
Intelligence and Symbolic Mathematical Computing
AISMC-1, Karlsruhe, Germany, Springer LNCS 737 (DVI,
34K), (Springer
LINK)
1991
ISMVL 1991
Uniform Notation of Tableaux
Rules for Multiple-Valued Logics Reiner Hähnle Proc. International Symposium
on Multiple-Valued Logic, Victoria, Canada, (DVI,
49K)
1990
CSL 1990
Towards an Efficient Tableau Proof Procedure for
Multiple-Valued Logics Reiner Hähnle Proc. Computer Science Logic,
Heidelberg, Germany, Springer LNCS 533 (DVI,
39K), (Springer
LINK)