BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Canada
1 × Estonia
1 × Finland
1 × India
1 × Japan
2 × Italy
3 × France
4 × United Kingdom
7 × USA
Collaborated with:
C.Enea A.Bouajjani R.Majumdar A.Lal J.Hamza Z.Rakamaric S.Qadeer B.K.Ozkan S.Tasiran R.Jhala G.Parlato R.Manevich D.Giannakopoulou C.S.Pasareanu K.Sen R.Biswas P.Ganty F.Rosa-Velardo M.F.Atig E.Kohler J.S.Fischer S.O.Mutluergil A.Haran M.Carter J.Chen C.Hawblitzel F.Perry J.Condit D.Coetzee P.Pratikaki
Talks about:
program (9) concurr (6) verifi (6) asynchron (4) lineariz (3) monitor (3) consist (3) analysi (3) object (3) refin (3)

Person: Michael Emmi

DBLP DBLP: Emmi:Michael

Contributed to:

CAV 20152015
ESOP 20152015
ICALP (2) 20152015
PLDI 20152015
POPL 20152015
TACAS 20152015
CAV 20142014
ESOP 20132013
CAV 20122012
FSE 20122012
POPL 20122012
SAS 20122012
TACAS 20122012
POPL 20112011
SAS 20112011
PLDI 20102010
TACAS 20092009
FM 20082008
PLDI 20082008
ISSTA 20072007
POPL 20072007
VMCAI 20072007
ESOP 20172017
CAV (2) 20172017
CAV (1) 20182018
CAV (2) 20192019
POPL 20162016
POPL 20182018
POPL 20192019

Wrote 30 papers:

CAV-2015-OzkanET #android #debugging
Systematic Asynchrony Bug Exploration for Android Apps (BKO, ME, ST), pp. 455–461.
ESOP-2015-EmmiGMR #analysis #source code
Analysis of Asynchronous Programs with Event-Based Synchronization (ME, PG, RM, FRV), pp. 535–559.
ICALP-v2-2015-BouajjaniEEH #on the #reachability
On Reducing Linearizability to State Reachability (AB, ME, CE, JH), pp. 95–107.
PLDI-2015-EmmiEH #monitoring #reasoning #refinement
Monitoring refinement via symbolic reasoning (ME, CE, JH), pp. 260–269.
POPL-2015-BouajjaniEEH #concurrent #refinement
Tractable Refinement Checking for Concurrent Objects (AB, ME, CE, JH), pp. 651–662.
TACAS-2015-HaranCELQR #composition #contest #verification
SMACK+Corral: A Modular Verifier — (Competition Contribution) (AH, MC, ME, AL, SQ, ZR), pp. 451–454.
CAV-2014-RakamaricE #implementation #named #verification
SMACK: Decoupling Source Language Details from Verifier Implementations (ZR, ME), pp. 106–113.
ESOP-2013-BouajjaniEEH #concurrent #source code #specification #verification
Verifying Concurrent Programs against Sequential Specifications (AB, ME, CE, JH), pp. 290–309.
CAV-2012-AtigBEL #detection #parallel #source code #thread
Detecting Fair Non-termination in Multithreaded Programs (MFA, AB, ME, AL), pp. 210–226.
FSE-2012-EmmiLQ #source code
Asynchronous programs with prioritized task-buffers (ME, AL, SQ), p. 48.
POPL-2012-BouajjaniE #analysis #parallel #recursion #source code
Analysis of recursively parallel programs (AB, ME), pp. 203–214.
SAS-2012-EmmiL #distributed #source code
Finding Non-terminating Executions in Distributed Asynchronous Programs (ME, AL), pp. 439–455.
TACAS-2012-BouajjaniE #analysis #bound #message passing #source code
Bounded Phase Analysis of Message-Passing Programs (AB, ME), pp. 451–465.
POPL-2011-EmmiQR #bound #scheduling
Delay-bounded scheduling (ME, SQ, ZR), pp. 411–422.
SAS-2011-BouajjaniEP #concurrent #on the #source code
On Sequentializing Concurrent Programs (AB, ME, GP), pp. 129–145.
PLDI-2010-EmmiMM #transaction #verification
Parameterized verification of transactional memories (ME, RM, RM), pp. 134–145.
TACAS-2009-EmmiJKM #implementation #verification
Verifying Reference Counting Implementations (ME, RJ, EK, RM), pp. 352–367.
FM-2008-EmmiGP #automaton #interface #verification
Assume-Guarantee Verification for Interface Automata (ME, DG, CSP), pp. 116–131.
PLDI-2008-ChenHPECCP #compilation #object-oriented #optimisation #scalability
Type-preserving compilation for large-scale optimizing object-oriented compilers (JC, CH, FP, ME, JC, DC, PP), pp. 183–192.
ISSTA-2007-EmmiMS #database #generative
Dynamic test input generation for database applications (ME, RM, KS), pp. 151–162.
POPL-2007-EmmiFJM
Lock allocation (ME, JSF, RJ, RM), pp. 291–296.
VMCAI-2007-EmmiM #transaction #verification
Verifying Compensating Transactions (ME, RM), pp. 29–43.
ESOP-2017-BouajjaniEEOT #concurrent #robust #source code #verification
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency (AB, ME, CE, BKO, ST), pp. 170–200.
CAV-2017-BouajjaniEEM #proving #simulation #using
Proving Linearizability Using Forward Simulations (AB, ME, CE, SOM), pp. 542–563.
CAV-2018-EmmiE #consistency #monitoring
Monitoring Weak Consistency (ME, CE), pp. 487–506.
CAV-2019-BiswasEE #complexity #consistency #data type #on the
On the Complexity of Checking Consistency for Replicated Data Types (RB, ME, CE), pp. 324–343.
CAV-2019-EmmiE #concurrent #generative #named #refinement #testing
Violat: Generating Tests of Observational Refinement for Concurrent Objects (ME, CE), pp. 534–546.
POPL-2016-EmmiE #data type #type inference
Symbolic abstract data type inference (ME, CE), pp. 513–525.
POPL-2018-EmmiE #concurrent #monitoring
Sound, complete, and tractable linearizability monitoring for concurrent collections (ME, CE), p. 27.
POPL-2019-EmmiE #specification
Weak-consistency specification via visibility relaxation (ME, CE), p. 28.

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.