BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Belgium
1 × Canada
1 × Estonia
1 × India
1 × Spain
1 × Switzerland
1 × Uruguay
2 × France
2 × United Kingdom
3 × Germany
4 × Italy
5 × USA
Collaborated with:
R.Bubel B.Beckert M.Hentschel P.H.Schmitt C.Engel A.Wallenburg S.Klingenbeck I.Schaefer E.Albert S.Genaim G.Román-Díez C.C.Din A.Flores-Montoya R.Ji U.Geilmann O.Mürk D.Larsson K.Johannisson A.Ranta N.V.Murray E.Rosenthal R.Hasegawa Y.Shirai M.Giese S.Käsdorf M.Baum M.Rothe P.Oel M.Sulzmann S.Gerberding W.Kernig M.Heisel W.Reif W.Stephan F.Damiani E.Kamburjan M.Lienhardt S.d.Gouw J.Rot F.S.d.Boer G.Puebla V.Klebanov P.Rümmer S.Schlager D.Clarke N.Diakov E.B.Johnsen J.Schäfer R.Schlatte P.Y.H.Wong W.Ahrendt T.Baar E.Habermalz W.Menzel W.Mostowski
Talks about:
verif (8) interact (6) program (6) model (5) base (5) theorem (4) softwar (4) formal (4) execut (4) deduct (4)

Person: Reiner Hähnle

DBLP DBLP: H=auml=hnle:Reiner

Facilitated 4 volumes:

SFM 2014Ed
IJCAR 2010Ed
TAP 2008Ed
FASE 2019Ed

Contributed to:

CADE 20152015
CAV 20152015
IFM 20142014
SFM 20142014
TAP 20142014
CADE 20132013
SEFM 20132013
FASE 20122012
PEPM 20112011
SEFM 20112011
SFM 20112011
ASE 20102010
CADE 20072007
TAP 20072007
SEFM 20062006
FATES 20032003
FASE 20022002
IJCAR 20012001
CL 20002000
CADE 19961996
CADE 19941994
CADE 19921992
CSL 19901990
CADE 19861986
ASE 20162016
FASE 20172017

Wrote 32 papers:

CADE-2015-DinBH #concurrent #deduction #modelling #named #verification
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS (CCD, RB, RH), pp. 517–526.
CAV-2015-GouwRBBH #java
OpenJDK’s Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case (SdG, JR, FSdB, RB, RH), pp. 273–289.
IFM-2014-HentschelKHB #ide #interactive #verification
An Interactive Verification Tool Meets an IDE (MH, SK, RH, RB), pp. 55–70.
SFM-2014-BubelMH #analysis #execution #modelling
Analysis of Executable Software Models (RB, AFM, RH), pp. 1–25.
TAP-2014-HentschelHB #bound #execution #symbolic computation #visualisation
Visualizing Unbounded Symbolic Execution (MH, RH, RB), pp. 82–98.
CADE-2013-HahnleSB #reuse #verification
Reuse in Software Verification by Abstract Method Calls (RH, IS, RB), pp. 300–314.
SEFM-2013-JiHB #deduction #execution #program transformation #symbolic computation
Program Transformation Based on Symbolic Execution and Deduction (RJ, RH, RB), pp. 289–304.
FASE-2012-AlbertBGHR #source code
Verified Resource Guarantees for Heap Manipulating Programs (EA, RB, SG, RH, GRD), pp. 130–145.
PEPM-2011-AlbertBGHPR #using
Verified resource guarantees using COSTA and KeY (EA, RB, SG, RH, GP, GRD), pp. 73–76.
SEFM-2011-BubelHG #formal method #java #specification #string #verification
A Formalisation of Java Strings for Program Specification and Verification (RB, RH, UG), pp. 90–105.
SFM-2011-ClarkeDHJSSSW #behaviour #modelling #variability
Modeling Spatial and Temporal Variability with the HATS Abstract Behavioral Modeling Language (DC, ND, RH, EBJ, IS, JS, RS, PYHW), pp. 417–457.
ASE-2010-HahnleBBR #debugging #execution #interactive #symbolic computation #visual notation
A visual interactive debugger based on symbolic execution (RH, MB, RB, MR), pp. 143–146.
CADE-2007-BeckertGHKRSS #component #deduction
The KeY system 1.0 (Deduction Component) (BB, MG, RH, VK, PR, SS, PHS), pp. 379–384.
CADE-2007-MurkLH #c #named #source code #verification
KeY-C: A Tool for Verification of C Programs (OM, DL, RH), pp. 385–390.
TAP-2007-EngelH #generative #proving #testing
Generating Unit Tests from Formal Proofs (CE, RH), pp. 169–188.
SEFM-2006-BeckertHS #deduction #design #object-oriented #verification
Integrating Object-Oriented Design and Deductive Verification of Software (BB, RH, PHS), p. 260.
FATES-2003-HahnleW #proving #testing #theorem proving #using
Using a Software Testing Technique to Improve Theorem Proving (RH, AW), pp. 30–41.
FASE-2002-AhrendtBBGHHMMS #design #formal method #object-oriented
The KeY System: Integrating Object-Oriented Design and Formal Methods (WA, TB, BB, MG, EH, RH, WM, WM, PHS), pp. 327–330.
FASE-2002-HahnleJR #authoring #requirements #specification
An Authoring Tool for Informal and Formal Requirements Specifications (RH, KJ, AR), pp. 233–248.
IJCAR-2001-HahnleMR #graph #order
Ordered Resolution vs. Connection Graph Resolution (RH, NVM, ER), pp. 182–194.
CL-2000-HahnleHS #constraints #finite #generative #proving #theorem proving
Moder Generation Theorem Proving with Finite Interval Constraints (RH, RH, YS), pp. 285–299.
CADE-1996-BeckertHOS #proving #theorem proving
The Tableau-based Theorem Prover 3TAP Version 4.0 (BB, RH, PO, MS), pp. 303–307.
CADE-1994-KlingenbeckH #semantics #strict
Semantic Tableaux with Ordering Restrictions (SK, RH), pp. 708–722.
CADE-1992-BeckertGHK #logic #multi #proving #theorem proving
The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics (BB, SG, RH, WK), pp. 758–760.
CADE-1992-BeckertH #semantics #similarity
An Improved Method for Adding Equality to Free Variable Semantic Tableaux (BB, RH), pp. 507–521.
CSL-1990-Hahnle #logic #multi #performance #proving #towards
Towards an Efficient Tableau Proof Procedure for Multiple-Valued Logics (RH), pp. 248–260.
CADE-1986-HahnleHRS #interactive #logic #verification
An Interactive Verification System Based on Dynamic Logic (RH, MH, WR, WS), pp. 306–315.
ASE-2016-HentschelHB #empirical #evaluation #interactive #user interface #verification
An empirical evaluation of two user interfaces of an interactive program verifier (MH, RH, RB), pp. 403–413.
ASE-2016-HentschelHB16a #comprehension #debugging #effectiveness #interactive #proving #verification
The interactive verification debugger: effective understanding of interactive proof attempts (MH, RH, RB), pp. 846–851.
FASE-2017-DamianiHKL #programming
A Unified and Formal Programming Model for Deltas and Traits (FD, RH, EK, ML), pp. 424–441.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.