Dear all,
The next talk in the IARCS Verification Seminar Series will be given
by Ashwani Anand, a final-year PhD scholar at the Max Planck Institute for
Software Systems (MPI-SWS), advised by Rupak Majumdar and Anne-Kathrin
Schmuck. The talk is scheduled on Tuesday, February 10, at 1900 hrs IST (add
to Google calendar
<https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=Njg0M29ib3UxdGkzZTY0cTJqZzRjZDkzY2kgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com>
).
The details of the talk can be found on our webpage (
https://fmindia.cmi.ac.in/vss/), and also appended to the body of this
email.
The Verification Seminar Series, an initiative by the Indian Association
for Research in Computing Science (IARCS), is a monthly, online
talk-series, broadly in the area of Formal Methods and Programming
Languages, with applications in Verification and Synthesis. The aim of this
talk-series is to provide a platform for Formal Methods researchers to
interact regularly. In addition, we hope that it will make it easier for
researchers to explore newer problems/areas and collaborate on them, and
for younger researchers to start working in these areas.
All are welcome to join.
Best regards,
Organizers, IARCS Verification Seminar Series
=============================================================
Title: Following the STARS: Dynamic ω-Regular Shielding of Learned Policies
Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)
Abstract:
In this talk, I will present a novel dynamic post-shielding framework that
enforces the full class of ω-regular correctness properties over
pre-computed probabilistic policies. This constitutes a paradigm shift from
the predominant setting of safety-shielding — i.e., ensuring that nothing
bad ever happens — to a shielding process that additionally enforces
liveness — i.e., ensures that something good eventually happens. At the
core, our method uses Strategy-Template-based Adaptive Runtime Shields
(STARs), which leverage permissive strategy templates to enable
post-shielding with minimal interference. As its main feature, STARs
introduce a mechanism to dynamically control interference, allowing a
tunable enforcement parameter to balance formal obligations and
task-specific behavior at runtime. This allows to trigger more aggressive
enforcement when needed, while allowing for optimized policy choices
otherwise. In addition, STARs support runtime adaptation to changing
specifications or actuator failures, making them especially suited for
cyber-physical applications. We evaluate STARs on a mobile robot benchmark
to demonstrate their controllable interference when enforcing
(incrementally updated) ω-regular correctness properties over learned
probabilistic policies.
This talk is based on joint work with Satya Prakash Nayak, Ritam Raha and
Anne-Kathrin Schmuck, which will appear at AAMAS 2026.
Bio: Ashwani Anand is a final-year PhD scholar at the Max Planck Institute
for Software Systems (MPI-SWS), advised by Rupak Majumdar and Anne-Kathrin
Schmuck. Prior to MPI-SWS, he earned a Master’s in Computer Science and a
Bachelor’s in Mathematics and Computer Science from the Chennai
Mathematical Institute. His research focuses on the synthesis and
verification of distributed systems, using two-player game models to
construct systems that meet formal specifications—correct by construction,
while remaining robust to change in practice. More recently, Ashwani’s work
has turned to providing formal guarantees for learned models to enable
safer automated systems.