BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Schellhorn:Gerhard

Contributed to:

FM 20152015
FM 20142014
IFM 20142014
CAV 20122012
FM 20112011
SEFM 20112011
FM 20092009
FM 20082008
TAP 20082008
IFM 20072007
FM 20062006
FME 20032003
IJCAR 20012001
FASE 20002000
FM-Trends 19981998
CADE 19971997

Wrote 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.
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.

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.