|
PUBLIC VIVA-VOCE NOTIFICATION Lecture Hall 6, 10:30 am Scalable Safety Verification of Statechart-like Programs Kumar Madhukar Chennai Mathematical Institute. 26-11-18 Abstract Proving correctness of software is one of the most central challenges in computer science. Modern state-of-the-art verification techniques still fail to scale to large, real-life systems. Our work is aimed at addressing this problem, under the principal thesis that it is useful to exploit the source-level syntactic and semantic structure of a given design, or an implementation, for improving the scalability of safety verification. This thesis focuses on three important aspects integral to Statechart-like systems, namely concurrency, cyclicity and size, and explores techniques to overcome their effect on scalability of software verifiers. In particular, the following questions are investigated: 1. For synchronous reactive systems modeled as Statemate Statecharts, is it possible to analyze synchronous concurrency explicitly, rather than encoding it as part of the system’s implementation? 2. Do loop accelerators enable existing program analysis algorithms to discover loop invariants more reliably and more efficiently? 3. Is it possible to generate counterexamples in a modular way to speed up safety refutation? 4. Is there a compositional approach to k-induction, in an abstraction-refinement framework that allows a component-wise refinement instead of a monolithic one? In this talk, we will take a quick look at these problems and our results, and shall discuss the problem of modular safety refutation in some details. All are invited to attend the viva-voce examination.
|
