Keynote speakers will be:

Sumit Gulwani, Microsoft Research, Redmond, WA, USA
Adenilso Simão, ICMC/USP, São Carlos, SP, Brazil

Title: Applications of Formal Methods to Data Wrangling and Education

Sumit Gulwani, Microsoft Research, Redmond, WA, USA

Abstract: Data is locked up in semi-structured formats such as spreadsheets, text/log files, webpages, pdf documents. Getting data out of these documents into structured formats that allow the data to be explored and analyzed is challenging. While data scientists spend 80% of their time cleaning data, programmatic solutions to data manipulation are beyond the expertise of 99% of end users who do not know programming. Programming by Examples (PBE) can make data wrangling a delightful experience for the masses. The first part of this talk will describe how formal methods can be used to address two key challenges in PBE: (a) efficient search algorithms to explore the huge state space of programs to find those that match the user-provided examples, and (b) effective ambiguity resolution techniques to deal with the inherent ambiguity in the examples. The second part of this talk will describe how formal methods can help automated two key tasks in Education, namely (a) problem generation and (b) feedback generation. I will illustrate this using recent research results that have been applied to various STEM subject domains including mathematics, programming, logic, and automata theory. These results advance the state-of-the-art in intelligent tutoring, and can play a significant role in enabling personalized and interactive education in both standard classrooms and MOOCs.

Short Bio: Sumit Gulwani is a principal researcher at Microsoft Research (in Redmond, USA), and an adjunct faculty in the Computer Science Department at IIT Kanpur (India). He has expertise in formal methods and automated program analysis and synthesis techniques. His recent research interests are in the cross-disciplinary areas of automating end-user programming and building intelligent tutoring systems. His programming-by-example work led to the Flash Fill feature of Microsoft Excel 2013 that is used by hundreds of millions of people. He was awarded the ACM SIGPLAN Robin Milner Young Researcher Award in 2014. He obtained his PhD in Computer Science from UC-Berkeley in 2005, and was awarded the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in Computer Science and Engineering from IIT Kanpur, and was awarded the President's Gold Medal.

Title: To test or not to test, that is formal question

Adenilso Simão, ICMC/USP, São Carlos, SP, Brazil

Abstract: The demand of highly dependable software has greatly motivated the research of two important areas of software engineering, namely, formal methods and software testing. Both areas have matured considerably in the last years, to the point of being mainstream approaches in the development of critical systems. However, despite some fruitful exchange of ideas between them, formal methods and software testing have advanced somehow isolated from each other. In this talk, we review the achievements related to the combination of formal methods and software testing. We will discuss, for instance, how testing can be formal and how formal methods can be aided by testing. The main goal of this talk is to identify opportunities to strengthen the exchange between these two exciting and important areas.

Short Bio: Adenilso Simao received the BS degree in computer science from the State University of Maringa (UEM), Brazil, in 1998, and the MS and PhD degrees in computer science from the University of Sao Paulo (USP), Brazil, in 2000 and 2004, respectively. Since 2004, he has been a professor of computer science at the Computer System Department of USP. From August 2008 to July 2010, he has been on a sabbatical leave at Centre de Recherche Informatique de Montreal (CRIM), Canada. He has received best paper awards in several important conferences. He has also received distinguishing teacher awards in many occasions. His research interests include software testing and formal methods.