Travelled to:1 × Australia
1 × Canada
1 × Finland
1 × Ireland
1 × Norway
1 × Singapore
1 × The Netherlands
1 × USA
1 × United Kingdom
1 × Uruguay
2 × Germany
4 × Italy
Collaborated with:W.Reif K.Stenzel J.Derrick H.Wehrheim A.Thums D.Haneberg H.Grandy M.Balser B.Tofan B.Dongol O.Travkin G.Ernst A.Dunets A.Schierl M.Bischof D.Hutter H.Mantel G.Rock W.Stephan A.Wolpers
Talks about:verifi (5) system (5) prove (5) kiv (5) lineariz (3) linearis (3) correct (3) formal (3) electron (2) develop (2)
Person: Gerhard Schellhorn
DBLP: Schellhorn:Gerhard
Contributed to:
20152014
2014
20122011
201120092008
2008200720062003
2001
20001998
1997
1997Wrote 19 papers:
- FM-2015-DerrickDSTW #transaction #verification
- Verifying Opacity of a Transactional Mutex Lock (JD, BD, GS, OT, HW), pp. 161–177.
- FM-2014-DerrickDSTTW #consistency #verification
- Quiescent Consistency: Defining and Verifying Relaxed Linearizability (JD, BD, GS, BT, OT, HW), pp. 200–214.
- IFM-2014-TofanSR #composition #multi #proving
- A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset (BT, GS, WR), pp. 357–372.
- CAV-2012-SchellhornWD #algorithm #how
- How to Prove Algorithms Linearisable (GS, HW, JD), pp. 243–259.
- FM-2011-DerrickSW #verification
- Verifying Linearisability with Potential Linearisation Points (JD, GS, HW), pp. 323–337.
- SEFM-2011-ErnstSR #analysis #empirical #interactive #proving #theorem proving #verification
- Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (GE, GS, WR), pp. 188–203.
- FM-2009-SchierlSHR #file system #memory management #specification
- Abstract Specification of the UBIFS File System for Flash Memory (AS, GS, DH, WR), pp. 190–206.
- FM-2008-GrandyBSSR #protocol #security #verification
- Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code (HG, MB, KS, GS, WR), pp. 165–180.
- TAP-2008-DunetsSR #analysis #bound #data type #relational
- Bounded Relational Analysis of Free Data Types (AD, GS, WR), pp. 99–115.
- IFM-2007-DerrickSW #proving #refinement
- Proving Linearizability Via Non-atomic Refinement (JD, GS, HW), pp. 195–214.
- IFM-2007-HanebergGRS #approach #smarttech #verification
- Verifying Smart Card Applications: An ASM Approach (DH, HG, WR, GS), pp. 313–332.
- FM-2006-SchellhornGHR #challenge #proving
- The Mondex Challenge: Machine Checked Proofs for an Electronic Purse (GS, HG, DH, WR), pp. 16–31.
- FME-2003-ThumsS #model checking
- Model Checking FTA (AT, GS), pp. 739–757.
- IJCAR-2001-ReifST #detection #specification
- Flaw Detection in Formal Specifications (WR, GS, AT), pp. 642–657.
- FASE-2000-BalserRSST #development
- Formal System Development with KIV (MB, WR, GS, KS, AT), pp. 363–366.
- FM-1998-BalserRSS
- KIV 3.0 for Provably Correct Systems (MB, WR, GS, KS), pp. 330–337.
- FM-1998-HutterMRSWBRSS #complexity #formal method #named
- VSE: Controlling the Complexity in Formal Software Developments (DH, HM, GR, WS, AW, MB, WR, GS, KS), pp. 351–358.
- CADE-1997-ReifSS #correctness #proving
- Proving System Correctness with KIV 3.0 (WR, GS, KS), pp. 69–72.
- TAPSOFT-1997-ReifSS #correctness #proving
- Proving System Correctness with KIV (WR, GS, KS), pp. 859–862.