闫士博 / 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: Safe Control for Mobile Robots under Stochastic Disturbances

I independently developed the system model, policy training, and safety constraints, combining certificate-guided controller optimization with online CBF action correction and testing closed-loop behavior across disturbance and obstacle trajectories.

View the project record
Updates

Recent updates.

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

  • Published paperMy first-author paper, Learning-Aided Reach-Avoid Controller Synthesis with Formal Guarantees for Stochastic Systems, is published online in MEMOCODE 2026 (a constituent conference of ESWEEK 2026). The original paper is linked under research outcomes.
  • Journal submissionA paper on safety guarantees for Bayesian neural-network control policies has been submitted to Formal Aspects of Computing; my supervisor is first author, and I am second author.
  • Conference submissionFollow-up work on reach-avoid controller synthesis and formal probabilistic guarantees for stochastic systems has been submitted to a CCF Class A conference.
  • Project resultsI independently developed CBF-Rover from March 2025 to July 2026, covering controller optimization, online CBF correction, and simulations across multiple scenarios. Research probability lower bounds and empirical robot validation are reported separately.
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.