Travelled to:1 × France
1 × Poland
2 × United Kingdom
3 × USA
Collaborated with:M.M.K.Martin R.Alur M.Y.Vardi M.Glusman G.Kamhi R.Fraer L.Fix E.Singerman A.Tiemeyer A.Udupa A.Raghavan J.V.Deshmukh L.Maranget S.Sarkar K.Memarian J.Alglave S.Owens P.Sewell D.Williams T.Arons E.Elster M.Mishaeli J.Shalev L.D.Zuck R.Armoni A.Flaisher R.Gerth B.Ginsburg T.Kanza A.Landver Y.Zbar
Talks about:memori (3) model (3) consist (2) tempor (2) litmus (2) test (2) multiprocessor (1) counterexampl (1) protocol (1) properti (1)
Person: Sela Mador-Haim
DBLP: Mador-Haim:Sela
Contributed to:
2013
2012
201120102005
20032002Wrote 7 papers:
- PLDI-2013-UdupaRDMMA #named #protocol #specification
- TRANSIT: specifying protocols with concolic snippets (AU, AR, JVD, SMH, MMKM, RA), pp. 287–296.
- CAV-2012-Mador-HaimMSMAOAMSW #axiom #memory management #multi
- An Axiomatic Memory Model for POWER Multiprocessors (SMH, LM, SS, KM, JA, SO, RA, MMKM, PS, DW), pp. 495–512.
- DAC-2011-Mador-HaimAM #consistency #how #memory management #modelling #question #testing
- Litmus tests for comparing memory consistency models: how long do they need to be? (SMH, RA, MMKM), pp. 504–509.
- CAV-2010-Mador-HaimAM #consistency #generative #memory management #modelling #testing
- Generating Litmus Tests for Contrasting Memory Consistency Models (SMH, RA, MMKM), pp. 273–287.
- CAV-2005-AronsEFMMSSTVZ #verification
- Formal Verification of Backward Compatibility of Microcode (TA, EE, LF, SMH, MM, JS, ES, AT, MYV, LDZ), pp. 185–198.
- TACAS-2003-GlusmanKMFV #abstraction #evaluation #industrial #multi #refinement
- Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation (MG, GK, SMH, RF, MYV), pp. 176–191.
- TACAS-2002-ArmoniFFGGKLMSTVZ #logic
- The ForSpec Temporal Logic: A New Temporal Property-Specification Language (RA, LF, AF, RG, BG, TK, AL, SMH, ES, AT, MYV, YZ), pp. 296–211.