[TYPES/announce] Second Workshop on Automated Deduction for Separation Logics

[Radu Iosif]

Second Workshop on Automated Deduction for Separation Logics, New Orleans, USA, January 20th 2020

https://popl20.sigplan.org/home/adsl-2020 <https://popl20.sigplan.org/home/adsl-2020>

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.

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 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020).

Invited speakers: 

* Robbert Krebbers (Delft University of Technology) : Relational reasoning using concurrent separation logic
* Josh Berdine (Facebook) : SLEdge: Bounded Model Checking in Separation Logic

Important dates (AoE):

Papers due: November 1st 
Author notification: December 15th
Workshop: January 20th

Program committee

Josh Berdine (Facebook)
James Brotherston (University College London)
Stephane Demri (LSV, CNRS, ENS Paris-Saclay)
Nikos Gorogiannis (Middlesex University London, Facebook)
Lukas Holik (Brno Univ. of Technology)
Radu Iosif (Verimag, CNRS, University of Grenoble Alpes)
Dominique Larchey-Wendling (CNRS, LORIA)
Quang Loc Le (Teeside University)
Alekandar Nanevski (IMDEA Software)
Peter O'Hearn (Facebook)
Nadia Polikarpova (University of California San Diego)
David Pym (University College London)
Mihaela Sighireanu (IRIF, CNRS, Universite Paris Diderot)
Thomas Wies (New York University)
Zhilin Wu (Chinese Academy of Sciences)
Florian Zuleger (Technical University of Vienna)

Organisation

Radu Iosif (VERIMAG, CNRS, University of Grenoble Alpes)
Nikos Gorogiannis (Middlesex University London, Facebook)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20191020/a447e71b/attachment-0001.html>