Charla: Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis


Compartir
Charlista: 
Isil Dillig - University of Texas at Austin
Fecha: 
18 Diciembre, 2015 - 11:00
Sala: 
Auditorio Picarte, 3er piso Edificio Norte
Organización: 
Éric Tanter - PLEIAD
Bio: 

Isil Dillig is an Assistant Professor of Computer Science at the University of Texas at Austin. She is also a Sloan Fellow and a recipient of the NSF CAREER award. She obtained all her degrees (BS, MS, PhD) from Stanford University. Prior to joining UT Austin, Dr. Dillig worked as a researcher at Microsoft Research (2013-2014) and as an assistant professor of computer science at the College of William & Mary (2012-2013).

Abstract: Abductive inference is a form of backwards logical reasoning that infers likely hypotheses from a given conclusion. In other words, given an invalid implication of the form A => B, abduction asks the question "What formula C do we need to conjoin with the antecedent A so that (i) A & C => B is logically valid and (ii) C is consistent with A?" Abductive reasoning has found many applications in program verification and synthesis, particularly in modular program analysis, invariant generation, and automated inference of missing program expressions. This tutorial will give an overview of logical abduction and algorithms for performing abductive inference. We will also survey several use cases of abductive inference in the context of program analysis, verification, and synthesis.