Separation Logic Modulo Theories

Presented as part of the 2013 HCSS conference.

ABSTRACT:

The aim of this talk is to describe a number of recent developments on the integration of Separation Logic, a prominent logic for statically reasoning about the memory usage of computer programs, and Satisfiability Modulo Theories (SMT). By leveraging on the power of SMT solvers, our reasoning tools are able to simultaneously handle supported theory assertions between data and pointer variables—including e.g. integer and real arithmetic, bit-vectors and arrays—and the shape of the data structures referenced by those pointers. The talk will include motivating examples and encouraging experimental results obtained with Aster*ıx, an implementation of our entailment checking algorithm that relies on Z3 as the theory reasoning back-end. The work presented is a joint collaboration with Andrey Rybalchenko from the Technische Universität München.

BIO:

Juan Navarro earned a BSc in Mathematics from Universidad de las Américas Puebla in Mexico, before obtaining his PhD degree in Computer Science from The University of Manchester in the UK. For a couple of years he was a visiting researcher at the Max Planck Institute for Software Systems, and then for two years more at the Technische Universität München, where he furthered his research in program analysis and verification. He began his academic career in 2012 at Queen Mary, University of London, and is currently a lecturer at University College London, where he is also member of the Programming Principles, Logic and Verification research group.