Principles of Programming Seminar

Thursday, May 5, 2016 -
10:00am to 11:00am


8102 Gates & Hillman Centers


REUBEN MARTINS, Postdoctoral Researcher /REUBEN%20MARTINS

Event Website:

For More Information, Contact:

In recent years, Boolean Satisfiability (SAT) solvers have been successfully used in many practical applications. Given a propositional formula, the SAT problem consists in deciding if the formula is satisfiable or unsatisfiable. For unsatisfiable formulas, we are often interested in knowing what is the maximum number of clauses that can be simultaneously satisfied. Such problem is known as the Maximum Satisfiability (MaxSAT) problem, the optimization counterpart to SAT as a decision problem. Many real-world applications, such as software package upgrades, error localization in C code, and malware detection, can be encoded into MaxSAT and take advantage of the recent advances in MaxSAT solving. In this talk, I will present effective and novel MaxSAT algorithms that lead to an order of magnitude improvement for solving real-world problems. I will also survey applications of MaxSAT, focusing on Android malware detection. Specifically, I will explain how to automatically infer malware signatures using MaxSAT from very few samples of a malware family with an accuracy of over 90%. — Ruben Martins is a postdoctoral researcher at the University of Texas at Austin, USA. Prior to joining UT Austin, he was a postdoctoral researcher at the University of Oxford, UK, and he received his PhD with honors from the Technical University of Lisbon, Portugal in 2013. His research aims to improve constraint solvers and broaden their applicability in program analysis, synthesis, and security. Dr. Martins has developed several award winning solvers and has consistently improved the state-of-the-art in Maximum Satisfiability (MaxSAT)< solving. He is currently the main developer of Open-WBO: an open source MaxSAT solver that won several awards in the MaxSAT competitions. Faculty Host: Frank Pfenning