|
3:30 pm, Seminar Hall Automating Deductive Verification using Decision-Tree Based Learning Deepak D'Souza IISc Bangalore. 26-11-18 Abstract The Floyd-Hoare style of proving assertions in programs involves coming up with logical annotations at different program points, that are consistent with the semantics of the program statements and adequate in that they are strong enough to imply the given assertions. Proofs in this style have the potential to be a lot more scalable than verification approaches like model-checking that rely on exhaustive search of the state-space of the program, since complex programs may often have simple proofs of the assertions in them. While a large part of these proofs can be automated using a verification engine that checks consistency and adequacy of given annotations with the help of logical solvers in the backend, a critical input that a user needs to supply manually are annotations at key points, like loop invariants and function contracts. A possible way to address this problem is to use learning techniques to find such candidate invariants, making use of counter-examples provided by the verification engine to previously conjectured invariants. In this talk we describe a decision-tree based approach to doing this, and highlight some of the challenges in adapting classical decision-tree learning algorithms to handle samples that may, in general, take the form of Horn clauses. This is joint work with P. Ezudheen (IISc), Pranav Garg (Amazon India), Daniel Neider (MPI, Kaiserslautern), and P. Madhusudan (UIUC). About the speaker: Deepak D'Souza received his PhD from Chennai Mathematical Institute in 2000. Since 2003 he has been at the Department of Computer Science and Automation of the Indian Institute of Science, Bangalore, where he is currently a Professor. His areas of interest include program verification, program analysis, and specification and analysis of real-time and hybrid systems.
|
