| Title | : | Leon and Orb - A System for Verifying Qualitative and Quantitative Properties of Functional Programs |
| Speaker | : | Ravi Kandhadai (EPFL, Switzerland) |
| Details | : | Fri, 28 Aug, 2015 3:00 PM @ BSB 361 |
| Abstract: | : | In this talk, I will give a brief overview of the Leon verification system (http://leon.epfl.ch), developed in our lab over the past few years, that can be used to verify deep correctness properties of purely functional programs involving recursive functions and data structures. Subsequently, I will describe an extension of Leon (Orb) that we developed for proving quantitative bounds on resources, such as the (sequential/parallel) execution time, stack space etc., consumed by a program. For example, Orb can prove that the function converting a propositional formula f into negation-normal form performs no more than 43 * size(f) − 17 operations, where size is the number of nodes in the syntax tree of the formula, and that the stack usage of the function is linear in the depth of the syntax tree. Orb can also verify nonlinear properties such as that the time taken by an insert procedure of a red-black tree is logarithmic in the height of the tree.
More references and publications related to Leon and Orb are available at: http://leon.epfl.ch/doc/references.html. Speaker bio: Ravi Kandhadai is a fourth year Ph.D student at EPFL, Switzerland and is advised by Prof. Viktor Kuncak. His research interests lie in the areas of programming languages, static program analysis and software verification. His current and past research has been mainly focused on static analysis of higher-order, object-oriented programs. He has developed softwares for analysing Java, C# and Scala programs. Before joining EPFL, Ravi was working as a Research Assistant in the Programming Languages and Tools group of Microsoft Research India. Ravi obtained his masters in Computer Science from Indian Institute of Science, Bangalore and bachelors in Computer Science from College of Engineering, Guindy. |
