Explore formal verification techniques for complex systems in this 43-minute lecture by Professor Alessandro Abate at the Alan Turing Institute. Delve into innovative approaches that combine model-based and data-driven methods to address limitations in standard formal verification techniques. Learn about a new measurement-driven and model-based automated technique for quantitative verification of systems with partly unknown dynamics, formulated as a data-driven Bayesian inference problem. Discover the concept of 'Logically Constrained Reinforcement Learning' for learning actions in a model while verifying logical constraints. Gain insights into applications for complex physical systems, including Cyber-Physical Systems (CPS) and building automation systems. Explore topics such as parametric Markov chains, parameter synthesis, confidence computation, and strategy synthesis for experiment design. Understand how this research pushes the boundaries of existing algorithms and tools in formal verification, offering potential solutions for large-scale, complex models. Read more