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 × Austria
1 × Germany
1 × USA
2 × Poland
3 × United Kingdom
4 × France
Collaborated with:
P.Fontaine B.W.Paleo F.Bourdoncle D.Doligez L.Lamport C.Weidenbach H.Fekih L.J.B.Ayed M.Hammer A.Knapp M.Wirsing J.Zappe D.Cansell D.Méry J.P.Bahsoun C.Servieres D.Déharbe K.Chaudhuri J.Marion L.P.Nieto A.F.Tiu D.Cousineau D.Ricketts H.Vanzetto
Talks about:
proof (4) system (3) tla (3) diagram (2) specif (2) combin (2) check (2) smt (2) transform (1) polymorph (1)

Person: Stephan Merz

DBLP DBLP: Merz:Stephan

Facilitated 1 volumes:

IFM 2010Ed

Contributed to:

FM 20122012
IJCAR 20122012
CADE 20112011
IJCAR 20102010
SAC 20062006
TACAS 20062006
TACAS 20052005
FASE 20032003
IFM 20002000
World Congress on Formal Methods 19991999
POPL 19971997
FSE 19931993

Wrote 13 papers:

FM-2012-CousineauDLMRV #proving
TLA + Proofs (DC, DD, LL, SM, DR, HV), pp. 147–154.
IJCAR-2012-FontaineMW #decidability
Combination of Disjoint Theories: Beyond Decidability (PF, SM, CW), pp. 256–270.
CADE-2011-DeharbeFMP #problem #smt #symmetry
Exploiting Symmetry in SMT Problems (DD, PF, SM, BWP), pp. 222–236.
CADE-2011-FontaineMP #proving
Compression of Propositional Resolution Proofs via Partial Regularization (PF, SM, BWP), pp. 237–251.
IJCAR-2010-ChaudhuriDLM #proving #safety #verification
Verifying Safety Properties with the TLA+ Proof System (KC, DD, LL, SM), pp. 142–148.
SAC-2006-FekihAM #diagrams #specification #state machine #uml
Transformation of B specifications into UML class diagrams and state machines (HF, LJBA, SM), pp. 1840–1844.
TACAS-2006-FontaineMMNT #automation #interactive #proving #smt #towards
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants (PF, JYM, SM, LPN, AFT), pp. 167–181.
TACAS-2005-HammerKM #ltl #model checking #on the fly
Truly On-the-Fly LTL Model Checking (MH, AK, SM), pp. 191–205.
FASE-2003-MerzWZ #logic #mobile #refinement #specification
A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems (SM, MW, JZ), pp. 87–101.
IFM-2000-CansellMM #diagrams #verification
Predicate Diagrams for the Verification of Reactive Systems (DC, DM, SM), pp. 380–397.
A More Complete TLA (SM), pp. 1226–1244.
POPL-1997-BourdoncleM #higher-order #multi #polymorphism
Type-Checking Higher-Order Polymorphic Multi-Methods (FB, SM), pp. 302–315.
FSE-1993-BahsounMS #concurrent #formal method #framework #programming
A Framework for Programming and Formalizing Concurrent Objects (JPB, SM, CS), pp. 126–137.

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.