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: Merz:Stephan
Facilitated 1 volumes:
Contributed to:
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.
- FM-v2-1999-Merz
- 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.