Scalable Program Analysis Techniques using Max-SMT
We are very pleased to invite you to the next Informatics Department Seminar given by Albert Rubio from the Universitat Politècnica de Catalunya.
Main content
Abstract
Program analyis is a formal method in which properties of computer programs are proved mathematically. As such it complements testing of programs, which cannot guarantee the absence of errors. The foundations of program analysis have been laid by Turing, Floyd, Dijkstra and Hoare in the 1950s and 60s. The method was long considered impracticable for real-life programs, but this has changed in recent years. Breakthroughs in SAT-solving have paved the way for (largely) automatic program analysis. In this talk we will provide an overview of the Max-SMT solving techniques and its application to compositional program analysis. These techniques have successfully been implemented in the VeryMax tool which currently can check safety, reachability and termination properties of C++ code.
Short biography
Albert Rubio is Full Professor at the Technical University of Catalonia - BarcelonaTech, Spain. He started his research on automated deduction and (higher-order) rewriting. He has also worked in the development of SMT solvers within the Barcelogic team and recently he has started a new line of research on the application of Max-SMT solvers in program analysis. Albert is Chair of the Steering Committee of the International Termination Competition, has been invited speaker at RTA and LOPSTR, and has been PC member in many international conferences (LICS, CADE, IJCAR, FOSSACS, CSL, LPAR, RTA, etc.).