|
|
| |
 |
|
Yuan Yu
Senior Researcher
Microsoft Research Silicon Valley
1065 La Avenida
Mountain View, CA 94043
Tel. +1 650.693.1607
|
I joined Microsoft Research Silicon Valley in 2002. My current research
focuses on distributed systems for large-scale data parallel computing. I have
been mainly working on DryadLINQ
and Dryad to build
a programming environment for large-scale data parallel computing.
I am currently leading the DryadLINQ project. While at Microsoft
Research, I also led the RaceTrack
project, and developed the TLC
model checker. Before joining MSR, I worked for 9 years at DEC/Compaq
Systems Research Center.
RESEARCH INTERESTS:
Static and runtime program analysis, distributed systems, formal specification and verification,
model checking, theorem proving, and software configuration and management.
SELECTED PUBLICATIONS:
Books:
Software Configuration Management Using Vesta, with Allan Heydon,
Roy Levin, and Timothy Mann, Monographs in Computer Science,
Springer Verlag, 262 pages, February 2006.
Articles:
Dryad: Distributed Data-Parallel Programs from Sequential Building Blocks,
with Michael Isard, Mihai Budiu, Andrew Birrell, and Dennis Fetterly.
European Conference on Computer Systems (EuroSys), Lisbon, Portugal,
March 21-23, 2007
RaceTrack: Efficient Detection of Data Race Conditions via Adaptive
Tracking, with Thomas Rodeheffer and Wei Chen. In Proceedings of the
20th ACM Symposium on Operating Systems Principles (SOSP), Brighton, UK,
October 23-26, 2005.
Using a formal specification and a model checker to monitor
and direct simulation, with Serdar Tasiran and Brannon Batson. In
Proceedings of the 40th ACM/IEEE Design Automation Conference (DAC'03),
San Diego, CA, 2003.
Checking Cache Coherence Protocols with TLA+, with Rajeev
Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, and Mark
Tuttle. Formal Methods in System Design 22, 2 (March 2003) 125-131.
The Vesta Software Configuration Management System, with
Allan Heydon, Roy Levin and Tim Mann. Research Report 177, Compaq Systems
Research Center, Palo Alto, CA, Janurary 2002.
Caching Function Calls Using Precise Dependencies, with
Allan Heydon and Roy Levin. In Proceedings of the ACM SIGPLAN '00
Conference on Programming Language Design and Implementation (PLDI),
pages 311-320. ACM Press, June 2000.
Model Checking TLA+ Specifications, with Leslie Lamport and
Panagiotis Manolios. In Correct Hardware Design and Verification
Methods (CHARME '99), Lecture Notes in Computer Science 1703,
Springer-Verlag, September 1999.
Alpha Shared Memory Model. In Alpha Architecture Reference
Manual, Alpha Architecture Commmittee, Digital Press, Boston, third
edition, 1998.
Automated Proofs of Object Code for a Widely Used Microprocessor,
with Robert S. Boyer. Journal of the ACM, Pages 166--192, Vol43(1),
Janurary 1996.
Automated Correctness Proofs of Machine Code Programs for a
Commercial Microprocessor, with Robert S. Boyer. In Proceedings of
the 11th International Conference on Automated Deduction (CADE), Lecture
Notes in Computer Science 607, Springer-Verlag, 1992.
|
|
