闫士博 / ShiBo Yan Stochastic Systems · Reach-Avoid Control · Formal Guarantees
中 EN
Southwest University · M.Eng. student in Software Engineering

I study how to synthesize reach-avoid controllers for stochastic systems and provide verifiable probabilistic guarantees.

Under stochastic disturbances, a system must reach its target region while avoiding unsafe regions beforehand. My work focuses on synthesizing controllers that meet this requirement and using formal methods to establish a lower bound on the probability of satisfying it.

Outside my core research, I also turn recurring problems in research, study, and content processing into software that I expect to keep using.

Explore my research View my resume
Current work

What I’m working on.

Since beginning graduate study, I have spent most of my time on the following three projects.

  1. RL Reference Policy
  2. Sparse Polynomial Controller
  3. Stochastic Barrier-like Certificate
  4. Certified Probability Lower Bound
Research

Learning-aided reach-avoid controller synthesis

Starting from a reference policy obtained through reinforcement learning, I construct sparse polynomial controllers that are easier to verify. I then use stochastic barrier-like certificates to compute and iteratively improve a verifiable lower bound on the reach-avoid probability.

View the research background
Funded research

Formal safety verification of neural-network control policies

I contribute to an NSFC General Program project on safety verification for neural-network control systems using polynomial algebraic methods.

Engineering

CBF-Rover: Vision-based reinforcement-learning simulation platform

I am responsible for system architecture, safety constraints, and simulation training. The current focus is online computation, visualization, and closed-loop validation of barrier certificates, with an interface reserved for embedded deployment.

View the project record
Updates

Recent updates.

This section records paper and project updates from the past year. Last updated in .

  • Paper acceptedMy first-author paper, Learning-Aided Reach-Avoid Controller Synthesis with Formal Guarantees for Stochastic Systems, has been accepted at MEMOCODE 2026.
  • Journal reviewA paper on safety guarantees for Bayesian-neural-network control policies is under review at Formal Aspects of Computing; my supervisor is first author, and I am second author.
  • Under reviewA related paper on reach-avoid controller synthesis for stochastic systems is currently under review.
  • Project updateI am advancing the CBF-Rover simulation platform, focusing on online computation, visualization, and closed-loop validation of barrier certificates.
Beyond research

Beyond research.

Away from papers and code, I listen to music and make time to ask why things work the way they do. This site records not only my current research, but also the studies, projects, and milestones that led here.

View the full profile

Ten years hence, they shall remember me; the whole nation still mad—with whom shall I speak?
The world without bounds, my aspirations without end; amid the vastness of sea and sky, long I stand.