Jason Yue Yang

RESEARCH INTERESTS

My research interests center around the design, analysis, and verification of complex software systems. I am also interested in related areas such as programming languages and compilers, software engineering, parallel and distributed computing, protocol design, embedded systems, and security.  

EDUCATION

• Ph.D. in Computer Science, University of Utah, GPA: 3.99/4.00, 05/2004

  Thesis: Formalizing Shared Memory Consistency Models for Program Analysis

  Advisors: Professor Ganesh Gopalakrishnan and Professor Gary Lindstrom

• M.E. in Computer Science, University of Utah, 06/1996

  Thesis project: Design and Application of a Portable Graphics Library

  Advisor: Professor Beat Bruderlin

• M.S. in Physics, Ohio State University, 12/1994

  Thesis: Molecular Dynamics Simulation of Fluid Flow in Confined Geometries

  Advisor: Professor Charles Ebner

• B.S. in Physics, Peking University, Beijing China, 07/1991

INDUSTRIAL EXPERIENCE

Enterasys Networks Corporation, Senior Firmware Engineer, 10/2001 – 04/2002

• Fully in charge of the switch fabric integration effort, a critical task for developing a high-end router product.

• Led the development effort for multicast protocol support. Implemented the routing table manager for DVMRP.

LSI Logic Corporation, Senior Software Engineer, 11/1996 – 09/2001

• Ported the Windows CE operating system to several MIPS-based microprocessors.

• Developed numerous device drivers for LSI Logic evaluation boards. The devices include graphics controller, Ethernet card, PCI controller, USB, I2C, EEPROM, Flash, RTC, IR, UART, keyboard/mouse, and sound card.

• Architected and developed the Service Tracking System (STS), a highly configurable web-based database system for tracking service requests and bug reports. This utility has been deployed by many company divisions and has dramatically increased their productivity and quality of service.

• Led the software development effort to support LSI Logic DVD decoders. Worked on-campus at Microsoft for several months and implemented a new video playback standard under an extremely tight schedule.

• Conducted internal trainings on DVD and compiler technologies.

• Participated in the BSPs (Board Support Packages) development for VxWorks and pSOS.

• Participated in the integration of the GNU tool chain for MIPS-based microprocessors.

Unisys Corporation, Software Engineer, 06/1996 – 11/1996

• Developed SCSI device drivers for the massively parallel Unisys servers.

• Optimized command utilities for the Unix SVR4 Micro Kernel.

Conceptual Geometry LLC, Consultant, 01/1996 – 06/1996

• Participated in the development of a portable graphics library.

• Designed and implemented the application software running on a special hand-held device for a military training system.

RESEARCH EXPERIENCE

University of Utah , Research Assistant, 08/1999 – 05/2004

• Developed a method to capture “programmer expectations” as constraints and automatically verify them using constraint solving. Applied this method to enable three important analyses: execution validation, race detection, and atomicity verification. Showed that the inter-thread memory model semantics must be combined with the intra-thread program semantics to enable such rigorous analyses for multithreaded programs. Built an analysis tool DefectFinder using constraint logic programming (CLP). 

• Developed a novel constraint-based approach that makes a memory model specification both declarative and executable.  Based on this approach, designed Nemos (Non-operational yet Executable Memory Ordering Specifications), an analytical framework for specifying and verifying axiomatic  memory models. 

• Developed an executable specification for the Intel Itanium memory ordering rules using the Nemos framework. Built a tool to analyze Itanium assembly programs. Demonstrated this tool at Intel and received highly encouraging feedback.

• Formalized a collection of classical memory models (including sequential consistency, coherence, PRAM, causal consistency, and processor consistency) using the Nemos framework, and conducted a formal comparative analysis.

• Designed UMM (Uniform Memory Model), a verification framework that integrates a built-in model checker with a generic memory abstraction for analyzing operational memory model specifications. 

• Provided an alternative Java thread specification using the UMM framework based on a proposal from Manson and Pugh. Uncovered two flaws from the original proposal.  

• Applied the model checking technique to analyze the CRF Java memory model. Showed how to abstract a synchronization idiom using a litmus test to verify memory model compliance. This was the first effort to apply model checking for verifying language level thread semantics and common programming patterns.

Ohio State University, Research Assistant, 06/1993 – 06/1995

• Developed a computer simulation program based on molecular dynamics for analyzing fluid flow behaviors in microscopically confined geometries. 

• Devised a realistic wall model to explain the heat transfer effect in the flow process.  

TEACHING EXPERIENCE

 University of Utah, Teaching Assistant, 09/1995 – 03/1996

• Data Communications and Networks

• Advanced Algorithms and Data Structures

Ohio State University, Teaching Assistant, 09/1991 – 06/1993

• General Physics

• Advanced Physics Laboratory

PUBLICATIONS

Refereed Conference Proceedings and Journal Papers

• QB or not QB: An Efficient Execution Verification Tool for Memory Orderings

          Ganesh Gopalakrishnan, Yue Yang, and Hemanthkumar Sivaraj,

          in the 16th International Conference on Computer Aided Verification (CAV 2004), July 2004.  

• Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models

          Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slind,

          in the 18th International Parallel and Distributed Processing Symposium (IPDPS 2004).

• Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT

          Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slind, 

          in the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods 

          (CHARME'03), Oct 2003.  

• UMM: An Operational Memory Model Specification Framework with Integrated Model Checking Capability

          Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom,

          to appear in Concurrency and Computation: Practice and Experience.

• Specifying Java Thread Semantics Using a Uniform Memory Model

          Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom,

          in Joint ACM Java Grande – ISCOPE Conference, 2002.

• Analyzing the CRF Java Memory Model

          Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom,

          in the 8th Asia-Pacific Software Engineering Conference, 2001.

Ph.D. Dissertation

• Formalizing Shared Memory Consistency Models for Program Analysis

Papers Submitted

• Rigorous Concurrency Analysis of Multithreaded Programs

          Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom, November 2003.  

• A Constraint-Based Approach for Specifying Memory Consistency Models

          Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom,

          submitted to Theory and Practice of Logic Programming, December 2003.

Other Papers

• A Unified Framework for Handling Constraints During Program Analysis

          Yue Yang and Ganesh Gopalakrishnan,

          in Workshop on Constraint Programming and Constraint for Verification (CP+CV'04).

• Molecular Dynamics Simulation of Fluid Flow in Confined Geometries

          M.S. Thesis, Ohio State University, 1994.  

• ⁵⁷Fe Mossbauer Study of RTiFe₁₁N_x Compounds

          Senlin Ge, Qin Pan, GuoqiangYang, Jingsong Zhang, Yue Yang, Wei Tao, Yingchang Yang,

          Solid State Communications, 83(7)487, 1992.

RESEARCH SOFTWARE

• DefectFinder, an automatic and rigorous program analysis tool for checking concurrent software.

          Available at http://www.cs.utah.edu/~yyang/DefectFinder.zip.  

• NemosFinder, a verification tool for analyzing axiomatic memory models.

          Available at http://www.cs.utah.edu/~yyang/NemosFinder.html.  

• UMMChecker, a verification tool for analyzing operational memory models.

          Available at http://www.cs.utah.edu/~yyang/UMMChecker.html.

PATENT 

• Computer Music Input Apparatus and Processing Methods, patent pending.

AWARDS

• Conference Travel Grant: DAC Ph.D. Forum, IPDPS'04, JGI’02, APSEC'01

• Top LSI Logic Award (this award also carried a $5,000 cash prize), LSI Logic, 1998

• Best Teaching Assistant Award, Ohio State University, 1993

• Outstanding Student Award, Peking University, 1988

OTHER ACTIVITIES

• Referee for:

  - Concurrency and Computation: Practice and Experience

  - Formal Method in System Design

  - Journal of the ACM

  - Journal of Parallel and Distributed Computing

• Active contributor for the Java memory model discussion group.  

• Member of the men's basketball team at Peking University (1987 – 1989).

SKILLS

• Broad industrial experience in system software development.

• Highly proficient in C/C++, Java, Perl, MIPS/X86 assembly, SQL, Fortran, Prolog.

• In-depth knowledge of OS kernels, including Windows (NT/CE), Unix (Linux/FreeBSD/Solaris), VxWorks, pSOS.

• In-depth knowledge of networking protocols, such as TCP/IP, RIP/OSPF, DVMRP/PIM/SIM, RPC, and Sockets.

• Graphics: Tcl/TK, Java 2D/3D, DirectX, Motif.

• Verification tools: proficient in Murphi and Spin; knowledge of PVS and HOL.

CURRENT STATUS

• U.S. Permanent Resident, Citizen of China

REFERENCES

Professor Ganesh Gopalakrishnan Professor Gary Lindstrom Professor Konrad Slind Steve Lynch, Director of LSI Logic

ganesh@cs.utah.edu gary@cs.utah.edu slind@cs.utah.edu STEVELYNCH@aol.com

801-581-3568 801-581-5586 801-585-6795 801-272-5427