IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2010 > Abductive, Deductive and Inductive Reasoning about Resources
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Peter O'Hearn

martes 30 de noviembre de 2010

3:00pm Amphitheatre H-1002

Peter O'Hearn, Profesor, Queen Mary, London University

Abductive, Deductive and Inductive Reasoning about Resources


I describe an automated reasoning method which approaches programs in a way inspired by the way that a scientist approaches the natural world. The method uses iterated Abductive, Inductive and Deductive inference. It allows us to synthesize a pre/- post spec for a program procedure, without requiring any information about the procedure’s calling context. The method can be used to obtain partial specifications for portions of large code bases in the millions of lines of code. This talk presents a survey and further development of work with Cristiano Calcagno, Dino Distefano and Hongseok Yang, which aims to leverage ideas from Separation Logic in program analysis. Among other things, the method attempts to automate the discovery of assertions describing footprints (the resources that a program component accesses), in a bid to obtain modular analyses.