Yang Zhao

Ph.D., software engineer, retired researcher

I am a software engineer currently living in Seattle area. My interests are building reliable and efficient cloud-based distributed systems serving all types of scenarios.

I used to be an active researcher on formal verification and model checking. I am looking into opportunities to apply formal verification to real software projects.

I came from Xi'an, China. Before moving to Seattle, WA, I lived in Riverside, CA for several years, and got married with my wife there.

This website is created using this github repro as the template. Kudos to the author!

Last update: January, 2026.

Experience

Senior Software Engineear

Salesforce

Agentforce reasoner/MCP team. Our team grew from a research project in Salesforce AI research. Now we are building next generation of reasoner in Agentforce.

  • MCP support in Agentforce
  • Deterministic agent graph
  • RAG

Tableau Query team: contribute to the core library transforming an internal query language in Tableau to executable queries on various databases.

  • Monitor data pipeline: from Flink job, Apache Airflow, and Hive/Iceberg tables
  • Common table expression support
  • Stored procedure support
September 2021 - Present

Software Engineer 2

Microsoft

I worked in several different teams in Microsoft:

  • Azure deployment:
  • Microsoft Hyper-Converge Infrastruction (HCI):
  • Failover clustering in Windows Server:
August 2013 - August 2021

Skills

I worked in several different domains, including formal verification, distributed system/storage, query processing/optimization, RAG, and AI agent.

Programming Languages & Tools
  • Python
  • C/C++
  • C#/.Net
  • Java

Education

University of California, Riverside

Ph.D.
Computer Science

Research topics: formal verification, model checking, Markov chain analysis, decision diagram

September 2008 - July 2013

Institute of Computing Technology, Chinese Academy of Sciences

M.S.
Computer Science

Research topics: hardware verification, SAT problem

September 2005 - July 2008

Peking University

B.S.
Electrical Engineer
September 2001 - July 2005

Publications

Conference paper:
  • Yang Zhao and Kristin Yvonne Rozier, Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems , IEEE/ACM 2014 International Conference on Computer-Aided Design (ICCAD), IEEE/ACM, November, 2014
  • Yang Zhao and Gianfranco Ciardo, A Two-Phase Gauss-Seidel Algorithm for Steady-state Solution of Structured CTMCs Encoded with EVMDDs , QEST 2012. [ Webpage about Flip model in the paper ]
  • Yang Zhao and Xiaoqing Jin and Gianfranco Ciardo, A Symbolic Algorithm for Shortest EG Witness Generation , 5th IEEE International Conference on Theoretical Aspects of Software Engineering (TASE 2011), pages 68-75, IEEE Computer Society. [ PDF ]
  • Yang Zhao and Gianfranco Ciardo, Symbolic Computation of Strongly Connected Components Using Saturation , Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, pages 202-211, Langley Research Center, Hampton VA 23681-2199, USA, April 2010. NASA. [ PDF ]
  • Yang Zhao and Gianfranco Ciardo, Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation , In Proc. 7th International Symposium on Automated Technology for Verification and Analysis (ATVA), LNCS 5799, pages 368-381. Macao, China, Oct. 2009. [ PDF ]
Journal paper:
  • Yang Zhao and Kristin Yvonne Rozier, Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System , In Science of Computer Programming Journal, volume 96, number 3, pages 337-353, Elsevier, December, 2014
  • Gianfranco Ciardo and Yang Zhao and Xiaoqing Jin, Ten Years of Saturation: A Petri Net Perspective , Transactions on Petri Nets and Other Models of Concurrency V, pages 51-95, vol.6900. [ Link ]
  • Yang Zhao and Gianfranco Ciardo, Symbolic Computation of Strongly Connected Components and Fair Cycles Using Saturation , Innovations in Systems and Software Engineering. [ Link ]
Workshop paper:
  • Yang Zhao and Gianfranco Ciardo, Tackling Truncation Errors in CSL Model Checking through Bounding Semantics , EPEW 2013 accepted .[ Webpage ]
  • Yang Zhao and Kristin Y. Rozier, Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System , International Workshop on Automated Verification of Critical Systems (AVoCS 2012), to appear