First Workshop on Automated Deduction for Separation Logics (ADSL)
In recent times, program verification, and particularly deductive program verification, has made significant progress. This progress is in part due to the incorporation of logical backends such as SMT solvers and other automated theorem-proving technologies. In parallel to these developments, the verification of heap manipulating programs, and static analyses in particular, has met with substantial successes, largely due to the development of Separation Logics.
Separation Logics allow local reasoning by means of built-in spatial atoms (empty heap, points-to) and spatial connectives (separating conjunction and implication, also known as the star and the magic wand). Combining this power with induction/recursion allows
- writing elegant and concise specifications for a large class of recursive data structures, and,
- capturing the semantics of programs with pointer updates by rather simple Hoare-style calculi.
Such expressivity comes with the inherent difficulty of automating these logics. As a consequence, some deductive program verifiers based on separation logic do not offer automation for handling arbitrary recursive predicates. Other verifiers support inductive reasoning but with various compromises, such as restricted support for the ground theories, or tractability issues.
The goal of this workshop is to bring together academic researchers and industrial practitioners focused on improving the state of the art of automated deduction methods for Separation Logics. We will consider technical submissions presenting work on the following topics (the list is not exclusive):
- the integration of Separation Logics with SMT,
- proof search and automata-based decision procedures for Separation Logics and sister logics such as Bunched Implication Logic;
- computational complexity of logical problems such as satisfiability, entailment and abduction;
- alternative semantics and computation models based on the notion of resource;
- application of separation and resource logics to different fields, such as sociology and biology.
The workshop is affiliated with the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018) and part of the Federated Logic Conference 2018 (FLOC 2018).
Invited speakers
- David Pym, University College London and The Alan Turing Institute, UK
- Viktor Vafeiadis, Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Programme
The programme of ADSL 2018 is now available.
Important dates
Papers due: April 20th 2018 (extended)
Author notification: May 15th 2018
Workshop: 13 July 2018
Program committee
| PC Member | Affiliation |
|---|---|
| Philippa Gardner | Imperial College London |
| Josh Berdine | |
| James Brotherston | University College London |
| Stéphane Demri | CNRS, LSV, ENS Paris-Saclay |
| Nikos Gorogiannis | Middlesex University London and Facebook |
| Christoph Haase | University of Oxford |
| Radu Iosif | VERIMAG, CNRS, University of Grenoble Alpes |
| Bart Jacobs | University of Leuven |
| Etienne Lozes | University of Nice |
| Daniel Méry | LORIA, Nancy |
| Peter O’Hearn | University College London, Facebook |
| Madhusudan Parthasarathy | University of Illinois |
| Nicolas Peltier | LIG, CNRS, University of Grenoble Alpes |
| Thomas Wies | Courant Institute, New York University |
SL-COMP
As part of this workshop, we intend to organize a second edition of the Separation Logic Competition (SL-COMP) for solvers targeting fragments of Separation Logics. The page for SL-COMP 2018 is now available.
| Tool and SL-COMP chair | ||
|---|---|---|
| Mihaela Sighireanu | LIAFA, University of Paris Diderot |
Organisation
| Radu Iosif | Nikos Gorogiannis | |
|---|---|---|
| Université Grenoble Alpes (France) | Middlesex University and Facebook (UK) |
The ADSL workshop is sponsored by
