Verifying Safety of Distributed Systems

Explore a comprehensive lecture on verifying the safety of distributed systems presented by Professor Mooly Sagiv. Delve into two ongoing efforts aimed at tackling the challenges of developing and testing these complex systems. Learn about IVY, an interactive static analysis tool for proving safety in infinite-state systems with unbounded nodes, combining SAT solver automation and user interaction. Discover the RML modeling language and its role in effective verification. Examine the verification of stateful networks with Middleboxes, understanding their abstract effects and the complexity of stateful network verification. Gain insights from a leading researcher in large-scale program analysis and shape analysis, covering essential topics in programming languages, compilers, and software composition.