-------- Forwarded Message -------- Subject: [WI] Workshop on Advances in Separation Logics (ASL 2022 @ FLOC 2022) Date: Fri, 18 Mar 2022 12:42:44 +0100 (CET) From: RADU IOSIF radu.iosif@univ-grenoble-alpes.fr Reply-To: RADU IOSIF radu.iosif@univ-grenoble-alpes.fr To: pakhfn@mi.ras.ru, d.i.saveliev@gmail.com, aarati@cs.stanford.edu, aayesh@dmu.ac.uk, admin@lists.oasis-open.org, agents@cs.umbc.edu, ageron@math.unicaen.fr, akoslow@gc.cuny.edu, alama@stanford.edu, alessandro.facchini@unine.ch, a.lisitsa@csc.liv.ac.uk, amirouche.moktefi@gersulp.u-strasbg.fr, anderssn@itu.dk, antti.j.kuusisto@uta.fi, arbiser@dc.uba.ar, asci@twi.tudelft.nl, nza@Cs.Nott.AC.UK, baader@tcs.inf.tu-dresden.de, baelde@lsv.fr, basin@inf.ethz.ch, Beata.Konikowska@ipipan.waw.pl, behounek@cs.cas.cz, Bernhard.Heinemann@fernuni-hagen.de, birkedal@cs.au.dk, blutner@web.de, carniell@cle.unicamp.br, carsten@itu.dk, categories@mta.ca, ccal@math.ist.utl.pt, ccshan@post.harvard.edu, cherrierp@wanadoo.fr, Christiane.Ruffieux@chuv.ch, cintula@cs.cas.cz, ckemke@cs.umanitoba.ca, c.konyevits@bluewin.ch, clp@comp.nus.edu.sg, cmartinez@wesleyan.edu, colognet@ucy.ac.cy, comlab@comlab.ox.ac.uk, complog@cs.nmsu.edu, comprox@doc.ic.ac.uk, compulognet-parimp@clip.dia.fi.upm.es, compulognet-parimp@dia.fi.upm.es, concurrency@cwi.nl, conferences@computer.org, coniglio@cle.unicamp.br, corpora@hd.uib.no, cotton@ensae.fr, cristi@ifi.uio.no, css@cs.stanford.edu, czhou@indiana.edu, daml-all@daml.org, davism@cs.nyu.edu, dbailey@cse.ucsc.edu, dbitaly@list.dia.uniroma3.it, dbworld@cs.wisc.edu, amelie.david@lsv.fr, demri@lsv.fr, dov.gabbay@kcl.ac.uk, nivelle@ii.uni.wroc.pl, amina.doumane@lsv.ens-cachan.fr, Diderik.Batens@UGent.be, digicult-forum@digicult.info, dunn@indiana.edu, eestevez@us.es, elsnet-list@elsnet.org, elsnet-list@let.uu.nl, enrique.alonso@uam.es, epontell@cs.nmsu.edu, erdelyi-szabo.miklos@renyi.mta.hu, event@in.tu-clausthal.de, events_calendar@acm.org, fg-db@informatik.uni-rostock.de, finite-model-theory@lists.RWTH-Aachen.DE, finng@ruc.dk, fm-discussion@cs.man.ac.uk, franceschet@dimi.uniud.it, frza@itu.dk, fsoler@us.es, ftohme@criba.edu.ar, Galmiche@loria.fr, Olivier.Gasquet@irit.fr, gemm@usal.es, genechoquette@hotmail.com, gfeng@usc.edu, gilberto.pastorello@terra.com.br, Grant.Marler@cgu.edu, guillaume.feuillade@irit.fr, guray@asu.edu, gwa@lists.ut.ee, haf@fc.unesp.br, hehuac@nwpu.edu.cn, hellm001@umn.edu, hermann@inf.puc-rio.br, hkurokawa@gc.cuny.edu, hugomar@ime.usp.br, humanist@lists.Princeton.EDU, humanist@princeton.edu, ifmsig@cs.tcd.ie, ilpo.halonen@helsinki.fi, imperativlogik@hotmail.com, inanc.seylan@gmail.com, itala@cle.unicamp.br, Jacques.Riche@cs.kuleuven.ac.be, janciu@uni.lodz.pl, jansana@cerber.mat.ub.es, janusz.czelakowski@uni.opole.pl, jarmuzek@uni.torun.pl, jyb.logician@gmail.com, jmfont@ub.edu, johan@science.uva.nl, jonni.virtema@uta.fi, jpg@ruc.dk, jsgrygiel@poczta.onet.pl, juliana.bueno@cle.unicamp.br, jv@imm.dtu.dk, jwaldmajer@uni.opole.pl, kamps@science.uva.nl, kashima@is.titech.ac.jp, kgank@wp.pl, kgl@cs.aau.dk, kgs@logic.at, Krister.Segerberg@filosofi.uu.se, kr@kr.org, ksnelson@subjectivity.com, ladusaw@cats.ucsc.edu, lazic@dcs.warwick.ac.uk, dominique.larchey-wendling@loria.fr, ldostal@kfi.zcu.cz, lfcs-interest@dcs.ed.ac.uk, tadeusz.litak@gmail.com, logic@cs.stanford.edu, logic-list@helsinki.fi, logic@math.uni-bonn.de, logik@math.uni-freiburg.de, logik@math.uni-muenster.de, loom-forum@isi.edu, lozes@lsv.fr, lucia@ime.usp.br, luismenasche@gmail.com, luiz@inf.puc-rio.br, maietti@math.unipd.it, mailings@iwv.jku.at, majer@site.cas.cz, malerba@di.uniba.it, mara@usal.es, marco.volpe@univr.it, marie.duzi@vsb.cz, mario@cos.ufrj.br, martin.lange@uni-kassel.de, marx@science.uva.nl, math.logik@gmx.net, maxime.beauquier@itu.dk, mccolm@math.usf.edu, mgehrke@liafa.univ-paris-diderot.fr, mhuertass@uoc.edu, michael.groneberg@unifr.ch, miraglia@ime.usp.br, mizar-forum@mizar.uwb.edu.pl, mspinksau@yahoo.com.au, mullers77@hotmail.com, mvazquez@ull.es, nechitajlov@mail.ru, inemeti@gmail.com, nepomuce@us.es, nicolosi@dmi.unict.it, Nikolaos.Tzevelekos@comlab.ox.ac.uk, nordlingnet@uib.no, om-announce@openmath.org, omp@di.uminho.pt, ontology@buffalo.edu, ontoquery@ruc.dk, E.Orlowska@itl.waw.pl, paoli@unica.it, patrick.allo@vub.ac.be, P.Bruscoli@bath.ac.uk, pcobrer@alumni.unav.es, pjparikh@aol.com, polacik@us.edu.pl, pozzato@di.unito.it, prog-lang@diku.dk, proof-complexity@math.cas.cz, ProofTheory.List@Gmail.com, psh@informatik.uni-tuebingen.de, public-owl-dev@w3.org, public-rif-wg@w3.org, puml-list@cs.york.ac.uk, QWN05577@nifty.ne.jp, rahm@informatik.uni-leipzig.de, raja@tifr.res.in, rantonse@ifi.uio.no, Razvan.Diaconescu@imar.ro, regis.alenda@gmail.com, rendsvig@gmail.com, rineke@ai.rug.nl, risc@risc.cnrs.fr, rlewin@mat.puc.cl, rodin@ens.fr, rosati@dis.uniroma1.it, Ross.Brady@latrobe.edu.au, ruy@cin.ufpe.br, rz@linguist.jussieu.fr, saliyari@Indiana.edu, saltcat@bc4.so-net.ne.jp, sayadyans@yahoo.com, schmitz@lsv.ens-cachan.fr, sefus@usal.es, semantic-web@w3.org, sep@phil.ufl.edu, sf@tut.fi, sigsem@aclweb.org, skgottipati@hotmail.com, slr@st-and.ac.uk, srirams@cs.stanford.edu, steinhorn@vassar.edu, geoff@cs.miami.edu, stephan.kreutzer@tu-berlin.de, Renate.Schmidt@manchester.ac.uk, su.rogerson@arts.monash.edu.au, swbyun@star.ks.ac.kr, sw-ergo@gui-design.de, tarlecki@mimuw.edu.pl, tballiso@umich.edu, tb@imm.dtu.dk, tbro@itu.dk, theorem-provers@ai.mit.edu, theory-logic@cs.cmu.edu, timm.lampert@philo.unibe.ch, tinko@fmi.uni-sofia.bg, tojo@jaist.ac.jp, torben@ruc.dk, tstuder@iam.unibe.ch, ura-list@helsinki.fi, uws@uni.opole.pl, valeria.depaiva@gmail.com, vandervk@uqtr.ca, vegetal@cle.unicamp.br, veloso@cos.ufrj.br, vero0304@yahoo.com, veta_v@mail.ru, vincent@hum.ku.dk, vki-list@dfki.de, vladan@ualberta.ca, ward.blonde@ugent.be, webmaster@aisb.org.uk, weinsteinm@mail.montclair.edu, wi@aifb.uni-karlsruhe.de, wojtek.jamroga@uni.lu, wojtylak@ux2.math.us.edu.pl, wilke@ti.informatik.uni-kiel.de, wyw@gdut.edu.cn, xcaicedo@uniandes.edu.co, yye@umich.edu, zhitaohe@vip.sina.com, Natasha.Alechina@nottingham.ac.uk, carlos.areces@gmail.com, balbiani@irit.fr, lbekl@yandex.ru, tobo@dtu.dk, serena@ibisc.univ-evry.fr, david.fernandez@itam.mx, melvin.fitting@lehman.cuny.edu, michael.gelfond@ttu.edu, gabelaia@gmail.com, silvio.ghilardi@unimi.it, valentin.goranko@philosophy.su.se, Rajeev.Gore@anu.edu.au, Andreas.Herzig@irit.fr, R.Iemhoff@uu.nl, agi.kurucz@kcl.ac.uk, roman@logic.at, clu@uni-bremen.de, Mate.andras@btk.elte.hu, angelo.montanari@uniud.it, lsm@cs.indiana.edu, odintsov@math.nsc.ru, ono@jaist.ac.jp, mark.reynolds@uwa.edu.au, shapir@iitp.ru, shehtman@netscape.net, Heinrich.Wansing@rub.de, michael@dcs.bbk.ac.uk, daniel.mery@loria.fr, hans.van-ditmarsch@loria.fr, gbezhani@math.nmsu.edu, Rob.Goldblatt@msor.vuw.ac.nz, kapur@cs.unm.edu, wies@cs.nyu.edu, siddharth.krishna@nyu.edu, rseba@disi.unitn.it, petar.iliev@loria.fr, sangnier@liafa.univ-paris-diderot.fr, nicola.olivetti@univ-cezanne.fr, agata@logic.at, sattler@cs.man.ac.uk, cialdea@dia.uniroma3.it, arild@ifi.uio.no, u.hustadt@csc.liv.ac.uk, roy.dyckhoff@googlemail.com, wolter@liverpool.ac.uk, sofronie@mpi-sb.mpg.de, villemaire.roger@uqam.ca, markey@lsv.fr, dwb@lsv.fr, praveenm@cmi.ac.in, dfigueira@gmail.com, frederic.blanqui@inria.fr, kit.fine@nyu.edu, goubault@lsv.ens-cachan.fr, damiananizer@gmail.com, potapov@liverpool.ac.uk, gilles.dowek@inria.fr, shkatov@gmail.com, goeller@lsv.ens-cachan.fr, nguyen@mimuw.edu.pl, pierre.bourhis@univ-lille1.fr, anuj.dawar@cl.cam.ac.uk, CLDixon@liverpool.ac.uk, uwe@mpi-inf.mpg.de, Pascal.Fontaine@loria.fr, Stephan.Merz@loria.fr, fcsatari@gmail.com, bitai.tamas@gmail.com, gomorim@gmail.com, balazs.inotai@freemail.hu, markovich.reka@yahoo.com, molnar.h.attila@gmail.com, fcarreiro@gmail.com, turms@renyi.hu, mekis@ludens.elte.hu, markovich@phil.elte.hu, Peter.Baumgartner@nicta.com.au, beckert@kit.edu, chrisf@logic.at, ghilardi@dsi.unimi.it, Konev@liverpool.ac.uk, roberto.sebastiani@disi.unitn.it, petar.iliev@gmail.com, sara.negri@helsinki.fi, patrickb@ruc.dk, gabriella.pigozzi@dauphine.fr, Guillaume.Feuillade@irit.fr, Emiliano.Lorini@irit.fr, Joseph.Boudou@irit.fr, David.Fernandez@irit.fr, Sophie.Pinchinat@irisa.fr, francois.schwarzentruber@ens-rennes.fr, troquard@loa.istc.cnr.it, luigi.santocanale@lif.univ-mrs.fr, dwb@lsv.ens-cachan.fr, wuzl@ios.ac.cn, fmurlak@mimuw.edu.pl, cabalar@udc.es, laura.bozzelli@fi.upm.es, cesar.sanchez@imdea.org, nalon@unb.br, bsl@cs.nott.ac.uk, fervari@famaf.unc.edu.ar, hoffmann@famaf.unc.edu.ar, dirk.pattinson@anu.edu.au, shalle@acm.org, fernandorvelazquezq@gmail.com, sophia.knight@gmail.com, lasha.abzianidze@gmail.com, igor.sedlar@uniba.sk, guido@um.es, halpern@cs.cornell.edu, s.l.uckelman@durham.ac.uk, y.wang@pku.edu.cn, fanjie@pku.edu.cn, jve@cwi.nl, colcombe@liafa.univ-paris-diderot.fr, WiebevanderHoek@csc.liv.ac.uk, sobekal@hotmail.com, dirk@ua.pt, vincent.demange@loria.fr, delima@cril.fr, J.Brotherston@ucl.ac.uk, work@erickoskinen.com, nikos.gorogiannis@gmail.com, Lutz.Schroeder@cs.fau.de, a.visser@uu.nl, wconradie@uj.ac.za, graedel@logic.rwth-aachen.de, igw@labri.fr
Workshop on Advances in Separation Logics (ASL 2022), Haifa, Israel, July 31st 2022
https://asl-workshop.github.io/asl22/
The past two decades have witnessed important progress in static analysis and verification of code with low-level pointer and heap manipulations, mainly due to the development of Separation Logic (SL). SL is a resource logic, a dialect of the logic of Bunched Implications (BI) designed to describe models of the heap memory and the mutations that occur in the heap as the result of low-level pointer updates. The success of SL in program analysis is due to the support for local reasoning, namely the ability of describing only the resource(s) being modified, instead of the entire state of the system. This enables the design of compositional analyses that synthesize specifications of the behavior of small parts of the program before combining such local specifications into global verification conditions. Another interesting line of work consists in finding alternatives to the underlying semantic domain of SL, namely heaps with aggregative composition, in order to address other fields in computing, such as self-adapting distributed networks, blockchain and population protocols, social networks or biological systems.
We consider submissions on topics including:
* decision procedures for SL and other resource logics, * computational complexity of decision problems such as satisfiability, entailment and abduction for SL and other resource logics, * axiomatisations and proof systems for automated or interactive theorem proving for SL and other resource logics, * verification conditions for real-life interprocedural and concurrent programs, using SL and other resource logics, * 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.
ASL 2022 is a workshop affiliated to IJCAR 2022 at FLOC 2022.
Keynote Speakers
* Philippa Gardner, Imperial College London * Ralf Jung, MIT CSAIL
Important Dates
* Papers due: May 10, 2022 (AoE) * Authors notification: June 15, 2022 (AoE) * Workshop: July 31, 2022
Program Committee
Nadia Polikarpova (UCSD, San Diego, USA) James Brotherston (UCL, London, UK) Qinxiang Cao (Shanghai Jiaotong University) Dan Frumin (University of Groningen, The Netherlands) Lennart Beringer (Princeton University, USA) Arthur Charguéraud (INRIA Strasbourg, France) Radu Iosif (Verimag, CNRS, Univ. Grenoble Alpes, France) Le Quang Loc (UCL, London, UK) Alessio Mansutti (University of Oxford, UK) Christoph Matheja (DTU, Lyngby, Denmark) Daniel Méry (University of Loraine, France) Koji Nakazawa (Nagoya University, Japan) Nicolas Peltier (LIG, CNRS, Grenoble, France) Adam Rogalewicz (Brno University of Technology, Czech Republic) Mihaela Sighireanu (LMF, ENS Paris-Saclay, France) Florian Zuleger (Vienna University of Technology, Austria)
Organizing committee
Radu Iosif (Verimag, CNRS, Univ. Grenoble Alpes, France) Nikos Gorogiannis (Meta, London, UK) Robbert Krebbers (Radboud Univ. Nijmegen, The Netherlands) Mihaela Sighireanu (LMF, ENS Paris-Saclay, France) Makoto Tatsuta (NII, Tokyo, Japan) Thomas Noll (RWTH, Aachen, Germany)
-- Mailing-Liste: wi@lists.kit.edu Administrator: wi-request@lists.kit.edu Konfiguration: https://www.lists.kit.edu/wws/info/wi