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

FSCD 2024: First Call for Papers
by Carsten Fuhs 31 Aug '23

31 Aug '23

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

1 0

PhD positions in Combinatorics, Random Graphs, Logic, Complexity, and
by Jonni T Virtema 25 Aug '23

25 Aug '23

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

1 0

GandALF 2023: Registration is open – Call For Participation
by Gabriele Puppis 21 Aug '23

21 Aug '23

*[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)*

1 0

ICDT 2024 - Call for Papers (Second Round)
by Graham Cormode 09 Aug '23

09 Aug '23

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.

1 0

Fwd: CFP: 5th Workshop on Artificial Intelligence and fOrmal
by Fabio Mogavero 14 Jul '23

14 Jul '23

*** 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>

1 0

ILDS Coq and Lean Autumn School 2023 – THIRD CALL FOR PARTICIPATION
by Andrei Sipoș 14 Jul '23

14 Jul '23

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/

1 0

FROM 2023 – THIRD CALL FOR PAPERS
by Andrei Sipoș 14 Jul '23

14 Jul '23

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/

1 0

CFP: 5th Workshop on Artificial Intelligence and fOrmal VERification,
by Andrea Brunello 14 Jul '23

14 Jul '23

*** 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>

1 0

Summer School on Reactive Synthesis + Workshop on Synthesis,
by Dario Della Monica 04 Jul '23

04 Jul '23

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/

1 0

FMCAD 2023 Student Forum: Call for Contributions
by Rozier, Kristin-Yvonne [AER E] 02 Jul '23

02 Jul '23

(apologies for multiple copies) ====================================================================== 2023 Formal Methods in Computer-Aided Design (FMCAD): Student Forum October 23-27, Ames, Iowa, USA Call for Student Contributions! ====================================================================== Please consider submitting or encouraging your students to submit to this year's FMCAD student forum. More information can be found here: https://fmcad.org/FMCAD23/student_forum/ Student Forum Continuing the tradition of the previous years, FMCAD 2023 is hosting a Student Forum that provides a platform for students at any career stage (undergraduate or graduate) to introduce their research to the wider Formal Methods community, and solicit feedback. Main Activities Each student will give a short presentation and present their poster in the poster session. Submissions for the event must be short reports describing research ideas or ongoing work that the student is currently pursuing and must be within the scope of FMCAD. Work, part of which has been previously published, will be considered; the novel aspect to be addressed in future work must be clearly described in such cases. All submissions will be reviewed by the Student Forum's program committee. Important Dates Student forum submission: July 12, 2023 Student forum notification: Aug 10, 2023 These deadlines are 11:59 pm AoE (Anywhere on Earth) Format The event will consist of short presentations by the student authors of each accepted submission and of a poster that will be on display throughout the duration of the conference. All participants of the conference are encouraged to attend the talks and approach the students during the poster presentation. Instructions for the preparation of the talks and poster sessions will be announced on notification of acceptance. Visibility Accepted submissions will be listed, with title and author name, in the event description in the conference proceedings. The authors will also have the option to upload their slide deck/poster/presentation to the FMCAD website. The report itself will not appear in the FMCAD proceedings. Thus, the presentation at the forum should not interfere with potential future submissions of this research (to FMCAD or elsewhere). Travel Awards Most of the applicants will receive travel reimbursement after the conference (the amount of support will be announced later). The first author of each contribution will be given priority over other authors. Please make sure you hold on to all receipts for reimbursement. Further instructions on how to apply for travel grants will be on the website. ---------- ____________________________________________________________ __ /\ \ \_____ / \ ###[==_____> / \ /_/ __ / __ \ \ \_____ | ( ) | ###[==_____> /| /\/\ |\ /_/ / | | | | \ / |=|==|=| \ Kristin Yvonne Rozier, Ph.D. / | | | | \ Associate Professor, Iowa State Univ / USA | ~||~ |NASA \ Departments of Aerospace Engineering, |______| ~~ |______| Computer Science, Mathematics, and (__||__) Electrical and Computer Engineering /_\ /_\ !!! !!! laboratory.temporallogic.org

1 0