--- Book announcement ---
"Computability and Complexity"
written by Hubie Chen
published by The MIT Press
* Publisher website for book:
https://mitpress.mit.edu/9780262048620/computability-and-complexity/
* Book excerpt:
An excerpt of this book, which includes the first chapter (of 4), is freely
useable and freely distributable under a Creative Commons CC-BY-NC-ND
license. See the above website or use a direct link:
https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/143…
.
* Description:
This initiation to the theory of computation covers the core notions,
techniques, methods, and questions of this theory, before turning to
several advanced topics. This book combines intuitive and conceptual
discussion—--backed by numerous diagrams and examples—--with a precise
mathematical treatment that includes comprehensive and rigorous proofs.
Topics covered by this book include:
- Automata theory – deterministic and nondeterministic finite automata,
regular expressions, proving non-regularity via Myhill-Nerode theory, DFA
minimization;
- Computability theory – deterministic and nondeterministic Turing
machines, universal Turing machines, diagonalization and non-computable
languages, reductions, Rice’s theorem;
- Complexity theory – time complexity classes (P, NP, and coNP), the P
versus NP question, the theories of NP-completeness and of
coNP-completeness, numerous completeness proofs, the space complexity class
PSPACE, hierarchy theorems, parameterized complexity.
Numerous exercises and notes expand upon the main presentation and cover
topics such as Gödel incompleteness, counting complexity, logarithmic space
complexity, and treewidth.
CALL FOR PAPERS
Ninth International Conference on
Formal Structures for Computation and Deduction (FSCD 2024)
July 10-13, 2024, Tallinn, Estonia
https://fscd-conference.org/2024
IMPORTANT DATES
---------------
All deadlines are midnight anywhere-on-earth (AoE); late submissions
will not be considered.
Abstract: February 5, 2024
Submission: February 12, 2024
Rebuttal: April 2-6, 2024
Notification: April 22, 2024
Final version: May 6, 2024
OVERVIEW
--------
FSCD (https://fscd-conference.org/) covers all aspects of formal
structures for computation and deduction from theoretical foundations to
applications. Building on two communities, RTA (Rewriting Techniques and
Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD
embraces their core topics and broadens their scope to closely related
areas in logic, models of computation, semantics and verification in new
challenging areas.
The suggested, but not exclusive, list of topics for submission is:
1. Calculi:
- Rewriting systems (string, term, higher-order, graph, conditional,
modulo, infinitary, etc.);
- Lambda calculus;
- Logics (first-order, higher-order, equational, modal, linear,
classical, constructive, etc.);
- Proof theory (natural deduction, sequent calculus, proof nets, etc.);
- Type theory and logical frameworks;
- Homotopy type theory;
- Process algebras (synchronous, asynchronous, static and dynamic
semantics with and without time, etc.);
- Quantum calculi.
2. Methods in Computation and Deduction:
- Type systems (polymorphism, dependent, recursive, intersection,
session, etc.);
- Induction, coinduction;
- Matching, unification, completion, orderings;
- Strategies (normalization, completeness, etc.);
- Tree automata;
- Model building and model checking;
- Proof search and theorem proving;
- Constraint solving and decision procedures.
3. Semantics:
- Operational semantics and abstract machines;
- Game Semantics and applications;
- Domain theory and categorical models;
- Quantitative models (timing, probabilities, etc.);
- Quantum computation and emerging models in computation.
4. Algorithmic Analysis and Transformations of Formal Systems:
- Type inference and type checking;
- Abstract Interpretation;
- Complexity analysis and implicit computational complexity;
- Checking termination, confluence, derivational complexity and
related properties;
- Symbolic computation.
5. Tools and Applications:
- Programming and proof environments;
- Verification tools;
- Proof assistants and interactive theorem provers;
- Applications in industry;
- Applications of formal systems in other sciences;
- Applications of formal systems in education.
6. Formal Systems for Semantics and Verification in new challenging areas:
- Certification;
- Security;
- Blockchain protocols;
- Data bases;
- Deep learning and machine learning algorithms;
- Planning.
PUBLICATION
-----------
The proceedings will be published as an electronic volume in the Leibniz
International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl.
All LIPIcs proceedings are open access.
SPECIAL ISSUE
-------------
Authors of selected papers will be invited to submit an extended version
to a special issue of Logical Methods in Computer Science, or to TheoretiCS.
SUBMISSION GUIDELINES
---------------------
The submission site is:
https://easychair.org/conferences/?conf=fscd2024
Submissions must be formatted using the LIPIcs style files
(https://submission.dagstuhl.de/series/details/5#author) and submitted
via EasyChair.
Submissions can be made in two categories. Regular research papers are
limited to 15 pages, excluding references and appendices. They must
present original research which is unpublished and not submitted
elsewhere. System descriptions are limited to 15 pages, excluding
references. Shorter papers are welcome and will be given equal
consideration.
A system description must present new software tools, or significantly
new versions of such tools, in which FSCD topics play an important role.
An archive of the code with instructions on how to install and run the
tool must be submitted. In addition, a webpage where the system can be
experimented with should be provided.
One author of each accepted paper is expected to register and present
the work in person at the conference. Alternatively to in-person
presentation, also online presentation is possible, but in-person
registration by at least one author will still be required.
BEST PAPER AWARD BY JUNIOR RESEARCHERS
--------------------------------------
The program committee will select a paper in which at least one author
is a junior researcher, i.e. either a student or whose PhD award date is
less than three years from the first day of the meeting. When submitting
the paper, other authors should declare to the PC Chair that at least
50% of contribution is made by the junior researcher(s).
PROGRAM COMMITTEE CHAIR
-----------------------
Jakob Rehof, TU Dortmund University
Email: fscd2024 at easychair.org
PROGRAM COMMITTEE
-----------------
Thorsten Altenkirch, University of Nottingham
Sandra Alves, University of Porto
Takahito Aoto, Niigata University
Mauricio Ayala-Rincón, Brasilia University
Stephanie Balzer, CMU
Thierry Coquand, University of Gothenburg
Alejandro Díaz-Caro, Quilmes National University & CONICET-Buenos Aires
University
Claudia Faggian, CNRS, Université de Paris
Silvia Ghilezan, University of Novi Sad
Simon Gay, University of Glasgow
Cezary Kaliszyk, University of Innsbruck
Ambrus Kaposi, Eötvös Loránd University, Budapest
Dexter Kozen, Cornell University
Dominique Larchey-Wendling, CNRS, Loria
Marina Lenisa, University of Udine
Sonia Marin, University of Birmingham
Naoki Nishida, Nagoya University
Christine Paulin-Mohring, Paris-Saclay University
Pierre-Marie Pédrot, Inria Rennes-Bretagne-Atlantique
Elaine Pimentel, University College London
Jakob Rehof (Chair), TU Dortmund University
Simona Ronchi della Rocca, University of Torino
Sylvain Schmitz, Université Paris Cité
Aleksy Schubert, University of Warsaw
Jakob Grue Simonsen, University of Copenhagen
Kathrin Stark, Heriot-Watt University, Edinburgh
Lutz Straßburger, Inria Saclay
Tachio Terauchi, Waseda University
Sarah Winkler, Free University of Bolzano
CONFERENCE CHAIR
----------------
Niccolò Veltri, Tallinn University of Technology
WORKSHOP CHAIR
--------------
Luigi Liquori, Inria
STEERING COMMITTEE WORKSHOP CHAIR
--------------------------------
Cynthia Kop, Radboud University Nijmegen
PUBLICITY CHAIR
---------------
Carsten Fuhs, Birkbeck, University of London
FSCD STEERING COMMITTEE
-----------------------
Herman Geuvers (Chair), Radboud University Nijmegen
Patrick Baillot, CNRS, Université de Lille
Alejandro Díaz-Caro, Quilmes National University & CONICET-Buenos Aires
University
Amy Felty, University of Ottawa
Carsten Fuhs, Birkbeck, University of London
Marco Gaboardi, Boston University
Jürgen Giesl, RWTH Aachen University
Delia Kesner, Université Paris Cité
Naoki Kobayashi, University of Tokyo
Cynthia Kop, Radboud University Nijmegen
Luigi Liquori, Inria
Giulio Manzonetto, Université Paris-Nord
Daniele Nantes, Imperial College London / University of Brasilia
Femke van Raamsdonk, Vrije Universiteit Amsterdam
*******************************************************
* PhD positions in Combinatorics, Random Graphs, Logic, Complexity, and Semantics
* University of Sheffield, UK
* Fully funded for 3.5 years for both UK Home and Overseas students
* Possible times to start: ASAP/Spring 2024
* Deadline: 17th September 2023
* Details: https://www.jobs.ac.uk/job/DCG686/fully-funded-phd-positions-in-combinatori…
*******************************************************
Up to four fully funded research positions with the opportunity of undertaking a PhD are available within the Foundation of Computation (FOX) Group, Department of Computer Science, at the University of Sheffield: www.sheffield.ac.uk/dcs/research/groups/foundations-computation.
The FOX research group at Sheffield is growing rapidly. These posts provide excellent opportunities for graduate students (UK and overseas) to obtain a PhD in any active research area of the group (see below the research interests of potential supervisors).
The posts are fully funded for three and half years. Note that exceptionally strong overseas candidates will be considered as well, with full cover of tuition fees.
Dr. Charles Grellois is mainly interested in the verification of functional programs, would they be deterministic or probabilistic. He has worked on higher-order model-checking in the deterministic case, and on higher-order termination analysis in the probabilistic case. These approaches use techniques from linear logic and its models, category theory, (intersection) type theory, tree automata theory, probabilistic semantics, realizability… Several interesting questions are still open so that several different PhD projects could be discussed on these topics; but he is also open to other research topics in this area, to be discussed with the prospective student.
Dr. Maksim Zhukovskii is interested in combinatorics, probability, logic, computational and descriptive complexity. Currently Maksim is working on variety of topics including extremal combinatorics (Turan-type questions, saturation, colourings, etc), random graphs (thresholds, limiting distributions, logical limit laws, almost sure theories), average-case complexity (canonical labelling of random graphs, search problems in random graphs, reconstruction problems), enumerative combinatorics (random regular graphs, degree sequences), algebraic combinatorics (Cayley graphs, isomorphism problem for abelian groups, matroids), random walks, first order logic and expressive power of its fragments, second order logic and modal logic. See scholar.google.com/citations?user=sd_xBDQAAAAJ for the list of publications.
Dr. Jonni Virtema is keen to supervise students in any area of his current research, which relate to the interplay of logic and complexity theory. Current topics include logics and complexity theory related to numerical data, and temporal logics designed to express so-called hyperproperties, which are important in information flow and security. A further emerging topic is to study foundations of neural networks using the machinery of logics and complexity theory related to numerical data. See www.virtema.fi for further details.
Dr. Harsh Beohar is broadly interested in comparative concurrency semantics and in the interplay of category theory, logic, and semantics. Current topics include expressive modal logics, behavioural equivalence games, synthesising distinguishing/characteristic formulae all at the level of coalgebras. See dblp.org/pid/13/7482.html for an uptodate list of publications.
*[apologies for cross-postings]*
* Registration is finally open for the Fourteenth International Symposium
on Games, Automata, Logics, and Formal Verification (GandALF 23), to be
held in Udine (Italy) on September 18-20, 2023. *** Early registration
deadline is September 4, 2023 (Monday) *** We invite you to attend GandALF
2023. We will offer a very exciting technical and social program, which
includes 15 contributed talks, 4 invited talks by renowned international
theoretical computer scientists: - Weighted Automata At The Border Of
Decidability by Laure Daviaud
<https://www.city.ac.uk/about/people/academics/laure-daviaud> – University
of East Anglia (UK),- Complexity Aspects Of Logics In Team Semantics by
Juha Kontinen <https://researchportal.helsinki.fi/en/persons/juha-kontinen>
– University of Helsinki (Finland),- Strategic Reasoning Under Imperfect
Information – The Case Of Synchronous Recall by Sophie Pinchinat
<https://people.irisa.fr/Sophie.Pinchinat/> – IRISA/University of Rennes
(France),- The Church Synthesis Problem Over Continuous Time by Alexander
Rabinovich <http://www.cs.tau.ac.il/~rabinoa> – Tel Aviv University
(Israel), and an enchanting boat trip and dinner at a traditional Casone
(check it out at https://gandalf23.uniud.it/excursion/
<https://gandalf23.uniud.it/excursion/>). To register to the conference,
follow the instructions at https://gandalf23.uniud.it/registration/
<https://gandalf23.uniud.it/registration/>. For more details about GandALF
2023 and about how to organize your visit to Udine, check our webpage
(https://gandalf23.uniud.it/ <https://gandalf23.uniud.it/>). The full
program will be published soon. cheers Dario and Antonis (GandALF 23 PC
co-chairs)*
CALL FOR PAPERS
27th INTERNATIONAL CONFERENCE ON DATABASE THEORY (ICDT 2024)
Paestum, Italy 25th-28th March 2024
For more info check https://dastlab.github.io/edbticdt2024/
*About ICDT*
ICDT is a series of international scientific conferences on research of
data management theory
(https://databasetheory.org/icdt-pages). Since 2009, it is annually
and jointly held with EDBT (Extending DB Technology). The 27th edition
of ICDT, in 2024, will take place in Paestum, Italy.
Topics of Interest
We welcome research papers on *every* topic related to the principles
and theory of data management, provided that there is a clear connection
to foundational aspects. This includes, for example, articles on
"classical" data management topics such as:
The design and study of data models and query languages
The development and analysis of algorithms for data management
The theoretical investigation of various aspects underlying data
management systems (indexes, concurrency, distributed computation,
privacy and security, ...)
but also includes papers exploring existing or identifying new
connections between data management and other areas, such as the areas of:
knowledge representation, semantic web
information retrieval and data mining
machine learning/AI
distributed computing
theoretical computer science.
In all of the above, a clear emphasis on foundational aspects is
expected. You may want to check https://dblp.org/db/conf/icdt/index.html
to get an overview of previous editions of ICDT. The Program Committee
reserves the right to desk reject a submission when it is regarded to be
out of scope.
*Important dates*
The second submission cycle for ICDT 2024 has deadlines as follows:
ICDT Submission Cycle 2
=======================
Abstract deadline: September 13, 2023
Full Submission due : September 20, 2023
Notification: November 29, 2023
* Program Committee *
Program Committee Chair:
Graham Cormode (University of Warwick)
Program Committee Members:
Mahmoud Abo Khamis (Relational.AI)
Antoine Amarilli (Telecom Paris)
Yael Amsterdamer (Bar Ilan University)
Pablo Barceló (PUC Chile)
Vladimir Braverman (Rice University)
Marco Calautti (Università degli Studi di Milano)
Hubie Chen (King's College London)
Cristina Feier (University of Warsaw)
Diego Figueira (Université de Bordeaux)
Dominik Freydenberger (Loughborough University)
Martin Grohe (RWTH Aachen University)
Daniel Kifer (Penn State University)
Benny Kimelfeld (Technion)
Paraschos Koutris (University of Wisconsin-Madison)
Stefan Mengel (CNRS)
Frank Neven (Hasselt University)
Matthias Niewerth (Bayreuth University)
Jeff M. Phillips (University of Utah)
Reinhard Pichler (TU Wien)
Cristian Riveros (PUC Chile)
Francesco Scarcello (Università della Calabria)
Markus Schmid (Humboldt-Universität)
Yufei Tao (CUHK)
Jef Wijsen (University of Mons)
*Submission Instructions*
All submissions will be electronic via EasyChair
at https://easychair.org/conferences/?conf=icdt2024
Papers must be written in English and provide sufficient detail to allow
the program committee to assess their merits. The results must be
unpublished and not submitted for publication elsewhere, including the
proceedings of other symposia or workshops.
Papers must be submitted as PDF documents, using the LIPIcs style
(http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors).
Papers must be at most 15 pages, excluding references. Additional
details may be included in a clearly marked appendix, which, however,
will be read at the discretion of the program committee (online
appendices are not allowed). Papers not conforming to these requirements
may be rejected without further consideration.
The proceedings will appear in the Leibniz International Proceedings in
Informatics (LIPIcs) series, based at Schloss Dagstuhl. This guarantees
that the proceedings will be available online and free of charge, while
the authors retain the rights over their work.
At least one author of each accepted paper is expected to register at
the conference and to present the paper.
**ANONYMOUS SUBMISSION**
For 2024, ICDT will adopt anonymous submission, in line with other
leading conferences in the database community such as SIGMOD and PODS.
The intent of anonymous submission is to ensure that the identity of the
authors is not presented to the reviewers during the review process.
Specifically, submitted papers should not list authors or affiliations,
and should not include acknowlegments to funding sources, or other
colleagues or collaborators. References to the authors' own prior work
should not be distinguished from other references. Where this is not
possible (for instance, when referring to a specific system to which the
authors have privileged access), anonymized citations are permissible.
For more background on the motivation for anonymous submissions, and the
mechanisms to achieve it, please consult [Snodgrass, 2007]
https://www2.cs.arizona.edu/~rts/pubs/TODS07.pdf
Simultaneously, we encouage authors to make their submissions available
to the community via pre-print services such as ArXiv and through talks.
We do require that work is not labeled as "under submission at ICDT"
or indicates that it is under review, but otherwise place no
restrictions on sharing results. This does not conflict with the
anonymous submission requirement.
*Awards*
An award will be given to the Best Paper. Also, an award will be given
to the Best Newcomer Paper written by newcomers to the field of database
theory. The latter award will preferentially be given to a paper written
only by students; in that case the award will be called Best
Student-Paper Award. The program committee reserves the following
rights: not to give any award; to split an award among several papers;
and to define the notion of a newcomer. Papers authored or co-authored
by program committee members are not eligible for any award.
*** We apologize for possible cross-posting ***
*********** CALL FOR PAPER ***********
OVERLAY 2023
6th - 9th November, 2023 (the precise day(s) will be announced later)
Rome, Italy
https://overlay.uniud.it/workshop/2023
Co-located with AIxIA 2023
http://www.aixia2023.cnr.it/
*********** *********** ***********
The increasing adoption of Artificial Intelligence techniques in
safety-critical systems, employed in real-world scenarios, requires the
design of reliable, robust, and verifiable methodologies. Artificial
Intelligence systems employed in such applications need to provide formal
guarantees about their safety, increasing the need for a close interaction
between the Artificial Intelligence and Formal Methods scientific
communities, and possibly leading to the proposal of novel neurosymbolic
approaches.
To witness this increasing need, tools and methodologies integrating Formal
Methods and Artificial Intelligence, and more broadly symbolic and
sub-symbolic solutions, are getting more and more attention, especially
considering the wide-range and pervasive applications of machine and deep
learning models.
The workshop is the main official initiative supported by the OVERLAY group
(https://overlay.uniud.it). The event aims at establishing a stable,
long-term scientific forum on relevant topics connected to the
relationships between Artificial Intelligence and Formal Methods, by
providing a stimulating environment where researchers can discuss
opportunities and challenges at the border of the two areas.
Important goals of the workshop are (i) to encourage the ongoing
interaction between the formal methods and artificial intelligence
communities, (ii) to identify innovative tools and methodologies, and (iii)
to elicit a discussion on open issues and new challenges.
This year edition will be held between 6th and 9th November 2023 (the
precise day(s) will be announced later), as a hybrid workshop co-located
with AIxIA 2023 (http://www.aixia2023.cnr.it/), which is scheduled to be
held in Rome, Italy.
Participants must be registered to AIxIA 2023 (http://www.aixia2023.cnr.it/).
Overlay does not have an additional specific fee.
*** Invited speaker ***
Luciano Serafini - Fondazione Bruno Kessler, Italy
*** Call for contributions ***
We accept extended abstracts (4 pages + references) focusing on the
interaction between Artificial Intelligence and Formal Methods and on the
issue of symbolic/sub-symbolic integration. Invited talks will complement
the presentations of contributed papers.
Topics of interest include (but are not limited to):
automata theory
automated reasoning
automated planning and scheduling
controller synthesis
formal specification languages
formal verification
game theory
hybrid and discrete systems
logics in computer science
neurosymbolic approaches
logic for neural networks
neural networks for logic
reactive synthesis
runtime verification and monitoring
satisfiability modulo theories and theorem proving
specification and verification of machine/deep learning systems
tools and applications
Contributed papers can present recent results at the border of the two
fields, new research directions, challenges and perspectives. Presentation
of results recently published in other scientific journals or conferences
is also welcome.
We plan to include all papers in the Proceedings of the event, published at
CEUR Workshop Proceedings. CEUR WS proceedings are archival proceedings
indexed by DBLP and Scopus.
Submitted papers should not exceed four (4) pages plus references. Authors
are asked to use CEUR's LaTeX style, available at
https://overlay.uniud.it/workshop/2023/CEURART.zip.
Submissions must be in PDF format and will be handled via the EasyChair
Conference system at the following address:
https://easychair.org/my/conference?conf=overlay2023.
*** Important dates ***
- Paper submission: September 8th, 2023
- Acceptance notification: September 22nd, 2023
- Camera-ready submission: October 15th, 2023
- Workshop: between 6th and 9th November, 2023 (the precise day(s) will be
announced later)
*** Program Committee ***
Chairs
Andrea Brunello - University of Udine, Italy
Alessandro Gianola - Free University of Bozen-Bolzano, Italy
Fabio Mogavero - University of Napoli Federico II, Italy
PC Members
Dylan Bellier - University of Rennes, France
Massimo Benerecetti - University of Napoli Federico II, Italy
Laura Bozzelli - University of Napoli Federico II, Italy
Daniele Dell'Erba - University of Liverpool, UK
Dario Della Monica - University of Udine, Italy
Marco Faella - University of Napoli Federico II, Italy
Luca Geatti - University of Udine, Italy
Silvio Ghilardi - Università degli Studi di Milano, Italy
Nicola Gigante - Free University of Bozen-Bolzano, Italy
Inês Lynce - INESC-ID / Instituto Superior Técnico, Lisbon, Portugal
Andrea Mazzullo - University of Trento, Italy
Andrea Micheli - Fondazione Bruno Kessler, Trento, Italy
Andrea Orlandini - ISTC-CNR, Rome, Italy
Matteo Papini - Universitat Pompeu Fabra, Barcelona, Spain
Gian Luca Pozzato - University of Turin, Italy
Guido Sciavicco - University of Ferrara, Italy
Ionel Eduard Stan - Free University of Bozen-Bolzano, Italy
Cesare Tinelli - The University of Iowa, USA
Tiziano Villa - University of Verona, Italy
Matteo Zavatteri - University of Padova, Italy
*** Contacts ***
For more information email overlay2023(a)easychair.org<mailto:
overlay2023(a)easychair.org>
ILDS Coq and Lean Autumn School 2023
interactive theorem proving school
September 18-20, 2023, Bucharest, Romania
https://events.ilds.ro/autumnschool2023/
co-located with FROM 2023
https://from2023.cs.unibuc.ro
DESCRIPTION
-----------
The ILDS Coq and Lean Autumn School 2023 aims to introduce potential
students to the Coq and Lean proof assistants, as well as to
theoretical underpinnings of interactive theorem proving. It is the
second school on interactive theorem proving organized in Bucharest,
following the ICUB Coq Autumn School, which was held in September 2018.
The event is co-located with FROM 2023 (https://from2023.cs.unibuc.ro/),
whose participants are eligible for a special discounted fee for the school.
ORGANIZERS
----------
Institute for Logic and Data Science (ILDS, https://ilds.ro/)
Research Center for Logic, Optimization and Security (LOS), University of
Bucharest (https://los.cs.unibuc.ro/)
SPEAKERS
--------
Horațiu Cheval (University of Bucharest)
Vlad Rusu (INRIA Lille)
Andrei Sipoș (University of Bucharest & ILDS & IMAR)
Julian Sutherland (Nethermind)
Traian Florin Șerbănuță (RV & University of Bucharest & ILDS)
COURSES
-------
Andrei Sipoș, Introduction to Type Theory for Interactive Theorem Proving
Vlad Rusu, Traian Florin Șerbănuță, Introduction to Coq
Julian Sutherland, Horațiu Cheval, Introduction to Lean
No parallel sessions are planned, so it will be possible to attend all
the courses.
REGISTRATION
------------
The registration fee is 150 EUR for the general public and
75 EUR for those who participate at FROM 2023.
It covers attendance, lunch, coffee breaks, and the official dinner.
To register, please use the common registration form
(https://forms.gle/aZ7zqK3UNwLeGaRL6) for the ILDS Coq
and Lean Autumn School 2023 and FROM 2023. Note that
one can still register later, separately, for the autumn school
and still benefit from the discount.
ILDS offers a limited number of fellowships (waiving the
registration fee) for students. Students interested in getting
a fellowship need to complete an application form
(https://forms.gle/ByrWCxUahQcfK35HA) by 1 August 2023.
Applicants will be notified by 14 August 2023.
IMPORTANT DATES
---------------
Deadline for fellowship (fee waiver) application: 1 August 2023
Notification of fellowship applicants: 14 August 2023
Deadline for registration: 7 September 2023
School: 18-20 September 2023
***************
Further information is available on our website,
https://events.ilds.ro/autumnschool2023/
FROM 2023
Seventh Working Formal Methods Symposium
September 21-22, 2023, Bucharest, Romania
https://from2023.cs.unibuc.ro
co-located with the ILDS Coq and Lean Summer School
https://events.ilds.ro/autumnschool2023/
DESCRIPTION
-----------
The Working Formal Methods Symposium (FROM) aims to bring together
researchers and practitioners who work on formal methods by contributing
new theoretical results, methods, techniques, and frameworks, and/or by
creating or using software tools that apply theoretical contributions.
The program of the symposium includes invited lectures and regular
contributions.
Submissions on the general topics of formal methods, theoretical computer
science, logic and applications are welcome.
This event is co-located with the ILDS Coq and Lean Autumn School 2023
(see https://events.ilds.ro/autumnschool2023/), for which there is a special
discounted fee for FROM 2023 participants.
ORGANIZERS
----------
Faculty of Mathematics and Computer Science of the University of Bucharest (
https://fmi.unibuc.ro/)
Institute for Logic and Data Science (ILDS, https://ilds.ro/)
IMPORTANT DATES
---------------
Deadline for paper/abstract submission: 25 July 2023
Deadline for author notification: 25 August 2023
Deadline for revised paper/abstract submission: 1 September 2023
Deadline for registration: 7 September 2023
Symposium: 21-22 September 2023
INVITED SPEAKERS
----------------
Radu Iosif (CNRS-VERIMAG)
Ulrich Kohlenbach (Technische Universität Darmstadt)
Eugenio Omodeo (Università degli Studi di Trieste)
Alicia Villanueva (Universitat Politècnica de València)
SUBMISSIONS
-----------
Papers of up to 16 pages prepared according to the EPTCS template
(see http://style.eptcs.org/) must be submitted electronically
using the EasyChair submission system at:
https://easychair.org/my/conference?conf=from2023
Research papers must contain original research results not submitted and
not
published elsewhere. They will be considered for inclusion in the EPTCS
proceedings
of the symposium. Authors who want to present work in progress or discuss
new aspects or a survey of their older research results at the workshop are
welcome
to submit an extended abstract (up to 8 pages). Papers will be refereed and
accepted
on the basis of their scientific merit and relevance to the workshop topics.
TOPICS OF INTEREST
------------------
The topics of interest for FROM 2023 include, but are not limited to:
Areas and formalisms:
+ Category theory in computer science
+ Distributed systems and concurrency
+ Domain science and engineering
+ Formal languages and automata theory
+ Formal modelling, verification and testing
+ Logic in computer science
+ Logical frameworks
+ Mathematical structures in computer science
+ Models of computation
+ Semantics of programming languages
+ Type systems
Methods:
+ Automated reasoning and model generation
+ Automated induction
+ Certified programs
+ Data-flow and control-flow analysis
+ Deductive verification
+ Mechanized proofs
+ Model checking
+ Proof mining
+ Symbolic computation
+ Term rewriting
Applications:
+ Computational logic
+ Computer mathematics
+ Knowledge representation, ontology reasoning, deductive databases
+ Program analysis
+ Verification and synthesis of software and hardware
+ Uncertainty reasoning and soft computing
Submissions on any other related topics are welcome.
PROGRAMME COMMITTEE
-------------------
Florin Crăciun (Babeș-Bolyai University of Cluj-Napoca)
Temur Kutsia (Johannes Kepler University Linz)
Laurențiu Leuștean (University of Bucharest & ILDS & IMAR) (co-chair)
Dorel Lucanu (Alexandru Ioan Cuza University of Iași)
Mircea Marin (West University of Timișoara)
David Nowak (CNRS & University of Lille)
Peter Csaba Ölveczky (University of Oslo)
Corina Păsăreanu (NASA & Carnegie Mellon University)
Andrei Popescu (University of Sheffield)
Thomas Powell (University of Bath)
Grigore Roșu (University of Illinois at Urbana-Champaign)
Vlad Rusu (INRIA Lille)
Andrei Sipoș (University of Bucharest & ILDS & IMAR) (co-chair)
Viorica Sofronie-Stokkermans (University of Koblenz and Landau)
REGISTRATION
------------
The registration fee is 100 EUR for the general public and
50 EUR for students. It covers the symposium kit, lunch, coffee breaks,
and the symposium dinner.
To register, please use the common registration form
(https://forms.gle/aZ7zqK3UNwLeGaRL6) for FROM 2023 and the
ILDS Coq and Lean Autumn School 2023
(https://events.ilds.ro/autumnschool2023/), for which there is
a special discounted fee for FROM 2023 participants. Note that
one can still register later, separately, for the autumn school
and still benefit from the discount.
***************
Further information is available on our website,
https://from2023.cs.unibuc.ro/
*** We apologize for possible cross posting ***
*********** CALL FOR PAPER ***********
OVERLAY 2023
6th - 9th November, 2023 (the precise day(s) will be announced later)
Rome, Italy
https://overlay.uniud.it/workshop/2023
Co-located with AIxIA 2023
http://www.aixia2023.cnr.it/
*********** *********** ***********
The increasing adoption of Artificial Intelligence techniques in safety-critical systems, employed in real world scenarios, requires the design of reliable, robust, and verifiable methodologies. Artificial Intelligence systems employed in such applications need to provide formal guarantees about their safety, increasing the need for a close interaction between the Artificial Intelligence and Formal Methods scientific communities, and possibly leading to the proposal of novel neurosymbolic approaches.
To witness this increasing need, tools and methodologies integrating Formal Methods and Artificial Intelligence, and more broadly symbolic and sub-symbolic solutions, are getting more and more attention, especially considering the wide-range and pervasive applications of machine and deep learning models.
The workshop is the main official initiative supported by the OVERLAY group (https://overlay.uniud.it). The event aims at establishing a stable, long-term scientific forum on relevant topics connected to the relationships between Artificial Intelligence and Formal Methods, by providing a stimulating environment where researchers can discuss opportunities and challenges at the border of the two areas.
Important goals of the workshop are (i) to encourage the ongoing interaction between the formal methods and artificial intelligence communities, (ii) to identify innovative tools and methodologies, and (iii) to elicit a discussion on open issues and new challenges.
This year edition will be held between 6th and 9th November 2023 (the precise day(s) will be announced later), as a hybrid workshop co-located with AIxIA 2023 (http://www.aixia2023.cnr.it/), which is scheduled to be held in Rome, Italy.
Participants must be registered to AIxIA 2023 (http://www.aixia2023.cnr.it/). Overlay does not have an additional specific fee.
*** Invited speaker ***
Luciano Serafini - Fondazione Bruno Kessler, Italy
*** Call for contributions ***
We accept extended abstracts (4 pages + references) focusing on the interaction between Artificial Intelligence and Formal Methods and on the issue of symbolic/sub-symbolic integration. Invited talks will complement the presentations of contributed papers.
Topics of interest include (but are not limited to):
automata theory
automated reasoning
automated planning and scheduling
controller synthesis
formal specification languages
formal verification
game theory
hybrid and discrete systems
logics in computer science
neurosymbolic approaches
logic for neural networks
neural networks for logic
reactive synthesis
runtime verification and monitoring
satisfiability modulo theories and theorem proving
specification and verification of machine/deep learning systems
tools and applications
Contributed papers can present recent results at the border of the two fields, new research directions, challenges and perspectives. Presentation of results recently published in other scientific journals or conferences is also welcome.
We plan to include all papers in the Proceedings of the event, published at CEUR Workshop Proceedings. CEUR WS proceedings are archival proceedings indexed by DBLP and Scopus.
Submitted papers should not exceed four (4) pages plus references. Authors are asked to use CEUR's LaTeX style, available at https://overlay.uniud.it/workshop/2023/CEURART.zip.
Submissions must be in PDF format and will be handled via the EasyChair Conference system at the following address: https://easychair.org/my/conference?conf=overlay2023.
*** Important dates ***
- Paper submission: September 8th, 2023
- Acceptance notification: September 22nd, 2023
- Camera-ready submission: October 15th, 2023
- Workshop: between 6th and 9th November, 2023 (the precise day(s) will be announced later)
*** Program Committee ***
Chairs
Andrea Brunello - University of Udine, Italy
Alessandro Gianola - Free University of Bozen-Bolzano, Italy
Fabio Mogavero - University of Napoli Federico II, Italy
PC Members
Dylan Bellier - University of Rennes, France
Massimo Benerecetti - University of Napoli Federico II, Italy
Laura Bozzelli - University of Napoli Federico II, Italy
Daniele Dell'Erba - University of Liverpool, UK
Dario Della Monica - University of Udine, Italy
Marco Faella - University of Napoli Federico II, Italy
Luca Geatti - University of Udine, Italy
Silvio Ghilardi - Università degli Studi di Milano, Italy
Nicola Gigante - Free University of Bozen-Bolzano, Italy
Inês Lynce - INESC-ID / Instituto Superior Técnico, Lisbon, Portugal
Andrea Mazzullo - University of Trento, Italy
Andrea Micheli - Fondazione Bruno Kessler, Trento, Italy
Andrea Orlandini - ISTC-CNR, Rome, Italy
Matteo Papini - Universitat Pompeu Fabra, Barcelona, Spain
Gian Luca Pozzato - University of Turin, Italy
Guido Sciavicco - University of Ferrara, Italy
Ionel Eduard Stan - Free University of Bozen-Bolzano, Italy
Cesare Tinelli - The University of Iowa, USA
Tiziano Villa - University of Verona, Italy
Matteo Zavatteri - University of Padova, Italy
*** Contacts ***
For more information email overlay2023(a)easychair.org<mailto:overlay2023@easychair.org>
Dear colleagues,
I hope this email finds you well. I wanted to inform you that Udine
University will be hosting a Summer School on Reactive Synthesis from
August 28 to August 31 and a Workshop on Synthesis, Monitoring and
Learning on from August 31 to September 1. The program includes lectures
from established researchers, covering both theory and applications of
the synthesis problem.
To ensure the success of this event, I'd like to kindly ask your help in
forwarding the following call for attendance to anyone you believe might
be interested in participating, particularly students and young researchers.
Thank you for your attention and support.
Best regards,
Dario Della Monica
-----------------------------------------------------------------------------
Third edition of the UniVr/UniUd Summer School on Formal Methods for
Cyber-Physical Systems - Udine, August 28-31
http://tcs.uniud.it/summer-school
<http://tcs.uniud.it/summer-school>
+
Workshop on Synthesis, Monitoring and Learning - Udine, August
31-September 1
http://tcs.uniud.it/smile
<http://tcs.uniud.it/smile>
-----------------------------------------------------------------------------
Synthesis is a fundamental problem in computer science and mathematics,
concerned with automatically generating programs that satisfy a given
logical specification. Its applications span a range of domains,
including model-based system design, software engineering, and automated
theorem proving. For instance, designing a controller that guides the
behavior of a reactive system, that is, a system that continually
interacts with its environment, can be framed as a synthesis problem.
Similarly, the design and verification of a distributed system often
depend on distributed synthesis, which finds programs that enforce
correct component interaction and satisfy desired specifications.
The third edition of the Summer School on Formal Methods for
Cyber-Physical Systems offers an in-depth exploration of reactive
synthesis, a topic that was already introduced in the first edition of
the school. The lecturers will provide a systematic account of the main
achievements and the current trends of research in reactive synthesis,
covering both theory and applications.
The course will begin with an overview of the classical synthesis
problem in the finite-state setting, as originally formulated by Church
and solved by Buechi and Landweber. This introductory part will
introduce the terminology of infinite two-player games, explain the
automatic construction of winning strategies in “regular games”, and
address history of the subject, discussing extensions and open problems.
From there, the course will investigate approaches for making reactive
synthesis more efficient and practical, including techniques for solving
the synthesis problem in restricted settings, for decomposing the
problem into subproblems, and for employing algorithms, data structures,
and heuristics to manage complexity. Variants of the synthesis problem
will also be explored, such as control strategies for hybrid and
distributed systems, monitor synthesis, synthesis under incomplete
information, distributed synthesis, and symmetric synthesis. The
implementation of synthesis tools will also receive significant
attention, with a focus on recent advances and applications of UPPAAL
Stratego and the SYNTCOMP reactive synthesis competition.
The summer school will conclude with a workshop on emerging research
trends in synthesis, monitoring, and learning, which showcases some
exciting interactions between formal methods and machine learning.
Distinguished invited speakers will lead the workshop. Participants will
also have the opportunity to engage with peers from around the world and
may propose to deliver short research talks voluntarily.
### Lecturers
Wolfgang Thomas - RWTH Aachen University, Germany
3-hour lecture on “Synthesis of strategies in infinite two-player games”
We give an introduction to the synthesis of reactive systems in the
finite-state setting, using the terminology of infinite two-player games
and explaining the automatic construction of winning strategies in
“regular games”. We also address the history of the subject, discuss
extensions, and mention basic problems that are still open.
Martin Zimmermann - Aalborg University, Denmark
3-hour lecture on “Synthesis of infinite-state systems”
The reactive synthesis problem asks to compute, from a given
specification of the input-output behavior of a reactive system, a
system satisfying this specification (or to determine that no such
system exists). In this lecture, we consider the synthesis of
infinite-state systems with a focus on pushdown systems, which model
simple recursive systems with finite data. On a technical level, we show
how to solve infinite games on configuration graphs of pushdown automata
and present recent work on generalizations to history-deterministic
pushdown automata.
Kim G. Larssen - Aalborg University, Denmark
3-hour lecture on “Synthesis and Optimization for Cyber Physical Systems”
In these lectures we will present recent advances and applications of
the tool UPPAAL Stratego (http://www.uppaal.org/
<http://www.uppaal.org/>)
supporting automatic synthesis of guaranteed safe and near-optimal
control strategies for Cyber Physical Systems (CPS). UPPAAL Stratego
combines symbolic methods from model checking, reinforcement learning
methods from machine learning, as well as abstraction techniques for
hybrid games. Trade-offs between efficiency of strategy representation
and degree of optimality subject to safety constraints will be
discussed, as well as successful applications (autonomous driving
maneuvers, heating systems and traffic control).
Dana Fisman - Ben Gurion University of the Negev, Israel
3-hour lecture on “Automata learning of languages of finite and infinite
words”
In these lectures we will get acquainted with the research area called
grammatical inference or automata learning. We will start with the
earliest results on the subject, and span different learning paradigms.
We will describe several positive results, and efficient algorithms for
learning regular languages. We will prove several negative results for
learning different classes of languages in different learning paradigms.
We will then discuss state-of-the-art results on learning regular
languages of infinite words.
Swen Jacobs - CISPA Helmholtz-Center for Information Security, Germany
3-hour lecture on “Reactive synthesis: towards practice”
I will give an overview of different lines of research that try to make
reactive synthesis (more) practical. This includes research into
approaches to restrict the problem to more efficiently solvable
fragments, into ways to split the problem into subproblems that can be
solved independently or iteratively, and into efficient algorithms and
data structures as well as heuristics that allow us to implement
synthesis tools that can solve problems of significant size. I will
report on progress observed in the reactive synthesis competition
(SYNTCOMP), and on case studies and benchmark problems that demonstrate
the capabilities of state-of-the-art synthesis tools.
Alessandro Cimatti - Fondazione Bruno Kessler, Italy
3-hour lecture on “Runtime verification and monitor synthesis”
Runtime Verification (RV) is a lightweight verification technique that
aims at checking whether a run of a system under scrutiny (SUS)
satisfies or violates a given correctness specification. The lecture
will first overview the general framework of RV, and the techniques to
synthesize run-time monitors that can be efficiently executed in
combination with the SUS. Then, we will cover the relationship between
RV and the field of Fault Detection and Isolation (FDI). In FDI, runtime
monitors are built taking into account models of the SUS, in order to
monitor the occurrence of internal (faulty) conditions that are not
directly observable.
### Programme
Monday, August 28
13:30 - 14:00 Registration
14:00 - 14:30 Course Introduction
14:30 - 16:00 Wolfgang Thomas
16:00 - 16:30 Coffee break
16:30 - 18:00 Wolfgang Thomas
Tuesday, August 29
09:30 - 11:00 Martin Zimmermann
11:00 - 11:30 Coffee break
11:30 - 13:00 Martin Zimmermann
13:00 - 14:00 Lunch
14:30 - 16:00 Kim G. Larsen
16:00 - 16:30 Coffee break
16:30 - 18:00 Kim G. Larsen
Wednesday, August 30
09:30 - 11:00 Dana Fisman
11:00 - 11:30 Coffee break
11:30 - 13:00 Dana Fisman
13:00 - 14:00 Lunch
14:30 - 16:00 Swen Jacobs
16:00 - 16:30 Coffee break
16:30 - 18:00 Swen Jacobs
19:00 - 23:00 Social dinner
Thursday, August 31
09:30 - 11:00 Alessandro Cimatti
11:00 - 11:30 Coffee break
11:30 - 13:00 Alessandro Cimatti
13:00 - 14:00 Lunch
14:30 - 16:30 Workshop on Synthesis, Monitoring and Learning
Friday, September 1
09:30 - 14:00 Workshop on Synthesis, Monitoring and Learning
### Admission and accommodation
The course is offered in a hybrid format giving the possibility to
remotely attend the course (on the Microsoft Teams platform).
On-site places are limited and assigned on first come first served basis.
The registration fees are:
- On-site participation, 250.00 Euro + VAT 22%
- Online participation, 120.00 Euro + VAT 22%
Deadline for online application is August 18, 2023.
Participation application is available at
https://www.cism.it/en/activities/courses/J2303/
<https://www.cism.it/en/activities/courses/J2303/>
### Contacts
CISM, Palazzo del Torso
Piazza Garibaldi 18, 39100 Udine, Italy
tel. +39 0432 248511
email: cism(a)cism.it | http://www.cism.it/
<http://www.cism.it/>
### Organization
Angelo Montanari - University of Udine, Italy
Gabriele Puppis - University of Udine, Italy
Tiziano Villa - University of Verona, Italy
--
Dario Della Monica, Associate Professor (Professore Associato)
Department of Mathematics, Computer Science, and Physics
University of Udine
via delle Scienze, 206 - 33100 Udine, Italy
cell: (+39) 328 2477327
email: dario.dellamonica [at] uniud.it
skype: dariodellamonica
web site:http://users.dimi.uniud.it/~dario.dellamonica/