We have two fully funded PhD scholarships for UK applicants in
the Security and Trust of Advanced Systems Group [1] (Prof. Achim
Brucker [2] and Dr. Diego Marmsoler [3]) at the Department of Computer
Science of the University of Exeter, UK [4].
We are looking for enthusiastic and outstanding Computer Science or
Mathematics students with a strong background in at least one of the
following topics:
* safety or security of (software) systems,
* formal modelling or formal reasoning/verification,
* program analysis or program verification,
* language-based security,
* semantics of programming languages,
* theorem proving, model checking,
* cryptographic protocols,
* distributed systems (e.g., blockchain),
* software security,
* cyber-physical systems,
* specification-based testing, and
* design and implementation of security architectures.
The positions offer the flexibility to define the PhD topic
jointly between the successful candidate and the supervisors.
Interested candidates should contact the potential supervisor
Prof. Achim Brucker (a.brucker(a)exeter.ac.uk) or Dr. Diego Marmsoler
(d.marmsoler(a)exeter.ac.uk) to discuss their application.
For more details, please consult the official advertisements:
* Compositional Verification of Smart Contracts in Isabelle:
https://www.exeter.ac.uk/study/funding/award/?id=4326
* Formal Verification for Safety- or Security-Critical Systems:
https://www.exeter.ac.uk/study/funding/award/?id=4328
The closing date for applications is midnight on the 29th April 2022.
Best,
Achim and Diego
[1] http://emps.exeter.ac.uk/computer-science/research/cyber-security/
[2] https://www.brucker.ch/
[3] https://marmsoler.com/
[4] http://emps.exeter.ac.uk/computer-science/
--
Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter
https://www.brucker.ch | https://logicalhacking.com/blog
@adbrucker | @logicalhacking
CONCUR 2022: last call for papers
==============================
September 12-16, 2022 at the University of Warsaw, Poland
Website: https://concur2022.mimuw.edu.pl/
The purpose of CONCUR 2022, the 33rd International Conference on Concurrency Theory, is to bring together researchers, developers, and students in order to advance the theory of concurrency, and promote its applications.
IMPORTANT NOTE CONCERNING THE COVID-19 PANDEMIC
CONCUR 2022 is planned as a physical, in-person event, with certain support for remote presence, both for speakers and for other participants who are unable or unwilling to come. Depending on the pandemic situation, we may have to make a decision whether to cancel the physical component of the event or not. This should be definitely decided by the end of June 2022.
INVITED SPEAKERS
Wojciech Czerwiński, University of Warsaw, Poland
Philippa Gardner, Imperial College London, UK
Rupak Majumdar, Max Planck Institute for Software Systems, Germany
Sergio Rajsbaum, Universidad Nacional Autonoma de Mexico, Mexico
CO-LOCATED CONFERENCES
19th International Conference on Quantitative Evaluation of SysTems (QEST 2022)
20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022)
27th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2022)
SATELLITE WORKSHOPS
Combined 29th Workshop on Expressiveness in Concurrency / 19th Workshop on Structural Operational Semantics (EXPRESS/SOS 2022)
11th IFIP WG 1.8 Workshop on Trends in Concurrency Theory (TRENDS 2022)
8th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR 2022)
10th Young Researchers Workshop on Concurrency Theory (YR-CONCUR 2022)
IMPORTANT DATES (all dates are AoE)
Abstract Submission: April 18, 2022
Paper Submission: April 25, 2022
Author Response: June 6-8, 2022
Notification: June 25, 2022
Camera Ready: July 9, 2022
Conference(s): September 13-16, 2022
Workshops: September 12, 2022
PAPER SUBMISSION
CONCUR 2022 solicits high quality papers reporting research results and/or experience related to the topics mentioned below. All papers must be original, unpublished, and not submitted for publication elsewhere.
Each paper will undergo a thorough review process. The paper may be supplemented with a clearly marked appendix, which will be reviewed at the discretion of the program committee.
The CONCUR 2022 proceedings will be published by LIPIcs.
Papers must be submitted electronically as PDF files via EasyChair:
https://easychair.org/conferences?conf=concur2022
Papers must not exceed 14 pages (excluding references and clearly marked appendices) using the LIPIcs style.
TOPICS
Submissions are solicited in semantics, logics, verification and analysis of concurrent systems. The principal topics include (but are not limited to):
* Basic models of concurrency such as abstract machines, domain-theoretic models, game-theoretic models, process algebras, graph transformation systems, Petri nets, hybrid systems, mobile and collaborative systems, probabilistic systems, real-time systems, biology-inspired systems, and synchronous systems;
* Logics for concurrency such as modal logics, probabilistic and stochastic logics, temporal logics, and resource logics;
* Verification and analysis techniques for concurrent systems such as abstract interpretation, atomicity checking, model checking, race detection, pre-order and equivalence checking, run-time verification, state-space exploration, static analysis, synthesis, testing, theorem proving, type systems, and security analysis;
* Distributed algorithms and data structures: design, analysis, complexity, correctness, fault tolerance, reliability, availability, consistency, self-organization, self-stabilization, protocols;
* Theoretical foundations of architectures, execution environments, and software development for concurrent systems such as geo-replicated systems, communication networks, multiprocessor and multi-core architectures, shared and transactional memory, resource management and awareness, compilers and tools for concurrent programming, programming models such as component-based, object- and service-oriented.
AWARDS
In 2022, CONCUR Test-of-Time and best paper awards will be given for the third time. The winners will be announced at the conference.
ORGANIZATION COMMITTEE
Lorenzo Clemente (workshop chair)
Piotrek Hofman
Bartek Klin
Sławek Lasota
Radek Piórkowski (webmaster)
PROGRAM COMMITTEE
C. Aiswarya, Chennai Mathematical Institute, India
S. Akshay, IIT Bombay, India
Shaull Almagor, Technion, Israel
Nathalie Bertrand, INRIA, France
Ilaria Castellani, INRIA, France
Constantin Enea, IRIF, Université de Paris, France
Bernd Finkbeiner, CISPA Helmholtz Center for Information Security, Germany
Blaise Genest, CNRS, France
Rob van Glabbeek, CSIRO, Sydney, Australia
Daniele Gorla, University of Rome La Sapienza, Italy
Jean Goubault-Larrecq, ENS Paris-Saclay, France
Ichiro Hasuo, National Institute of Informatics, Japan
Marcin Jurdzinski, The University of Warwick, UK
Stefan Kiefer, University of Oxford, UK
Bartek Klin, University of Oxford, UK (co-chair)
Barbara König, University of Duisburg-Essen, Germany
Sławomir Lasota, University of Warsaw, Poland (co-chair)
Martin Leucker, University of Lübeck, Germany
Bas Luttik, Eindhoven University of Technology, The Netherlands
P. Madhusudan, University of Illinois at Urbana-Champaign, US
Hernan Melgratti, Universidad de Buenos Aires, Argentina
Anca Muscholl, Bordeaux University, France (co-chair)
Jan Otop, University of Wrocław, Poland
Joel Ouaknine, Max Planck Institute for Software Systems, Germany
Jean-François Raskin, Université libre de Bruxelles, Belgium
Grigore Rosu, University of Illinois at Urbana-Champaign, US
Jurriaan Rot, Radboud University, The Netherlands
Davide Sangiorgi, University of Bologna, Italy
Alexandra Silva, University College London, UK and Cornell University, US
Paweł Sobociński, Tallinn University of Technology, Estonia
Ana Sokolova, University of Salzburg, Austria
Alwen Tiu, The Australian National University, Australia
Frits Vaandrager, Radboud University, The Netherlands
Nobuko Yoshida, Imperial College London, UK
Lijun Zhang, Chinese Academy of Sciences, China
STEERING COMMITTEE
Javier Esparza, TU München, Germany (chair)
Pedro D’Argenio, National University of Cordoba, Argentina
Wan Fokkink, Vrije Universiteit Amsterdam, The Netherlands
Joost-Pieter Katoen, RWTH, Germany
Catuscia Palamidessi, INRIA and Ecole Polytechnique, France
Davide Sangiorgi, University of Bologna, Italy
Jiri Srba, Aalborg University, Denmark
EATCS-IPEC Nerode Prize - Call for Nominations
Deadline: 15 May, 2022
The EATCS-IPEC Nerode Prize for outstanding papers in the area of
multivariate algorithmics, is presented annually with the presentation
taking place at IPEC (International Symposium on Parameterized and Exact
Computation). IPEC 2022 is due to take place as part of ALGO 2022 on 5-9
September in Potsdam, Germany. The Prize is named in honor of Anil
Nerode in recognition of his major contributions to mathematical logic,
theory of automata, computability and complexity theory.
Award Committee
The winning paper(s) will be selected by the EATCS-IPEC Nerode Prize
Award Committee. This year's committee consists of the following people.
Anuj Dawar, chair (University of Cambridge, anuj.dawar(a)cl.cam.ac.uk)
Fedor Fomin (University of Bergen, fedor.fomin(a)uib.no)
Thore Husfeldt (IT University of Copenhagen, thore(a)itu.dk)
Deadline for Nominations: 15 May, 2022.
Decision: 1 July, 2022.
The Award Committee is solely responsible for the selection of the
winner of the award which may be shared by more than one paper or series
of papers. The Award Committee reserves the right to declare no winner
at all.
Eligibility
Any research paper or series of research papers by a single author or by
a team of authors published in a recognized refereed journal. The
research work nominated for the award should be in the area of
multivariate algorithms and complexity meant in a broad sense, and
encompasses, but is not restricted to those areas covered by IPEC. The
Award Committee has the ultimate authority to decide on the eligibility
of a nomination. Papers authored by a member of the Award Committee are
not eligible for nomination.
Note that the past restrictions that require a certain number of years
before/after the publication of the nominated papers have been removed.
Nominations
Nominations may be made by any member of the scientific community
including the members of the Award Committee. A nomination should
contain a brief summary of the technical content of each nominated paper
and a brief explanation of its significance. Nominations are done by an
email to the Award Committee Chair with copies to the members of the
committee. The Subject line of the nomination E-mail should contain the
group of words "Nerode Prize Nomination".
[ Apologies for cross posting ]
Runtime Verification 2022 CALL FOR PAPERS
[ https://rv22.gitlab.io/ | https://rv22.gitlab.io ]
We are pleased to invite you to submit papers for the 22nd International Conference on Runtime Verification (RV'22), which will take place as part of the Computational Logic Autumn Summit CLAS 2022 ( [ http://viam.science.tsu.ge/clas2022/ | http://viam.science.tsu.ge/clas2022/ ] ) in Tbilisi, Georgia, from September 28-30, 2022.
### Dates ###
Paper submission: Thursday, 5 May 2022
Notification: Wednesday, 22 June 2022
Camera-ready: Sunday, 24 July 2022
Conference: 28-30 September 2022
Deadlines expire at 23:59 anywhere on earth on the dates displayed above.
### Conference Objectives and Scope ###
Runtime verification is concerned with the monitoring and analysis of the runtime behaviour of software and hardware systems. Runtime verification techniques are crucial for system correctness, reliability, and robustness; they provide an additional level of rigor and effectiveness compared to conventional testing and are generally more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair.
The topics of the conference include, but are not limited to:
- specification languages for monitoring
- monitor construction techniques
- program instrumentation
- logging, recording, and replay
- combination of static and dynamic analysis
- specification mining and machine learning over runtime traces
- monitoring techniques for concurrent and distributed systems
- runtime checking of privacy and security policies
- metrics and statistical information gathering
- program/system execution visualization
- fault localization, containment, resilience, recovery and repair
- systems with learning-enabled components
- dynamic type checking and assurance cases
- runtime verification for autonomy and runtime assurance
Application areas of runtime verification include cyber-physical systems, autonomous systems, safety/mission critical systems, enterprise and systems software, cloud systems, reactive control systems, health management and diagnosis systems, and system security and privacy.
### Papers ###
There are four categories of papers which can be submitted: regular, short, tool demo, and benchmark papers. Papers in each category will be reviewed by at least three members of the Program Committee.
- Regular Papers (up to 16 pages, not including references) should present original unpublished results. We welcome theoretical papers, system papers, papers describing domain-specific variants of RV, and case studies on runtime verification.
- Short Papers (up to 8 pages, not including references) may present novel but not necessarily thoroughly worked out ideas, for example emerging runtime verification techniques and applications, or techniques and applications that establish relationships between runtime verification and other domains.
- Tool Demonstration Papers (up to 8 pages, not including references) should present a new tool, a new tool component, or novel extensions to existing tools supporting runtime verification. The paper must include information on tool availability, maturity, selected experimental results and it should provide a link to a website containing the theoretical background and user guide. Furthermore, we strongly encourage authors to make their tools and benchmarks available with their submission.
- Benchmark Papers (up to 8 pages, not including references) should describe a benchmark, suite of benchmarks, or benchmark generator useful for evaluating RV tools. Papers should include information as to what the benchmark consists of and its purpose (what is the domain), how to obtain and use the benchmark, an argument for the usefulness of the benchmark to the broader RV community and may include any existing results produced using the benchmark. We are interested in both benchmarks pertaining to real-world scenarios and those containing synthetic data designed to achieve interesting properties. Broader definitions of benchmark e.g. for generating specifications from data or diagnosing faults are within scope. We encourage benchmarks that are tool agnostic, especially if they have been used to evaluate multiple tools. We also welcome benchmarks that contain verdict labels and with rigorous arguments for correctness of these verdicts, and benchmarks that are demonstrably challenging with respect to the state-of-the-art tools. Benchmark papers must be accompanied by an easily accessible and usable benchmark submission. Papers will be evaluated by a separate benchmark evaluation panel who will assess the benchmarks relevance, clarity, and utility as communicated by the submitted paper.
The Program Committee of RV 2021 will give a Springer-sponsored Best Paper Award to one eligible regular paper.
### Submissions ###
All papers and tutorials will appear in the conference proceedings in an LNCS volume. Submitted papers and tutorials must use the LNCS/Springer style detailed here: [ http://www.springer.de/comp/lncs/authors.html | http://www.springer.de/comp/lncs/authors.html ] .
Springer encourages authors to include their ORCIDs ( [ https://www.springer.com/gp/authors-editors/orcid | https://www.springer.com/gp/authors-editors/orcid ] ) in their papers.
Papers must be original work and not be submitted for publication elsewhere. Papers must be written in English and submitted electronically (in PDF format) using the EasyChair submission page here: [ https://easychair.org/conferences/?conf=rv2022 | https://easychair.org/conferences/?conf=rv2022 ] .
The page limitations mentioned above include all text and figures, but exclude references. Additional details omitted due to space limitations may be included in a clearly marked appendix, that will be reviewed at the discretion of reviewers, but not included in the proceedings.
At least one author of each accepted paper and tutorial must register and attend RV'22 to present.
Please find below a school announcement, with an excellent programme of
internationally-renowned speakers. The school is not only open to students
but also to post-docs and established researchers. The application deadline
is in one week.
**************************************************************************************************
CALL FOR APPLICATIONS
Joint EDBT-INTENDED School on Data and Knowledge
July 4th-9th, 2022
Bordeaux, France
https://edbtschool22.labri.fr/
***************************************************************************************************
APPLICATION DEADLINE: April 3rd, 2022
SOME STUDENT GRANTS AVAILABLE
***************************************************************************************************
The EDBT association and INTENDED AI Chair are happy to announce a jointly
sponsored Summer School on Data and Knowledge, which will be hosted in
Bordeaux, France, from Monday July 4 to Saturday July 9, 2022. The school
will cover a diverse range of topics around foundational database theory
and the use of knowledge (constraints, ontologies) in data management, with
a special focus on inconsistent, incomplete and more generally "imperfect"
data.
We invite students, postdocs, and other researchers interested in learning
about the foundational aspects of databases and handling imperfect data to
participate in the summer school.
Application and registration details can be found on the school website:
https://edbtschool22.labri.fr/
PROGRAM
The summer school will feature 11 tutorials from internationally renowned
researchers:
* Reasoning with Constraints
Andreas Pieris, University of Edinburgh, UK; University of Cyprus, Cyprus
* Foundations of Graph Databases
Pablo Barceló, Universidad Católica de Chile, Chile
* Provenance
Val Tannen, University of Pennsylvania, USA
* Enumeration
Nicole Schweikardt, Humboldt-University Berlin, Germany
* Probabilistic Databases
Antoine Amarilli, Télécom Paris, France
* Consistent Query Answering
Jef Wijsen, University of Mons, Belgium
* Quantitative Reasoning about Constraint Violations
Benny Kimelfeld, Technion, Israel
* Ontology-Mediated Query Answering
Carsten Lutz, University of Bremen, Germany
* Ontology-Based Data Access Made Practical
Diego Calvanese, Free University of Bozen-Bolzano, Italy; Ontopic
s.r.l., Italy; Umeå University, Sweden
* Computational Fact Checking
Paolo Papotti, EURECOM, France
* Data Quality
Floris Geerts, University of Antwerp, Belgium
The school will also feature several social events to encourage discussions
between participants and lecturers.
IMPORTANT DATES
Deadline for application: April 3, 2022
Notification of acceptance: April 15, 2022
Deadline for registration: May 22, 2022
EDBT Summer School: July 4–9, 2022
ORGANIZATION
Meghyn Bienvenu, CNRS & University of Bordeaux, France
Diego Figueira, CNRS & University of Bordeaux, France
If you have any questions, please contact us at:
edbtschool2022(a)easychair.org
[Apologies for multiple cross-posting]
--------------------------------------------------------------------------------
1st Call for Contributions
2nd International Workshop on
Logical Aspects in Multi-Agent Systems and Strategic Reasoning (LAMAS&SR)
2022
25-26 August 2022, Rennes, France
URL: https://lamassr.github.io/
--------------------------------------------------------------------------------
Objectives
----------
Logics and strategic reasoning play a central role in multi-agent systems.
Logics can be used, for instance, to express the agents’ abilities,
knowledge,
and objectives. Strategic reasoning refers to algorithmic methods that
allow for
developing good behaviour for the agents of the system. At the
intersection, we
find logics that can express existence of strategies or equilibria, and can
be
used to reason about them.
The LAMAS&SR workshop merges two international workshops: LAMAS (Logical
Aspects
of Multi-Agent Systems), which focuses on all kinds of logical aspects of
multi-agent systems from the perspectives of artificial intelligence,
computer
science, and game theory, and SR (Strategic Reasoning), devoted to all
aspects
of strategic reasoning in formal methods and artificial intelligence.
List of Topics
--------------
The topics covered by the workshop include, but are not limited to:
* Logical systems for specification, analysis, and reasoning about
multi-agent systems
* Logic-based modelling of multi-agent systems
* Dynamical multi-agent systems
* Deductive systems and decision procedures for logics for multi-agent
systems
* Development and implementation of methods for verification in multi-agent
systems
* Logic-based tools for multi-agent systems
* Logics for reasoning about strategic abilities
* Logics for multi-agent mechanism design, verification, and synthesis
* Logical foundations of decision theory for multi-agent systems
* Strategic reasoning in formal verification
* Automata theory for strategy synthesis
* Applications and tools for cooperative and adversarial reasoning
* Robust planning and optimisation in multi-agent systems
* Risk and uncertainty in multi-agent systems
* Quantitative aspects in strategic reasoning
Invited Speakers
----------------
* Rineke Verbrugge, University of Groningen
Co-Located Event
----------------
LAMAS&SR 2022 will be an event co-located with the 14th International
Conference
on Advances In Modal Logic (AiML 2022, 22-25 August).
About COVID-19
--------------
Local organizers are following closely the evolution of the pandemic
situation.
Our preference is for a full in-person event, but we will employ an online
or
hybrid format according to the situation.
Important Dates
---------------
* Paper submission: May 23 (AoE)
* Author notification: June 30 (AoE)
* Camera ready: July 15 (AoE)
* Workshop: August 25-26, 2022
Contribution Submission
-----------------------
Authors are invited to submit extended abstracts of 2 pages, plus 1 page for
references only, in the AAMAS 2022 format. Both published and unpublished
works
are welcome. Submissions are subject to a single-blind review process, thus,
submissions should not be anonymous, must be in PDF format, and will be
handled
via EasyChair at https://easychair.org/conferences/?conf=lamassr22
Although there will be no formal proceedings, accepted extended abstracts
will
be made available on the workshop website. Extensions of selected original
contributions will be then invited to a special issue of Games, an MDPI
open-access journal, with a special arrangement.
Program Co-Chairs
-----------------
* Fabio Mogavero, Università di Napoli Federico II
* Sophie Pinchinat, Université de Rennes 1
Program Committee
-----------------
* Thomas Agotnes, University of Bergen
* Natasha Alechina, Utrecht University
* Guy Avni, University of Haifa
* Massimo Benerecetti, University of Naples Federico II
* Hans van Ditmarsch, Open University of Netherlands
* Valentin Goranko, Stockholm University
* Wojtek Jamroga, University of Luxembourg and Polish Academy of Sciences
* Dario Della Monica, University of Udine
* Emiliano Lorini, Université Paul Sabatier
* Nicolas Markey, Université de Rennes 1
* Bastien Maubert, University of Naples Federico II
* John-Jules C. Meyer, Utrecht University
* Aniello Murano, University of Naples Federico II
* Rohit J. Parikh, City University of New York
* Sasha Rubin, The University of Sydney, Australia
* Marija Slavkovik, University of Bergen
* Yanjing Wang, Peking University
Organising Committee
--------------------
* Sophie Pinchinat, Université de Rennes 1
* Dylan Bellier, Université de Rennes 1
* Pierre Le Scornet, Université de Rennes 1
* Sophie Maupile, Université de Rennes 1
* Alexandre Terefenko, Université de Rennes 1
* Fabio Mogavero, Università di Napoli Federico II
Learning and Automata (LearnAut) -- ICALP 2022 workshop
July 4th - Paris, France and virtually
Website: https://learnaut22.github.io
Deadline: Extended to April 7th
Submission portal: https://easychair.org/conferences/?conf=learnaut2022
Learning models defining recursive computations, like automata and formal
grammars, are the core of the field called Grammatical Inference (GI). The
expressive power of these models and the complexity of the associated
computational problems are major research topics within mathematical logic
and computer science. Historically, there has been little interaction
between the GI and ICALP communities, though recently some important
results started to bridge the gap between both worlds, including
applications of learning to formal verification and model checking, and
(co-)algebraic formulations of automata and grammar learning algorithms.
The goal of this workshop is to bring together experts on logic who could
benefit from grammatical inference tools, and researchers in grammatical
inference who could find in logic and verification new fruitful
applications for their methods.
We invite submissions of recent work, including preliminary research,
related to the theme of the workshop. The Program Committee will select a
subset of the abstracts for oral presentation. At least one author of each
accepted abstract is expected to represent it at the workshop (in person,
or virtually).
Note that accepted papers will be made available on the workshop website
but will not be part of formal proceedings (i.e., LearnAut is a
non-archival workshop).
Topics of interest include (but are not limited to):
- Computational complexity of learning problems involving automata and
formal languages.
- Algorithms and frameworks for learning models representing language
classes inside and outside the Chomsky hierarchy, including tree and graph
grammars.
- Learning problems involving models with additional structure, including
numeric weights, inputs/outputs such as transducers, register automata,
timed automata, Markov reward and decision processes, and semi-hidden
Markov models.
- Logical and relational aspects of learning and grammatical inference.
- Theoretical studies of learnable classes of languages/representations.
- Relations between automata or any other models from language theory and
deep learning models for sequential data.
- Active learning of finite state machines and formal languages.
- Methods for estimating probability distributions over strings, trees,
graphs, or any data used as input for symbolic models.
- Applications of learning to formal verification and (statistical) model
checking.
- Metrics and other error measures between automata or formal languages.
** Invited speakers **
Jeffrey Heinz (Stony Brook University)
Sheila McIlraith (University of Toronto)
Ariadna Quattoni (Universitat Politècnica de Catalunya)
** Submission instructions **
Submissions in the form of anonymized extended abstracts must be at most 8
single-column pages long at most (plus at most four for bibliography and
possible appendixes) and must be submitted in the JMLR/PMLR format. The
LaTeX style file is available here:
https://ctan.org/tex-archive/macros/latex/contrib/jmlr
We do accept submissions of work recently published or currently under
review.
- Submission url: https://easychair.org/conferences/?conf=learnaut2022
- Submission deadline: April 7th
- Notification of acceptance: May 5th
- Early registration: TBD
** Program Committee **
- Dana Angluin (Yale University)
- Leonor Becerra-Bonache (Jean Monnet University, Saint-Étienne)
- Jorge Castro (Universitat Politècnica de Catalunya)
- Dana Fisman (Ben-Gurion University)
- Matthias Gallé (Naver Labs Europe)
- Gerco van Heerdt (University College London)
- Colin de la Higuera (University of Nantes)
- Falk Howar (TU Dortmund)
- Nils Jansen (Radboud University)
- Joshua Moerman (Open University of the Netherlands)
- Ariadna Quattoni (Universitat Politècnica de Catalunya)
- Bernhard Steffen (TU Dortmund)
- Henning Urbat (Friedrich-Alexander University Erlangen-Nürnberg)
- Frits Vaandrager (Radboud University)
- Ryo Yoshinaka (Tohoku University)
** Organizers **
Rémi Eyraud (Jean Monnet University, Saint-Étienne)
Tobias Kappé (ILLC, University of Amsterdam)
Guillaume Rabusseau (Mila & DIRO, Université de Montréal)
Matteo Sammartino (Royal Holloway, University of London & University
College London)
Guarded Fragments: Current Trends and Applications (GF@25)
April 5-6, 2022, Fully Online
Webpage: https://events.illc.uva.nl/GF25/
The Guarded Fragment (GF) was introduced in 1996 by Hajnal Andreka, Johan
van Benthem and Istvan Nemeti, as a decidable fragment of first-order logic
that aims to explain the attractive algorithmic and model theoretic
behavior of modal logic. It subsequently gave rise to a larger family of
decidable guarded fragments of first-order logic and second-order logic.
These guarded fragments are, up to today, still actively studied and used
in various application domains across different areas of computer science
and artificial intelligence (e.g., data management, knowledge
representation).
This workshop is a celebration of the 25th anniversary of GF. It will
showcase recent results, bringing together different strands of research,
and offering an opportunity for reflection.
The workshop is fully online, with a program consisting of 7 invited
lectures, spread out across two days.
CALL FOR PAPERS
QBF 2022
--------
International Workshop on
Quantified Boolean Formulas and Beyond
August 1, 2022
To be held in hybrid format (virtually + in-person).
https://www.ac.tuwien.ac.at/qbf2022/
Affiliated to and co-located with:
Int. Conf. on Theory and Applications
of Satisfiability Testing (SAT 2022),
August 2-5, 2022.
-------------------------------------------------------------
Quantified Boolean formulas (QBF) are an extension of propositional
logic which allows for explicit quantification over propositional
variables. The decision problem of QBF is PSPACE-complete, compared to
the NP-completeness of the decision problem of propositional logic (SAT).
Many problems from application domains such as model checking, formal
verification or synthesis are PSPACE-complete, and hence could be
encoded in QBF in a natural way. Considerable progress has been made
in QBF solving throughout the past years. However, in contrast to SAT,
QBF is not yet widely applied to practical problems in academic or
industrial settings. For example, the extraction and validation of
models of (un)satisfiability of QBFs has turned out to be
challenging, given that state-of-the-art solvers implement different
solving paradigms.
The goal of the International Workshop on Quantified Boolean Formulas
(QBF Workshop) is to bring together researchers working on theoretical
and practical aspects of QBF solving. In addition to that, it
addresses (potential) users of QBF in order to reflect on the
state-of-the-art and to consolidate on immediate and long-term
research challenges.
The workshop also welcomes work on reasoning with quantifiers in
related problems, such as dependency QBF (DQBF), quantified constraint
satisfaction problems (QCSP), and satisfiability modulo theories (SMT)
with quantifiers.
===============
IMPORTANT DATES
===============
May 1: Submission
June 5: Notification of acceptance
June 19: Final versions of accepted papers due
August 1: Workshop
Please see the workshop webpage for any updates:
https://www.ac.tuwien.ac.at/qbf2022/
======================
CALL FOR CONTRIBUTIONS
======================
The workshop is concerned with all aspects of current research on all
formalisms enriched by quantifiers, and in particular QBF. The topics
of interest include (but are not limited to):
Applications, encodings and benchmarks with quantifiers
QBF Proof theory and complexity results
Experimental evaluations of solvers or related tools
Case studies illustrating the power of quantifiers
Certificates and proofs for QBF, QCSP, SMT with quantifiers, etc.
Formats of proofs and certificates
Implementations of proof checkers and verifiers
Decision procedures
Calculi and their relationships
Data structures, implementation details and heuristics
Pre- and inprocessing techniques
Structural reasoning
==========
SUBMISSION
==========
Submissions of extended abstracts are invited and will be managed via
Easychair:
https://easychair.org/conferences/?conf=qbf2022
In particular, we invite the submission of extended abstracts on work
that has been published already, novel unpublished work, or work in
progress.
The following forms of submissions are solicited:
- Proposals for short tutorial presentations on topics related to the
workshop. Tutorial proposals will be reviewed by the PC. The number
of accepted tutorials depends on the overall number of accepted
papers and talks, with the aim to set up a balanced workshop
program.
- Talk abstracts reporting on already published work. Such an abstract
should include an outline of the planned talk, and pointers to
relevant bibliography.
- Talk proposals presenting work that is unpublished or in progress.
- Submissions which describe novel applications of QBF or related
formalisms in various domains are particularly welcome.
Additionally, this call comprises known applications which have been
shown to be hard for QBF solvers in the past as well as new
applications for which present QBF solvers might lack certain
features still to be identified.
Each submission should have an overall length of 1-4 pages in LNCS
format. Authors may decide to include an appendix with additional
material. Appendices will be considered at the reviewers' discretion.
The accepted extended abstracts will be published on the workshop
webpage. The workshop does not have formal proceedings.
Authors of accepted contributions are expected to give a talk at the
workshop.
=======
CONTACT
=======
qbf2022(a)easychair.org
=================
PROGRAM COMMITTEE
=================
Hubie Chen, Birkbeck, University of London
Florian Lonsing, Stanford University
Martina Seidl, JKU Linz
Friedrich Slivovsky, TU Wien