From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id A55A75D5 for ; Fri, 10 Jan 2020 13:31:52 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.69,417,1571695200"; d="scan'208,217";a="430797778" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 10 Jan 2020 14:31:50 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 909237F3D1; Fri, 10 Jan 2020 14:31:50 +0100 (CET) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id A719A7F214 for ; Fri, 10 Jan 2020 14:31:13 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lpulina@uniss.it; spf=Pass smtp.mailfrom=lpulina@uniss.it; spf=None smtp.helo=postmaster@mail-wr1-f42.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AjBSIfx37Q+NnczGJsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?se0fLfad9pjvdHbS+e9qxAeQG9mCsLQe1bGd7/CocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmTSwbalsIBi3owjducYbjIh/Iast1xXFpWdFdf?= =?us-ascii?q?5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALM?= =?us-ascii?q?TRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljj?= =?us-ascii?q?oMOTwk/2HNksF+jLxVrg+iqRJxzYHbb52aOeFkca/BZ94XX3ZNU8hTWiFHH4iy?= =?us-ascii?q?b5EPD+0EPetAqYf9ukcBogGjDge2GePvzj5Ihnns0qYn1OkhFRnG3BEkH9IPtn?= =?us-ascii?q?Tbts74NLoUUeC016nI1i/Pb/JK2Trk7oXDbx4vofaJXb1qcMrRz1EiFxjdjlWK?= =?us-ascii?q?qIzlOTyV2foXs2SB8+VgUuevh3Ymqw5svDeg3N4gipPXiYIO1F/L7z95z5o1Jd?= =?us-ascii?q?28UkF0esSoEJxKtyGVMYZ9X8AsQ3lwtSok1rELvYS3cSsKxZg92RLTdeGLf5KH?= =?us-ascii?q?7x79TOqdPDN1iGx/dL6ihhu/81Ksx+zzW8WuzVpGsitIn9/RvX4XzRPT8NKISv?= =?us-ascii?q?5l80ehxzmP0wfT5/lBIU8ulKrbL4ctw7AqlpYOqEjDECD7lFvsgK+ZcUUk/eeo?= =?us-ascii?q?6+D5bbn8upCcMIp0hhn/MqQohMO/Hfw1PhYSU2Wf4+ix173u8VfnTLlUk/E6iK?= =?us-ascii?q?bUvI7CKcQevKG5AgtV0og56xa4CjeryNAYnWEaLFJBeRKHiZLmNkrTIPD+DPe/?= =?us-ascii?q?mE+snC1qx/DaJrHhGInCLmDfkLf9erZw81JTxxA2zdBb/p5UDrABIOnvWkLqr9?= =?us-ascii?q?zZDho5MxSuzOr9CdV90JkeWWOVDaODPqPSqwzA2uV6KOCJYMoRuS3hA/kj/f/n?= =?us-ascii?q?y3EjynEHeqz8+YYcYTiAA/BnJUzRNX70n9MAF24ioww/V/esiUHUAm0bXGq7Q6?= =?us-ascii?q?9pvmJzM4mhF4qWHtnw0ozE5z+yG9htXk4DCl2IFi21JYCNWvNJdzjLZ8E9yHoL?= =?us-ascii?q?Ur+uT4Jn3har5lejmuhXa9HM8yhdjqrNkd185undjxY3rGQmEsKcyHrLTn0mxz?= =?us-ascii?q?pUFQ9z57h2pAlG8nnGybJx2qQKCNpS/OgPUxtobZM=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ByAwB9exhehirdVdFlHQEBAQkBEQUFA?= =?us-ascii?q?YF7gSWBcFVchAmPGYV/lGiCCQNUCQEDAQoBAR8OAgEBhECBcxwHAQQ0EwIQAQE?= =?us-ascii?q?EAQEBAgECAwQBEwEBAQgLCwgphT4MgjsigxoLBh0BAQcfEhg6AQIHAjYBBQEvB?= =?us-ascii?q?gIBAR6DBAGCew+PW48OgQM9iyaBMh+CXwEBBYYFgTQJCQEIgSSMGRqBQT+BESe?= =?us-ascii?q?BSnSBcIFHggqDBIJejUYYkjCPLYFnWoMrgn+BEY5sBhuBBYFCd4cKhAuMF4RCk?= =?us-ascii?q?nKFIIFNiy0CBAIEBQIGDyOBRlmBITMaCDCDJwlHGA2STxgCHoM7hRSFQEAzAYE?= =?us-ascii?q?DkCwBAQ?= X-IPAS-Result: =?us-ascii?q?A0ByAwB9exhehirdVdFlHQEBAQkBEQUFAYF7gSWBcFVchAm?= =?us-ascii?q?PGYV/lGiCCQNUCQEDAQoBAR8OAgEBhECBcxwHAQQ0EwIQAQEEAQEBAgECAwQBE?= =?us-ascii?q?wEBAQgLCwgphT4MgjsigxoLBh0BAQcfEhg6AQIHAjYBBQEvBgIBAR6DBAGCew+?= =?us-ascii?q?PW48OgQM9iyaBMh+CXwEBBYYFgTQJCQEIgSSMGRqBQT+BESeBSnSBcIFHggqDB?= =?us-ascii?q?IJejUYYkjCPLYFnWoMrgn+BEY5sBhuBBYFCd4cKhAuMF4RCknKFIIFNiy0CBAI?= =?us-ascii?q?EBQIGDyOBRlmBITMaCDCDJwlHGA2STxgCHoM7hRSFQEAzAYEDkCwBAQ?= X-IronPort-AV: E=Sophos;i="5.69,417,1571695200"; d="scan'208,217";a="430797627" X-MGA-submission: =?us-ascii?q?MDFs6TvATkaNT5C9lwi//JflcpK2OTUmre6wp/?= =?us-ascii?q?Xfj4k+DY5xVtbTZzuqdEWebgfddLECwdFC9D1LFS6ArlTWlleCc9JHdP?= =?us-ascii?q?brUwjXTFHOWxpnyTvBYwlmmJYTuB0inXoe9cxLSTb0lkKLq2SIK2W599?= =?us-ascii?q?SVnKou4k6HCJElSXWpCBv1Cg=3D=3D?= Received: from mail-wr1-f42.google.com ([209.85.221.42]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 10 Jan 2020 14:31:12 +0100 Received: by mail-wr1-f42.google.com with SMTP id j42so1785711wrj.12 for ; Fri, 10 Jan 2020 05:31:12 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=uniss-it.20150623.gappssmtp.com; s=20150623; h=from:to:subject:message-id:date:user-agent:mime-version :content-language; bh=nno3ZInJbRlbWLcr8cQiPO2XCtAcmtOaUEmXR4RqKGM=; b=ShB6WnofkejtpHB1GlUaFaas0kpaikFjIDffW6XdT9Ca0cO55VI8B2d/h9yRUK4dpF 8hS40b7oOMCXXfFdqpDz8xhnkOZG9dDSo/RqxJklgKPcSOZt4+LsJnHawB+4DDV4ZADa OSGaQrqzJ9djqduHx6YOYLaA+96dmsMzghj2bvN7RAkq4doq85ZGoOULXtIA18rPU/eN lMtJVPSIs3gwS+cHAsA3b7yWNH+KV8/PFv8TCY9mNM8DTfa2qA0YQ3gKMmoMesXl/Zoq zDABja4d7vJ6IR+YzVaUiMFp2r2vyZr0Lhh9r+pqIJy9hfyr0Qb0RuR/TueidmeF0ols QXdg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:subject:message-id:date:user-agent :mime-version:content-language; bh=nno3ZInJbRlbWLcr8cQiPO2XCtAcmtOaUEmXR4RqKGM=; b=OYy64owzK/f9KtV3TVNAALvPtqMRq2G1hC1l4LdIFC0MFsppw4LrHF4xOqzG/sBGjO pPMLuCUaeMkZK+UO+ws4TjeMEex5QjGeZNABoWYGfN9zVH64gFK9O9Us03bFB11pYwvH JdYAU79lBePGx4ZRZJfRTzA2DM3iX0N3WRadg6v9WN485zQSIePd3ix+SgtipNldoGmL +oaPBS8cdNpKqiKMpwAMuGyg+zF4AmswAM/sJGG34RpI3GeYWwSi+3B0P1PN2ojSc9lZ lPiKgXA0pCrnA80T1LwVyI+GwzBRw0mbUtuNivkhdKF1ZZ9puBqhZGCHAuJsP/DY2CY0 FIig== X-Gm-Message-State: APjAAAXOrSQvtoXs2J3cowK9SUBEMzKyZv1zEfY2/FyjN4Dk3BDI684u weGd/WbsZs/lwhu5Mo0knh1af7MxN8fSVCziPdRUJVOyOuLLiFKoWRcucnFus+7c+Uj5nTff3Yd bZrXkuEIf5Q== X-Google-Smtp-Source: APXvYqwr+FKAorj8Kkx4P15VFFSJJSPiw4IBOjL+Vz21WUi1loKRDKPOGsUmOTouqptXVlDqAgnw8A== X-Received: by 2002:a5d:68c5:: with SMTP id p5mr3701235wrw.193.1578663071514; Fri, 10 Jan 2020 05:31:11 -0800 (PST) Received: from Lucas-MacBook-Pro.local ([192.167.64.106]) by smtp.gmail.com with ESMTPSA id q14sm2292608wmj.14.2020.01.10.05.31.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 10 Jan 2020 05:31:10 -0800 (PST) From: Luca Pulina To: caml-list@inria.fr Message-ID: <057ca49d-a0af-598b-336a-1117e91d4917@uniss.it> Date: Fri, 10 Jan 2020 14:31:09 +0100 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:60.0) Gecko/20100101 Thunderbird/60.9.1 MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="------------D0012AF059AFC28B29591B74" Content-Language: en-US X-Validation-by: lpulina@uniss.it Subject: [Caml-list] [CfP] SAT2020 - The 23rd International Conference on Theory and Applications of Satisfiability Testing Reply-To: Luca Pulina X-Loop: caml-list@inria.fr X-Sequence: 17945 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: This is a multi-part message in MIME format. --------------D0012AF059AFC28B29591B74 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable ******************** Call for Papers ******************** =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0The 23rd= International Conference on =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Theory and Applications of Satisfiability Te= sting =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0(SAT 2020= ) =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A05-9 July 2020, Alghero, Italy http://sat2020.idea-researchlab.org/ ********************************************************* The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the premier annual meeting for researchers focusing on the theory and applications of the propositional satisfiability problem, broadly construed. In addition to plain propositional satisfiability, it also includes Boolean optimization (such as MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning. *** Scope *** SAT 2020 welcomes scientific contributions addressing different aspects of the satisfiability problem, interpreted in a broad sense. Topics include, but are not restricted to: * Theoretical advances * Practical search algorithms * Knowledge compilation * Implementation-level details of SAT solving tools * Problem encodings and reformulations * Applications * Case studies based on rigorous experimentation *** Invited Speakers *** * Georg Gottlob, TU Wien, Austria * Aarti Gupta, Princeton University, US *** Out of Scope *** Papers claiming to resolve a major long-standing open theoretical question in Mathematics or Computer Science (such as those for which a Millennium Prize is offered), are outside the scope of the conference because there is insufficient time in the schedule to referee such papers; instead, such papers should be submitted to an appropriate technical journal. *** Paper Categories *** Submissions to SAT 2020 are solicited in three categories, describing original contributions. * Long papers (9 to 15 pages, excluding references) * Short papers (up to 8 pages, excluding references) * Tool papers (up to 6 pages, excluding references) Long and short papers should contain original research, with sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data and implementations available with their submission. Submissions on applications and cases studies are especially welcome. Such papers should describe details, weaknesses and strengths of the considered approaches in sufficient depth, but they are not expected to introduce novel solving approaches. Tool papers must obey to specific content criteria. A tool paper should describe the implemented tool and its novel features. Here =E2=80=9Ctools=E2=80=9D are interpreted in a broad sense, including descriptions of implemented solvers, preprocessors, etc. as well as systems that exploit SAT solvers or their extensions for use in interesting problem domains. A demonstration is expected to accompany a tool presentation. Papers describing tools that have already been presented previously are expected to contain significant and clear enhancements to the tool. Long and short papers will be evaluated with the same quality standards, and are expected to contain a similar contribution per page ratio. *** Submissions *** Submissions should not be under review elsewhere nor be submitted=20 elsewhere while under review for SAT 2020, and should not consist of=20 previously published material. Submissions not consistent with the above guidelines may be returned=20 without review. All papers submissions are done exclusively via EasyChair in Springer=E2=80= =99s=20 LaTeX llncs2e style. One author of each accepted paper is expected to present it at the=20 conference. Further details can be found at the website of SAT 2020: http://sat2020.idea-researchlab.org/ *** Proceedings *** The proceedings will be published by Springer in the series Lecture=20 Notes in Computer Science, seewww.springer.com/lncs=20 . *** Important Dates *** Workshops=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 July 5, 20= 20 Conference =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 July 6-9, 2020 Abstract submission=C2=A0 =C2=A0 =C2=A0 February 15, 2020 Paper submission =C2=A0 =C2=A0 =C2=A0 =C2=A0 February 22, 2020 Author response period =C2=A0 March 29 =E2=80=93 April 2, 2020 Author notification=C2=A0 =C2=A0 =C2=A0 April 18, 2020 Camera-ready =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 May 3, 2020 *** Organization *** Program Chairs * Luca Pulina, University of Sassari * Martina Seidl, Johannes Kepler University Linz Workshop Chair * Florian Lonsing, Stanford University Publicity Chair * Laura Pandolfo, University of Sassari Program Committee * Fahiem Bacchus, University of Toronto * Olaf Beyersdorff, Friedrich Schiller University Jena * Armin Biere, Johannes Kepler University Linz * Nikolaj Bjorner, Microsoft * Maria Luisa Bonet, Universitat Polit=C3=A8cnica de Catalunya * Sam Buss, University of California San Diego * Florent Capelli, Universit=C3=A9 de Lille * Pascal Fontaine, Universit=C3=A9 de Li=C3=A8ge, Belgium * Marijn Heule, Carnegie Mellon University * Alexey Ignatiev, Universidade de Lisboa * Mikolas Janota, University of Lisbon * Matti J=C3=A4rvisalo, University of Helsinki * Oliver Kullmann, Swansea University * Jie-Hong Roland Jiang, National Taiwan University * Jan Johannsen, Ludwig Maximilian University of Munich * Benjamin Kiesl, CISPA Helmholtz Center for Information Security * Daniel Le Berre, Universit=C3=A9 d=E2=80=99Artois * Florian Lonsing, Stanford University * Ines Lynce, Universidade de Lisboa * Vasco Manquinho, Universidade de Lisboa, Portugal * Felip Many=C3=A0, IIIA-CSIC * Joao Marques-Silva, University of Toulouse * Ruben Martins, Carnegie Mellon University * Kuldeep S. Meel, National University of Singapore * Alexander Nadel, Intel * Aina Niemetz, Stanford University * Jakob Nordstrom, University of Copenhagen * Markus N. Rabe, Google * Roberto Sebastiani, University of Trento * Natasha Sharygina, Universit=C3=A0 della Svizzera italiana * Laurent Simon, Bordeaux Institute of Technology * Friedrich Slivovsky, Vienna University of Technology * Stefan Szeider, Vienna University of Technology * Ralf Wimmer, Concept Engineering GmbH & Albert-Ludwigs-Universit=C3=A4t= =20 Freiburg * Christoph M. Wintersteiger, Microsoft *** Contact *** For any questions, please contact sat2020@easychair.org --=20 -- *Dona il=C2=A0 5x1000* all'Universit=C3=A0 degli Studi di Sassaricodice fis= cale:=20 00196350904 --------------D0012AF059AFC28B29591B74 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

******************** Call for Papers ********************


=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0The 2= 3rd International Conference on=C2=A0

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Theory and Applications of Satisfiability= Testing

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0(SAT 2= 020)


=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A05-9 July 2020, Alghero, Italy


=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0http://sat2= 020.idea-researchlab.org/


*********************************************************


The International Conference on Theory and Applications

of Satisfiability Testing (SAT) is the premier annual

meeting for researchers focusing on the theory and

applications of the propositional satisfiability problem,

broadly construed. In addition to plain propositional

satisfiability, it also includes Boolean optimization

(such as MaxSAT and Pseudo-Boolean (PB) constraints),

Quantified Boolean Formulas (QBF), Satisfiability Modulo

Theories (SMT), and Constraint Programming (CP) for

problems with clear connections to Boolean-level reasoning.



*** Scope ***


SAT 2020 welcomes scientific contributions addressing=C2=A0

different aspects of the satisfiability problem, interpreted=C2=A0

in a broad sense. Topics include, but are not restricted to:=C2=A0


* Theoretical advances

* Practical search algorithms

* Knowledge compilation

* Implementation-level details of SAT solving tools

* Problem encodings and reformulations

* Applications=C2=A0

* Case studies based on rigorous experimentation


*** Invited Speakers ***

* Georg Gottlob, TU Wien, Austria

* Aarti Gupta, = Princeton= University, US



*** Out of Scope ***=C2=A0


Papers claiming to resolve a major long-standing open=C2=A0

theoretical question in Mathematics or Computer Science

(such as those for which a Millennium Prize is offered),

are outside the scope of the conference because there is

insufficient time in the schedule to referee such papers;

instead, such papers should be submitted to an appropriate

technical journal.



*** Paper Categories ***


Submissions to SAT 2020 are solicited in three categories,

describing original contributions.


* Long papers (9 to 15 pages, excluding references)

* Short papers (up to 8 pages, excluding references)

* Tool papers (up to 6 pages, excluding references)


Long and short papers should contain original research, with

sufficient detail to assess the merits and relevance of the

contribution. For papers reporting experimental results, authors=

are strongly encouraged to make their data and implementations

available with their submission.


Submissions on applications and cases studies are especially=C2=A0

welcome. Such papers should describe details, weaknesses

and strengths of the considered approaches in sufficient depth,=C2=A0

but they are not expected to introduce novel solving approaches.=C2=A0<= /span>


Tool papers must obey to specific content criteria. A tool=C2=A0=

paper should describe the implemented tool and its novel=C2=A0

features. Here =E2=80=9Ctools=E2=80=9D are interpreted in a broad sense= ,=C2=A0

including descriptions of implemented solvers, preprocessors,=C2=A0

etc. as well as systems that exploit SAT solvers or their=C2=A0<= /p>

extensions for use in interesting problem domains.=C2=A0


A demonstration is expected to accompany a tool presentation.=C2=A0

Papers describing tools that have already been presented=C2=A0

previously are expected to contain significant and clear

enhancements to the tool.


Long and short papers will be evaluated with the same quality

standards, and are expected to contain a similar contribution

per page ratio.




*** Submissions ***


Submissions should not be under review elsewhere nor be submitted elsew= here while under review for SAT 2020, and should not consist of previously = published material.


Submissions not consistent with the above guidelines may be returned wi= thout review.


All papers submissions are done exclusively via EasyChair in Springer= =E2=80=99s LaTeX llncs2e style.


One author of each accepted paper is expected to present it at the conf= erence.


Further details can be found at the website of SAT 2020:=C2=A0

http://sat2020.idea-researchlab.org/



*** Proceedings ***


The proceedings will be published by Springer in the series Lecture Not= es in Computer Science, see www.sprin= ger.com/lncs.=C2=A0



*** Important Dates ***


Workshops=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 July 5= , 2020

Conference =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 July 6-9, 2= 020


Abstract submission=C2=A0 =C2=A0 =C2=A0 February 15, 2020

Paper submission =C2=A0 =C2=A0 =C2=A0 =C2=A0 February 22, 2020

Author response period =C2=A0 March 29 =E2=80=93 April 2, 2020

Author notification=C2=A0 =C2=A0 =C2=A0 April 18, 2020

Camera-ready =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 May 3, 2020



*** Organization ***



Program Chairs


* Luca Pulina, University of Sassari

* Martina Seidl, Johannes Kepler University Linz



Workshop Chair


* Florian Lonsing, Stanford University



Publicity Chair


* Laura Pandolfo, University of Sassari



Program Committee


* Fahiem Bacchus, University of Toronto

* Olaf Beyersdorff, Friedrich Schiller University Jena

* Armin Biere, Johannes Kepler University Linz

* Nikolaj Bjorner, Microsoft

* Maria Luisa Bonet, Universitat Polit=C3=A8cnica de Catalunya

* Sam Buss, University of California San Diego

* Florent Capelli, Universit=C3=A9 de Lille

* Pascal Fontaine, Universit=C3=A9 de Li=C3=A8ge, Belgium

* Marijn Heule, Carnegie Mellon University

* Alexey Ignatiev, Universidade de Lisboa

* Mikolas Janota, University of Lisbon

* Matti J=C3=A4rvisalo, University of Helsinki

* Oliver Kullmann, Swansea University

* Jie-Hong Roland Jiang, National Taiwan University

* Jan Johannsen, Ludwig Maximilian University of Munich

* Benjamin Kiesl, CISPA Helmholtz Center for Information Security

* Daniel Le Berre, Universit=C3=A9 d=E2=80=99Artois

* Florian Lonsing, Stanford University

* Ines Lynce, Universidade de Lisboa

* Vasco Manquinho, Universidade de Lisboa, Portugal

* Felip Many=C3=A0, IIIA-CSIC

* Joao Marques-Silva, University of Toulouse

* Ruben Martins, Carnegie Mellon University

* Kuldeep S. Meel, National University of Singapore

* Alexander Nadel, Intel

* Aina Niemetz, Stanford University

* Jakob Nordstrom, University of Copenhagen

* Markus N. Rabe, Google

* Roberto Sebastiani, University of Trento

* Natasha Sharygina, Universit=C3=A0 della Svizzera italiana

* Laurent Simon, Bordeaux Institute of Technology

* Friedrich Slivovsky, Vienna University of Technology

* Stefan Szeider, Vienna University of Technology

* Ralf Wimmer, Concept Engineering GmbH & Albert-Ludwigs-Universit= =C3=A4t Freiburg

* Christoph M. Wintersteiger, Microsoft



*** Contact ***=C2=A0


For any questions, please contact sat2020@easychair.org



--
Dona il=C2=A0 5x1000 all'Universit=C3=A0 degli Studi di= Sassari
codice fiscale: 001963509= 04
--------------D0012AF059AFC28B29591B74--