Write a Blog >>

In recent times, the verification of heap-manipulating programs, and static analyses in particular, has seen substantial success, largely due to the development of ‘Separation Logics’ (SLs). SLs provide embedded support for ‘local reasoning’: reasoning about the resource(s) being modified, instead of the state of the entire system. This form of reasoning is enabled by new syntax (dedicated atomic proposition and separating connectives) and corresponding semantics. Such expressivity comes with the inherent difficulty of automating these logics. Combining this power with induction/recursion allows to concisely specify a large class of recursive data structures and programs, but further increases the computational burden.

This has led to a fruitful search for restrictions of SLs which guarantee tractabilty. At the same time, this progress hints at possible generalisations, which would benefit the field significantly through SMT-like standardisation of tools and theories.

This workshop aims at bringing together academic researchers and industrial practitioners focused on improving the state of the art of automated deduction methods for SLs. We will consider technical submissions on topics which include :

  • the integration of SLs with SMT,

  • decision procedures,

  • computational complexity of 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.

Invited speakers

  • Robbert Krebbers (Delft University of Technology) : Relational reasoning using concurrent separation logic

  • Josh Berdine (Facebook) : SLEdge: Bounded Model Checking in Separation Logic

Mon 20 Jan

adsl-2020-papers
09:00 - 10:00: ADSL 2020 - Morning Keynote at Conde
adsl-2020-papers09:00 - 10:00
Talk
Robbert KrebbersDelft University of Technology
Media Attached File Attached
POPL-2020-catering
10:00 - 10:30: Catering - Monday Morning Break at Break
adsl-2020-papers
10:30 - 12:30: ADSL 2020 - Research Papers at Conde
adsl-2020-papers10:30 - 11:00
Research paper
File Attached
adsl-2020-papers11:00 - 11:30
Research paper
Denis MerigouxINRIA, Aymeric FromherzCarnegie Mellon University
File Attached
adsl-2020-papers11:30 - 12:00
Research paper
File Attached
adsl-2020-papers12:00 - 12:30
Research paper
Mnacho Echenim, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Nicolas Peltier
Pre-print File Attached
POPL-2020-catering
12:30 - 14:00: Catering - Monday Lunch at Lunch Room
POPL-2020-catering12:30 - 14:00
Lunch
adsl-2020-papers
14:00 - 15:05: ADSL 2020 - Afternoon Keynote at Conde
adsl-2020-papers14:00 - 15:05
Talk
Josh BerdineFacebook
File Attached
POPL-2020-catering
15:05 - 15:35: Catering - Monday Afternoon Break at Break
adsl-2020-papers
15:35 - 17:45: ADSL 2020 - Closing Session at Conde
adsl-2020-papers15:35 - 16:40
Talk
Nadia PolikarpovaUniversity of California, San Diego
adsl-2020-papers16:40 - 17:45
Talk
Thomas WiesNew York University

Call for Papers

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 resource logics such as Separation Logic and other variants of Bunched Implications. We will consider technical submissions presenting work on the following topics (the list is not exclusive):

  • the integration with SMT,
  • proof search and automata-based decision procedures,
  • 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.

Because ADSL does not publish proceedings, we do not impose a submission format. Indicatively, a maximum of 20 pages in LNCS format is advisable.