- finite-model-theory - lists.rwth-aachen.de

CONCUR 2022 - last CFP
by Bartek Klin 03 Apr '22

03 Apr '22

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

1 0

EATCS-IPEC Nerode Award - CfN
by Anuj Dawar 02 Apr '22

02 Apr '22

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".

1 0

Second Call for Papers - Runtime Verification RV'22 (Computational
by Thao Dang 01 Apr '22

01 Apr '22

[ 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.

1 0

Summer School on Data and Knowledge (Bordeaux, France)
by Diego Figueira 28 Mar '22

28 Mar '22

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

1 0

LAMAS & SR 2022 - 1st Call for Contributions
by Fabio Mogavero 27 Mar '22

27 Mar '22

[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

1 0

Learning and Automata (LearnAut) 2022 -- ICALP 2022 Workshop, last
by Tobias Kappé 25 Mar '22

25 Mar '22

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)

1 0

April 5-6, 2022: Guarded Fragments: Current Trends and Applications (GF@25)
by Balder ten Cate 22 Mar '22

22 Mar '22

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.

1 0

Call for papers: QBF '22
by HUBERT MING CHEN 21 Mar '22

21 Mar '22

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

1 0

Permanent positions at University of Birmingham
by Anupam das 21 Mar '22

21 Mar '22

Dear colleagues, The University of Birmingham is seeking to make several tenured appointments at the moment: * Assistant or Associate Professor (deadline 3 April). https://bham.taleo.net/careersection/external/jobdetail.ftl?job=220000E3&tz… * Professor (deadline 25 March). https://bham.taleo.net/careersection/external/jobdetail.ftl?job=220000G4&tz… These posts are not associated to any particular research area, but the School has an outstanding tradition in Theoretical Computer Science: https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-c… If you are interested in applying please feel free to contact one of us for informal discussions: https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-c… Best, Anupam

1 0

Workshop on Advances in Separation Logics (ASL 2022 @ FLOC 2022)
by RADU IOSIF 18 Mar '22

18 Mar '22

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)

1 0