Search Results

Documents authored by Hähnle, Reiner

Document
DOI: 10.4230/DagRep.12.11.1
Principles of Contract Languages (Dagstuhl Seminar 22451)

Authors: Dilian Gurov, Reiner Hähnle, Marieke Huisman, Giles Reger, and Christian Lidström

Published in: Dagstuhl Reports, Volume 12, Issue 11 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22451 "Principles of Contract Languages". At the seminar, participants discussed the fundamental aspects of software contracts. Topics included the format and expressiveness of contracts, their use cases in software development and analysis, and contract composition and decomposition.
Cite as

Dilian Gurov, Reiner Hähnle, Marieke Huisman, Giles Reger, and Christian Lidström. Principles of Contract Languages (Dagstuhl Seminar 22451). In Dagstuhl Reports, Volume 12, Issue 11, pp. 1-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{gurov_et_al:DagRep.12.11.1,
  author =	{Gurov, Dilian and H\"{a}hnle, Reiner and Huisman, Marieke and Reger, Giles and Lidstr\"{o}m, Christian},
  title =	{{Principles of Contract Languages (Dagstuhl Seminar 22451)}},
  pages =	{1--27},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{11},
  editor =	{Gurov, Dilian and H\"{a}hnle, Reiner and Huisman, Marieke and Reger, Giles and Lidstr\"{o}m, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.11.1},
  URN =		{urn:nbn:de:0030-drops-178334},
  doi =		{10.4230/DagRep.12.11.1},
  annote =	{Keywords: software contracts, program specifications, software development, program analysis}
}
Document
DOI: 10.4230/LITES.8.2.4
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors: Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Cite as

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:LITES.8.2.4,
  author =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  title =	{{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:34},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.4},
  doi =		{10.4230/LITES.8.2.4},
  annote =	{Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.1
Locally Static, Globally Dynamic Session Types for Active Objects

Authors: Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Active object languages offer an attractive trade-off between low-level, preemptive concurrency and fully distributed actors: syntactically identifiable atomic code segments and asynchronous calls are the basis of cooperative concurrency, still permitting interleaving, but nevertheless being mechanically analyzable. The challenge is to reconcile local static analysis of atomic segments with the global scheduling constraints it depends on. Here, we propose an approximate, hybrid approach; At compile-time we perform a local static analysis: later, any run not complying to a global specification is excluded via runtime checks. That specification is expressed in a type-theoretic language inspired by session types. The approach reverses the usual (first global, then local) order of analysis and, thereby, supports analysis of open distributed systems.
Cite as

Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan. Locally Static, Globally Dynamic Session Types for Active Objects. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hahnle_et_al:OASIcs.Gabbrielli.1,
  author =	{H\"{a}hnle, Reiner and Haubner, Anton W. and Kamburjan, Eduard},
  title =	{{Locally Static, Globally Dynamic Session Types for Active Objects}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{1:1--1:24},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.1},
  URN =		{urn:nbn:de:0030-drops-132237},
  doi =		{10.4230/OASIcs.Gabbrielli.1},
  annote =	{Keywords: Session Types, Active Objects, Runtime Verification, Static Verification}
}
Document
DOI: 10.4230/DagRep.6.4.161
Machine Learning for Dynamic Software Analysis: Potentials and Limits (Dagstuhl Seminar 16172)

Authors: Amel Bennaceur, Dimitra Giannakopoulou, Reiner Hähnle, and Karl Meinke

Published in: Dagstuhl Reports, Volume 6, Issue 4 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16172 "Machine Learning for Dynamic Software Analysis: Potentials and Limits". Machine learning is a powerful paradigm for software analysis that provides novel approaches to automating the generation of models and other essential artefacts. This Dagstuhl Seminar brought together top researchers active in the fields of machine learning and software analysis to have a better understanding of the synergies between these fields and suggest new directions and collaborations for future research.
Cite as

Amel Bennaceur, Dimitra Giannakopoulou, Reiner Hähnle, and Karl Meinke. Machine Learning for Dynamic Software Analysis: Potentials and Limits (Dagstuhl Seminar 16172). In Dagstuhl Reports, Volume 6, Issue 4, pp. 161-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{bennaceur_et_al:DagRep.6.4.161,
  author =	{Bennaceur, Amel and Giannakopoulou, Dimitra and H\"{a}hnle, Reiner and Meinke, Karl},
  title =	{{Machine Learning for Dynamic Software Analysis: Potentials and Limits (Dagstuhl Seminar 16172)}},
  pages =	{161--173},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{4},
  editor =	{Bennaceur, Amel and Giannakopoulou, Dimitra and H\"{a}hnle, Reiner and Meinke, Karl},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.4.161},
  URN =		{urn:nbn:de:0030-drops-66954},
  doi =		{10.4230/DagRep.6.4.161},
  annote =	{Keywords: Machine learning, Automata learning, Software analysis, Dynamic analysis, Testing, Model extraction, Systems integration}
}
Document
DOI: 10.4230/DagRep.3.10.1
Deduction and Arithmetic (Dagstuhl Seminar 13411)

Authors: Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach

Published in: Dagstuhl Reports, Volume 3, Issue 10 (2014)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13411 "Deduction and Arithmetic". The aim of this seminar was to bring together researchers working in deduction and fields related to arithmetic constraint solving. Current research in deduction can be categorized in three main strands: SMT solvers, automated first-order provers, and interactive provers. Although dealing with arithmetic has been in focus of all three for some years, there is still need of much better support of arithmetic. Reasong about arithmetic will stay at the center of attention in all three main approaches to automated deduction during the coming five to ten years. The seminar was an important event for the subcommunities involved that made it possible to communicate with each other so as to avoid duplicate effort and to exploit synergies. It succeeded also in identifying a number of important trends and open problems.
Cite as

Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach. Deduction and Arithmetic (Dagstuhl Seminar 13411). In Dagstuhl Reports, Volume 3, Issue 10, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.3.10.1,
  author =	{Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph},
  title =	{{Deduction and Arithmetic (Dagstuhl Seminar 13411)}},
  pages =	{1--24},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{10},
  editor =	{Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.10.1},
  URN =		{urn:nbn:de:0030-drops-44250},
  doi =		{10.4230/DagRep.3.10.1},
  annote =	{Keywords: Automated Deduction; Program Verification; Arithmetic Constraint Solving}
}
Document
DOI: 10.4230/DagSemProc.09411.1
09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction

Authors: Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
From 04.10. to 09.10.2009, the Dagstuhl Seminar 09411 ``Interaction versus Automation: The two Faces of Deduction'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow. 09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ball_et_al:DagSemProc.09411.1,
  author =	{Ball, Thomas and Giesl, J\"{u}rgen and H\"{a}hnle, Reiner and Nipkow, Tobias},
  title =	{{09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.1},
  URN =		{urn:nbn:de:0030-drops-25032},
  doi =		{10.4230/DagSemProc.09411.1},
  annote =	{Keywords: Formal Logic, Deduction, Artificial Intelligence}
}
Document
DOI: 10.4230/DagSemProc.09411.2
09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions

Authors: Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
This seminar was the ninth in the series of the Dagstuhl "Deduction" seminars held biennially since 1993. Its goal was to bring together the closely related but unnecessarily disjoint communities of researchers working in interactive and automatic program verification.
Cite as

Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow. 09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ball_et_al:DagSemProc.09411.2,
  author =	{Ball, Thomas and Giesl, J\"{u}rgen and H\"{a}hnle, Reiner and Nipkow, Tobias},
  title =	{{09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.2},
  URN =		{urn:nbn:de:0030-drops-24213},
  doi =		{10.4230/DagSemProc.09411.2},
  annote =	{Keywords: Formal Logic, Deduction, Artificial Intelligence}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact