Reiner Hähnle

Orcid: 0000-0001-8000-7613

Affiliations:
  • Technical University of Darmstadt, Germany


According to our database1, Reiner Hähnle authored at least 190 papers between 1986 and 2024.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Schematic Program Proofs with Abstract Execution.
J. Autom. Reason., June, 2024

Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages.
ACM Trans. Program. Lang. Syst., March, 2024

SmartML: Towards a Modeling Language for Smart Contracts.
CoRR, 2024

Context-Aware Trace Contracts.
Proceedings of the Active Object Languages: Current Research Trends, 2024

2023
Variability modules.
J. Syst. Softw., 2023

Provably Fair Cooperative Scheduling.
CoRR, 2023

Context, Composition, Automation, and Communication - The C2AC Roadmap for Modeling and Simulation.
CoRR, 2023

Context-aware Trace Contracts.
CoRR, 2023

Herding CATs.
Proceedings of the Software Engineering and Formal Methods - 21st International Conference, 2023

Trace-based Deductive Verification.
Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

2022
Principles of Contract Languages (Dagstuhl Seminar 22451).
Dagstuhl Reports, November, 2022

A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems.
Leibniz Trans. Embed. Syst., 2022

Towards Trace-based Deductive Verification (Tech Report).
CoRR, 2022

LAGC Semantics of Concurrent Programming Languages.
CoRR, 2022

Automating Software Re-engineering: Introduction to the ISoLA 2022 Track.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, 2022

Towards a Usable and Sustainable Deductive Verification Tool.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, 2022

Automatic Loop Invariant Generation for Data Dependence Analysis.
Proceedings of the 10th IEEE/ACM International Conference on Formal Methods in Software Engineering, 2022

Finding Semantic Bugs Fast.
Proceedings of the Fundamental Approaches to Software Engineering, 2022

Dijkstra's Legacy on Program Verification.
Proceedings of the Edsger Wybe Dijkstra: His Life, Work, and Legacy, 2022

2021
Automated model analysis tools and techniques presented at FASE 2019.
Int. J. Softw. Tools Technol. Transf., 2021

Automated model extraction: From non-deterministic C code to active objects.
Sci. Comput. Program., 2021

An Architectural Pattern to Realize Multi Software Product Lines in Java.
Proceedings of the VaMoS'21: 15th International Working Conference on Variability Modelling of Software-Intensive Systems, 2021

Variability modules for Java-like languages.
Proceedings of the SPLC '21: 25th ACM International Systems and Software Product Line Conference, 2021

Delta-based verification of software product families.
Proceedings of the GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17, 2021

Certified Abstract Cost Analysis.
Proceedings of the Fundamental Approaches to Software Engineering, 2021

2020
Behavioral Contracts for Cooperative Scheduling.
Proceedings of the Deductive Software Verification: Future Perspectives, 2020

Safer Parallelization.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles, 2020

Who Carries the Burden of Modularity? - Introduction to ISoLA 2020 Track on Modularity and (De-)composition in Verification.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Automating Software Re-engineering - Introduction to the ISoLA 2020 Track.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles, 2020

Locally Static, Globally Dynamic Session Types for Active Objects.
Proceedings of the Recent Developments in the Design and Implementation of Programming Languages, 2020

2019
Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools.
Proceedings of the Computing and Software Science - State of the Art and Perspectives, 2019

The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more.
Int. J. Softw. Tools Technol. Transf., 2019

Verifying OpenJDK's Sort Method for Generic Collections.
J. Autom. Reason., 2019

Modeling and Verifying Cyber-Physical Systems with Hybrid Active Objects.
CoRR, 2019

The Trace Modality.
Proceedings of the Dynamic Logic. New Trends and Applications, 2019

Asynchronous Cooperative Contracts for Cooperative Scheduling.
Proceedings of the Software Engineering and Formal Methods - 17th International Conference, 2019

Automated Planning of ETCS Tracks.
Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2019

A Program Logic for Dependence Analysis.
Proceedings of the Integrated Formal Methods - 15th International Conference, 2019

Modeling Non-deterministic C Code with Active Objects.
Proceedings of the Fundamentals of Software Engineering - 8th International Conference, 2019

Abstract Execution.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2018
Formal modeling and analysis of railway operations with active objects.
Sci. Comput. Program., 2018

Analysis of SLA Compliance in the Cloud - An Automated, Model-based Approach.
Proceedings of the Second Workshop on Verification of Objects at RunTime EXecution, 2018

Prototyping Formal System Models with Active Objects.
Proceedings of the Proceedings 11th Interaction and Concurrency Experience, 2018

Interoperability of software product line variants.
Proceedings of the Proceeedings of the 22nd International Systems and Software Product Line Conference, 2018

Modular, Correct Compilation with Automatic Soundness Proofs.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Modeling, 2018

Constraint-Based Behavioral Consistency of Evolving Software Systems.
Proceedings of the Machine Learning for Dynamic Software Analysis: Potentials and Limits, 2018

Same Same But Different: Interoperability of Software Product Line Variants.
Proceedings of the Principled Software Development, 2018

2017
A Survey of Active Object Languages.
ACM Comput. Surv., 2017

Automatic detection and demonstrator generation for information flow leaks in object-oriented programs.
Comput. Secur., 2017

Abstraction Refinement for the Analysis of Software Product Lines.
Proceedings of the Tests and Proofs - 11th International Conference, 2017

Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2017

Deductive Verification of Railway Operations.
Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2017

Inferring Secrets by Guided Experiments.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2017, 2017

A Unified and Formal Programming Model for Deltas and Traits.
Proceedings of the Fundamental Approaches to Software Engineering, 2017

24 Challenges in Deductive Software Verification.
Proceedings of the ARCADE 2017, 2017

2016
Abstract Interpretation.
Proceedings of the Deductive Software Verification - The KeY Book, 2016

Quo Vadis Formal Verification?
Proceedings of the Deductive Software Verification - The KeY Book, 2016

KeY-Hoare.
Proceedings of the Deductive Software Verification - The KeY Book, 2016

Formal Verification with KeY: A Tutorial.
Proceedings of the Deductive Software Verification - The KeY Book, 2016

Debugging and Visualization.
Proceedings of the Deductive Software Verification - The KeY Book, 2016

A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY.
Softw. Syst. Model., 2016

Proof Repositories for Compositional Verification of Evolving Software Systems - Managing Change When Proving Software Correct.
LNCS Trans. Found. Mastering Chang., 2016

Machine Learning for Dynamic Software Analysis: Potentials and Limits (Dagstuhl Seminar 16172).
Dagstuhl Reports, 2016

A UML profile for delta-oriented programming to support software product line engineering.
Proceedings of the 20th International Systems and Software Product Line Conference, 2016

The interactive verification debugger: effective understanding of interactive proof attempts.
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

An empirical evaluation of two user interfaces of an interactive program verifier.
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

Towards Incremental Validation of Railway Systems.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Correctness-by-Construction and Post-hoc Verification: Friends or Foes?
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

Can Formal Methods Improve the Efficiency of Code Reviews?
Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

A General Lattice Model for Merging Symbolic Execution Branches.
Proceedings of the Formal Methods and Software Engineering, 2016

Uniform Modeling of Railway Operations.
Proceedings of the Formal Techniques for Safety-Critical Systems, 2016

Array Abstraction with Symbolic Pivots.
Proceedings of the Theory and Practice of Formal Methods, 2016

2015
Testing abstract behavioral specifications.
Int. J. Softw. Tools Technol. Transf., 2015

Designing Resource-Aware Cloud Applications.
Computer, 2015

A Dynamic Logic with Traces and Coinduction.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Exploit Generation for Information Flow Leaks in Object-Oriented Programs.
Proceedings of the ICT Systems Security and Privacy Protection, 2015

History-Based Specification and Verification of Scalable Concurrent and Distributed Systems.
Proceedings of the Formal Methods and Software Engineering, 2015

OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS.
Proceedings of the Automated Deduction - CADE-25, 2015

2014
Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS.
Serv. Oriented Comput. Appl., 2014

Reasoning and Verification: State of the Art and Current Trends.
IEEE Intell. Syst., 2014

The KeY Platform for Verification and Analysis of Java Programs.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

Visualizing Unbounded Symbolic Execution.
Proceedings of the Tests and Proofs - 8th International Conference, 2014

Analysis of Executable Software Models.
Proceedings of the Formal Methods for Executable Software Models, 2014

Symbolic Execution Debugger (SED).
Proceedings of the Runtime Verification - 5th International Conference, 2014

Introduction to Track on Engineering Virtualized Services.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014

Fully Abstract Operation Contracts.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014

An Interactive Verification Tool Meets an IDE.
Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Resource Analysis of Complex Programs with Cost Equations.
Proceedings of the Programming Languages and Systems - 12th Asian Symposium, 2014

2013
Deduction and Arithmetic (Dagstuhl Seminar 13411).
Dagstuhl Reports, 2013

Program Transformation Based on Symbolic Execution and Deduction.
Proceedings of the Software Engineering and Formal Methods - 11th International Conference, 2013

Engineering virtualized services.
Proceedings of the Second Nordic Symposium on Cloud Computing & Internet Technologies, 2013

Reuse in Software Verification by Abstract Method Calls.
Proceedings of the Automated Deduction - CADE-24, 2013

2012
A Liskov Principle for Delta-Oriented Programming.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, 2012

Adaptable and Evolving Software for Eternal Systems - (Track Summary).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, 2012

The Abstract Behavioral Specification Language: A Tutorial Introduction.
Proceedings of the Formal Methods for Components and Objects, 2012

Verified Resource Guarantees for Heap Manipulating Programs.
Proceedings of the Fundamental Approaches to Software Engineering, 2012

Formal Modeling of Resource Management for Cloud Architectures: An Industrial Case Study.
Proceedings of the Service-Oriented and Cloud Computing - First European Conference, 2012

2011
Preface: Special Issue of Selected Extended Papers of IJCAR 2010.
J. Autom. Reason., 2011

Formal Methods in Software Product Line Engineering.
Computer, 2011

Modeling Spatial and Temporal Variability with the HATS Abstract Behavioral Modeling Language.
Proceedings of the Formal Methods for Eternal Networked Software Systems, 2011

A Formalisation of Java Strings for Program Specification and Verification.
Proceedings of the Software Engineering and Formal Methods - 9th International Conference, 2011

Verified resource guarantees using COSTA and KeY.
Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2011

HATS Abstract Behavioral Specification: The Architectural View.
Proceedings of the Formal Methods for Components and Objects, 10th International Symposium, 2011

2010
Tests and Proofs - Preface of the Special Issue.
J. Autom. Reason., 2010

HATS - A Formal Software Product Line Engineering Methodology.
Proceedings of the Software Product Lines - 14th International Conference, 2010

A visual interactive debugger based on symbolic execution.
Proceedings of the ASE 2010, 2010

Task Forces in the EternalS Coordination Action.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

HATS: Highly Adaptable and Trustworthy Software Using Formal Methods.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Specifying Imperative ML-Like Programs Using Dynamic Logic.
Proceedings of the Formal Verification of Object-Oriented Software, 2010

ABS: A Core Language for Abstract Behavioral Specification.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

Program Specialization via a Software Verification Tool.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

2009
Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification.
Proceedings of the Teaching Formal Methods, Second International Conference, 2009

Interleaving Symbolic Execution and Partial Evaluation.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions.
Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

09411 Abstracts Collection - Interaction versus Automation: The two Faces of Deduction.
Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

2008
Integration of a security type system into a program logic.
Theor. Comput. Sci., 2008

Abstract Interpretation of Symbolic Execution with Explicit State Updates.
Proceedings of the Formal Methods for Components and Objects, 7th International Symposium, 2008

Specification Predicates with Explicit Dependency Information.
Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008

2007
A New Look at Formal Methods for Software Construction.
Proceedings of the Verification of Object-Oriented Software. The KeY Approach, 2007

Pattern-Driven Formal Specification.
Proceedings of the Verification of Object-Oriented Software. The KeY Approach, 2007

Generating Unit Tests from Formal Proofs.
Proceedings of the Tests and Proofs - 1st International Conference, 2007

KeY: A Formal Method for Object-Oriented Systems.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2007

KeY-C: A Tool for Verification of C Programs.
Proceedings of the Automated Deduction, 2007

Symbolic Fault Injection.
Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

The KeY system 1.0 (Deduction Component).
Proceedings of the Automated Deduction, 2007

2006
Preface.
Soft Comput., 2006

Intelligent Systems and Formal Methods in Software Engineering.
IEEE Intell. Syst., 2006

Integrating Object-Oriented Design and Deductive Verification of Software.
Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 2006

Automating Verification of Loops by Parallelization.
Proceedings of the Logic for Programming, 2006

Verifying Object-Oriented Programs with KeY: A Tutorial.
Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

Verification by Parallelization of Parametric Code.
Proceedings of the Algebraic and Proof-theoretic Aspects of Non-classical Logics, 2006

2005
Integration of informal and formal development of object-oriented safety-critical software.
Int. J. Softw. Tools Technol. Transf., 2005

The KeY tool.
Softw. Syst. Model., 2005

Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages.
Log. J. IGPL, 2005

A Theorem Proving Approach to Analysis of Secure Information Flow.
Proceedings of the Security in Pervasive Computing, Second International Conference, 2005

Normal Forms for Knowledge Compilation.
Proceedings of the Foundations of Intelligent Systems, 15th International Symposium, 2005

2004
Linearity and regularity with negation normal form.
Theor. Comput. Sci., 2004

OCL and Model Driven Engineering.
Proceedings of the UML Modeling Languages and Applications, 2004

Verification of Safety Properties in the Presence of Transactions.
Proceedings of the Construction and Analysis of Safe, 2004

2003
Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software: A Case Study with the KeY System.
Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems, 2003

Fair Constraint Merging Tableaux in Lazy Functional Programming Style.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2003

Using a Software Testing Technique to Improve Theorem Proving.
Proceedings of the Formal Approaches to Software Testing, 2003

2002
An Authoring Tool for Informal and Formal Requirements Specifications.
Proceedings of the Fundamental Approaches to Software Engineering, 2002

The KeY System: Integrating Object-Oriented Design and Formal Methods.
Proceedings of the Fundamental Approaches to Software Engineering, 2002

2001
Complexity of Many-Valued Logics.
Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic, 2001

A Modular Reduction of Regular Logic to Classical Logic.
Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic, 2001

Ordered Resolution vs. Connection Graph Resolution.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Tableaux and Related Methods.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000
Entwurfgesteuerte Erzeugung von OCL-Constraints.
Softwaretechnik-Trends, 2000

The KeY Approach: Integrating Object Oriented Design and Formal Verification.
Proceedings of the Logics in Artificial Intelligence, European Workshop, 2000

The 2-SAT Problem of Regular Signed CNF Formulas.
Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic, 2000

Entwurfsmustergesteuerte Erzeugung von OCL-Constraints.
Proceedings of the Informatik 2000, 2000

Moder Generation Theorem Proving with Finite Interval Constraints.
Proceedings of the Computational Logic, 2000

1999
J.UCS Special Issue on Integration of Deduction Systems.
J. Univers. Comput. Sci., 1999

Proof Confluent Tableau Calculi.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1999

Transformations between Signed and Classical Clause Logic.
Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic, 1999

1998
Commodious Axiomatization of Quantifiers in Multiple-Valued Logic.
Stud Logica, 1998

Simplification of Many-Valued Logic Formulas Using Anti-Links.
J. Log. Comput., 1998

Integrierter Deduktiver Software-Entwurf.
Künstliche Intell., 1998

Some Remarks on Completeness, Connection Graph Resolution and Link Deletion.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998

1997
Proof theory of many-valued logic--linear optimization--logic design: connections and interactions.
Soft Comput., 1997

Fast Subsumption Checks Using Anti-Links.
J. Autom. Reason., 1997

Ordered Tableaux: Extensions and Applications.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1997

Restart Tableaux with Selection Function.
Proceedings of the Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, 1997

Completeness for Linear Regular Negation Normal Form Inference Systems.
Proceedings of the Foundations of Intelligent Systems, 10th International Symposium, 1997

1996
A-Ordered Tableaux.
J. Log. Comput., 1996

Exploiting Data Dependencies in Many-Valued Logics.
J. Appl. Non Class. Logics, 1996

The Tableau-based Theorem Prover <sub>3</sub>T<sup>A</sup>P Version 4.0.
Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995
Deduction by Combining Semantic Tableaux and Integer Programming.
Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994
Short Conjunctive Normal Forms in Finitely Valued Logics.
J. Log. Comput., 1994

The Liberalized delta-Rule in Free Variable Semantic Tableaux.
J. Autom. Reason., 1994

Many-Valued Logic and Mixed Integer Programming.
Ann. Math. Artif. Intell., 1994

On Anti-Links.
Proceedings of the Logic Programming and Automated Reasoning, 5th International Conference, 1994

Efficient Deduction in Many-Valued Logics.
Proceedings of the 24th IEEE International Symposium on Multiple-Valued Logic, 1994

Improving Temporal Logic Tableaux Using Integer Constraints.
Proceedings of the Temporal Logic, First International Conference, 1994

Semantic Tableaux with Ordering Restrictions.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

Automated deduction in multiple-valued logics.
International series of monographs on computer science 10, Oxford University Press, ISBN: 978-0-19-853989-6, 1994

1993
Verification of Switch-Level Designs with Many-Valued Logic.
Proceedings of the Logic Programming and Automated Reasoning,4th International Conference, 1993

The Even More Liberalized delta-Rule in Free Variable Semantic Tableaux.
Proceedings of the Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, 1993

Short CNF in Finitely-Valued Logics.
Proceedings of the Methodologies for Intelligent Systems, 7th International Symposium, 1993

1992
The Many-Valued Theorem Prover <sub>3</sub>T<sup>A</sup>P.
IWBS Report, 1992

Analytic Tableau and Integer Programming (Extended Abstract).
Proceedings of the Workshop Theorem Proving with Analytic Tableaux and Related Methods, 1992

An Improved Method for Adding Equality to Free Variable Semantic Tableaux.
Proceedings of the Automated Deduction, 1992

The Tableau-Based Theorem Prover <sub>3</sub>T<sup>A</sup>P for Multi-Valued Logics.
Proceedings of the Automated Deduction, 1992

A New Translation from Deduction into Integer Programming.
Proceedings of the Artificial Intelligence and Symbolic Mathematical Computation, 1992

1991
Uniform Notation of Tableau Rules for Multiple-Valued Logics.
Proceedings of the 21st International Symposium on Multiple-Valued Logic, 1991

1990
Spezifikation eines Theorembeweisers für dreiwertige First-Order Logik.
IWBS Report, 1990

Towards an Efficient Tableau Proof Procedure for Multiple-Valued Logics.
Proceedings of the Computer Science Logic, 4th Workshop, 1990

1986
An Interactive Verification System Based on Dynamic Logic.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986


  Loading...