BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Martingale-based Methods for Formal Verification and Certified Con
 trol of Stochastic Systems
DTSTART:20220725T140000
DTEND:20220725T150000
DTSTAMP:20260407T021153Z
UID:622298e090c1250480afdced564c2e10ab8df3112d95380af8b8fec6
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Djordje Zikelic \n\n\n\n\n\n\n\n\nAbstract\n\n\n\n\n\n\n\n\
 n\n\nThis talk will advocate for the use of martingale-based methods towar
 ds the formal verification of infinite state stochastic systems. Stocha
 sticity is commonly used to model and quantify uncertainty in a system\, a
 nd martingale-based methods present a promising approach to the formal ve
 rification of stochastic systems with applications in PL and AI. The key a
 dvantage of martingale-based methods is that they provide formal soundne
 ss and even certain level of theoretical completeness guarantees\, while a
 llowing for fully automated verification algorithms for stochastic syste
 m verification. In this talk\, we present martingale-based methods for st
 atic analysis of probabilistic programs as well as for learning stabilizin
 g control policies in stochastic systems with formal guarantees on stabili
 zation. First\, we show that martingale-based methods can be used to desi
 gn sound and fully automated algorithms for the verification of terminatio
 n and safety properties in probabilistic programs. Second\, we present a r
 ecent method that utilizes martingales in order to either learn or formall
 y verify a stabilizing policy for a stochastic system. Stability is one of
  the most important safety properties of control systems which requires th
 e agent to eventually reach and stabilize within some specified region wit
 h probability 1. Our method learns a control policy together with a marti
 ngale-based certificate that formally certifies almost-sure stability of t
 he learned policy\, both parametrized as neural networks.\n\nBio\nDjordje 
 is a PhD student in computer science at IST Austria\, under the supervisio
 n of Krishnendu Chatterjee and Petr Novotný. His research focuses on deve
 loping algorithms for formally verifying correctness of software and combi
 ne ideas from formal verification\, programming languages and machine lear
 ning in order to design mathematically rigorous yet fully automated method
 s for providing formal guarantees about programs\, systems with learned co
 mponents and safe learning. Prior to joining IST Austria\, he completed hi
 s bachelor's and master's degrees in mathematics at the University of Camb
 ridge.\n\n \n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/68895790153?pwd=OEJhMTNsalFlSDJybGRDV0xBZ0U5Zz09
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR