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: Emmi:Michael
Contributed to:
2015
2015
2015
2015
2015
2015201420132012
20122012
201220122011201120102009
20082008
20072007
20072017201720182019201620182019Wrote 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.