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: H=auml=hnle:Reiner
Facilitated 4 volumes:
Ed
Ed
Ed
EdContributed to:
2015
2015
2014201420142013
20132012
201120112011
2010200720072006
200320022001
2000199619941992
1990198620162017Wrote 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.