ADSL2018: First Workshop on Automated Deduction for Separation Logics Oxford, UK, July 13, 2018 |
Conference website | http://adsl.univ-grenoble-alpes.fr |
Submission link | https://easychair.org/conferences/?conf=adsl2018 |
Conference program | https://easychair.org/smart-program/FLoC2018/ |
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.
Submission Guidelines
All papers must be original and not simultaneously submitted to another journal or conference. The following paper categories are welcome:
- Regular papers describing e.g. novel decision procedures, complexity results or applications for Separation Logic and related logics
- Tool papers describing implementations of systems for e.g. theorem proving, satisfiability modulo theories or program analysis
Regular papers should have at most 20 pages written in LNCS format, not counting references and appendices. Tool papers are limited to 10 pages in LNCS format, not counting references.
List of Topics
- 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.
Committees
Program Committee
|
Organizing committee
- Radu Iosif (VERIMAG/CNRS/Université de Grenoble Alpes)
- Nikos Gorogiannis (Midlessex University London and Facebook)
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
Publication
ADSL2018 proceedings will be published in a special issue of Electronic Notes in Theoretical Computer Science.
Venue
The conference is part of the Federated Logic Conference (FLOC 2018) and will be held in Oxford, UK.
Contact
All questions about submissions should be emailed to Radu Iosif (radu.iosif@univ-grenoble-alpes.fr) and Nikos Gorogiannis (nikos.gorogiannis@gmail.com)
Sponsors
Facebook, Verimag