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

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

GandALF 2023: Deadline extension (abstract and paper submission)
by Gabriele Puppis 28 Jun '23

28 Jun '23

[apologies for cross-postings] · New abstract submission deadline: 23 June 2023 *30 June 2023* · New paper submission deadline: 30 June 2023 *7 July 2023* The Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 23) will be held in Udine (Italy) on *September 18-20, 2023*. The aim of GandALF 2023 <https://urldefense.com/v3/__https://gandalf23.uniud.it/__;!!IBzWLUs!Rooz29B…> is to bring together researchers from academia and industry who are actively working in the fields of Games, Automata, Logics, and Formal Verification. The idea is to cover an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization. Papers focused on formal methods are especially welcome. Authors are invited to submit original research or tool papers on all relevant topics in these areas. Papers discussing new ideas that are at an early stage of development are also welcome. The topics covered by the conference include, but are not limited to, the following: · Automata Theory · Automated Deduction · Computational aspects of Game Theory · Concurrency and Distributed computation · Decision Procedures · Deductive, Compositional, and Abstraction Techniques for Verification · Finite Model Theory · First-order and Higher-order Logics · Formal Languages · Formal Methods for Systems Biology, Hybrid, Embedded, and Mobile Systems · Game Semantics · Games and Automata for Verification · Logical aspects of Computational Complexity · Logics of Programs · Modal and Temporal Logics · Model Checking · Models of Reactive and Real-Time Systems · Probabilistic Models (Markov Decision processes) · Program Analysis and Software Verification · Reinforcement Learning · Run-time Verification and Testing · Specification and Verification of Finite and Infinite-state Systems · Synthesis Important Dates · Abstract submission deadline: 23 June 2023 *30 June 2023* · Paper submission deadline: 30 June 2023 *7 July 2023* · Acceptance notification: 7 August 2023 · Camera-ready deadline: 6 September 2023 · Conference dates: 18-20 September 2023 ⚠ all deadlines are AoE <https://urldefense.com/v3/__https://time.is/Anywhere_on_Earth__;!!IBzWLUs!R…> Publication The proceedings will be published by Electronic Proceedings in Theoretical Computer Science <https://urldefense.com/v3/__http://www.eptcs.org/__;!!IBzWLUs!Rooz29BBsOWdk…>. Authors of selected papers will be invited to submit a revised version of their work to a special issue of Logical Methods in Computer Science <https://urldefense.com/v3/__https://lmcs.episciences.org/__;!!IBzWLUs!Rooz2…> . The previous editions of GandALF already led to special issues of the International Journal of Foundations of Computer Science (GandALF 2010), Theoretical Computer Science (GandALF 2011 and 2012), Information and Computation (GandALF 2013, 2014, 2016, 2017, 2018, 2019, and 2020), Acta Informatica (GandALF 2015) and Logical Methods in Computer Science (GandALF 2021 and 2022). Submission Submitted papers should not exceed 14 pages (excluding references and clearly marked appendices) using EPTCS format (please use the LaTeX style provided here <https://urldefense.com/v3/__http://style.eptcs.org__;!!IBzWLUs!Rooz29BBsOWd…>), be unpublished, and contain original research. For papers reporting experimental results, authors are encouraged to make their data available with their submission. Submissions must be in PDF format and will be handled via easychair at the following address: https://easychair.org/conferences/?conf=gandalf23 <https://urldefense.com/v3/__https://easychair.org/conferences/?conf=gandalf…> Invited Speakers · Laure Daviaud <https://urldefense.com/v3/__https://www.city.ac.uk/about/people/academics/l…> – University of East Anglia (UK) · Juha Kontinen <https://urldefense.com/v3/__https://researchportal.helsinki.fi/en/persons/j…> – University of Helsinki (Finland) · Sophie Pinchinat <https://urldefense.com/v3/__https://people.irisa.fr/Sophie.Pinchinat/__;!!I…> – IRISA/University of Rennes (France) · Alexander Rabinovich <https://urldefense.com/v3/__http://www.cs.tau.ac.il/*rabinoa__;fg!!IBzWLUs!…> – Tel Aviv University (Israel) Program Committee · Dario Della Monica (co-chair) – University of Udine (Italy) · Antonis Achilleos (co-chair) – Reykjavik University (Iceland) · Parosh Aziz Abdulla – Uppsala University (Sweden) · Christel Baier – Technische Universität Dresden (Germany) · Valentina Castiglioni – Reykjavik University (Iceland) · Giorgio Delzanno – University of Genova (Italy) · Léo Exibard – Université Gustave Eiffel (France) · Gabriele Fici – University of Palermo (Italy) · Dana Fisman – Ben-Gurion University (Israel) · Nicola Gigante – Free University of Bozen-Bolzano (Italy) · Miika Hannula – University of Helsinki (Finland) · Naoki Kobayashi – The University of Tokyo (Japan) · Orna Kupferman – Hebrew University (Israel) · Martin Leucker – University of Lübeck (Germany) · Jakub Michaliszyn – University of Wrocław (Poland) · Fabio Mogavero – University of Napoli (Italy) · Shankara Narayanan Krishna – Indian Institute of Technology, Bombay (India) · Pawel Parys – University of Warsaw (Poland) · Guillermo Pérez – University of Antwerp (Belgium) · Giovanni Pighizzini – University of Milano (Italy) · Gabriele Puppis – University of Udine (Italy) · Joshua Sack – California State University Long Beach (USA) · Ocan Sankur – CNRS/Irisa (France) · Patrick Totzke – University of Liverpool (UK) · Jana Wagemaker – Reykjavik University (Iceland) · Matteo Zavatteri– University of Padova (Italy) · Martin Zimmermann – Aalborg University (Denmark) Steering Committee · Luca Aceto – Reykjavik University (Iceland) · Javier Esparza – University of Munich (Germany) · Salvatore La Torre – University of Salerno (Italy) · Angelo Montanari – University of Udine (Italy) · Mimmo Parente – University of Salerno (Italy) · Jean-François Raskin – Université libre de Bruxelles (Belgium) · Martin Zimmermann – Aalborg University (Denmark) Website https://gandalf23.uniud.it/ <https://urldefense.com/v3/__https://gandalf23.uniud.it/__;!!IBzWLUs!Rooz29B…>

1 0

CfP High-Performance Computing and Formal Methods: Deadline July 10th
by Rosemary Monahan 19 Jun '23

19 Jun '23

Call for papers: Frontiers in High Performance Computing Research topic: High-Performance Computing and Formal Methods Manuscript Submission: Deadline 10 July 2023 We welcome submissions of papers reporting both original research and case studies on algorithmic advances and the use of high-performance computing for scaling automated reasoning and application of formal methods in system verification and synthesis, and mathematical and logical foundations of parallel formal verification and synthesis algorithms including contributions discussing complexity and correctness guarantees of parallel algorithms. Topics of interest include (but are not limited to): - Algorithms and tools for verifying models and implementations; including model-checking, theorem proving, runtime verification, and decision procedures - Algorithms and tools for system synthesis; including software synthesis and reactive (discrete-time, timed, hybrid) synthesis - Mathematical and logical foundations of scalable formal verification and synthesis algorithms; including complexity analysis, correctness guarantees, and performance improvements - Case studies and experience reports on the use of high-performance computing in applying formal methods for system verification and synthesis. Frontiers in High Performance Computing is an open access journal, so publishing fees are applied to accepted articles. Please contact highperformancecomputing.submissions(a)frontiersin.org to discuss fees, institutional waivers, and discounts. For further information and submission guidelines see https://www.frontiersin.org/research-topics/50797/high-performance-computin… Regards, Kristin Yvonne Rozier, Iowa State University Rosemary Monahan, Maynooth University Rohit Dureja, IBM (United States) Professor Rosemary Monahan Principles of Programming Research Group Department of Computer Science & Hamilton Institute, Maynooth University, Maynooth, Co. Kildare, Ireland. T: +353 1 7083847 F:+353-1-7083848 W: https://www.maynoothuniversity.ie/computer-science/our-people/rosemary-mona…

1 0

Final Call for Participation: Logic Mentoring Workshop (LMW@LICS 2023)
by Ilina Stoilkovska 19 Jun '23

19 Jun '23

------------------------------------------------------------------------ *Final Call for Participation* Logic Mentoring Workshop (LMW@LICS 2023) Boston, USA June 25, 2023 https://logic-mentoring-workshop.github.io/lics23/ Co-located with Logic in Computer Science (LICS) 2023 Registration at https://lics.siglog.org/lics23/ ------------------------------------------------------------------------ The Logic Mentoring Workshop introduces young researchers to the technical and practical aspects of a career in logic research. It is targeted at students, from senior undergraduates to doctoral students, and will include tutorials and plenary talks as well as a panel discussion, where experienced researchers from the field answer career-related questions from the audience. The workshop will be a hybrid event, however on-site participation in Boston, USA, is highly recommended. It is co-located with Logic in Computer Science (LICS’23, https://lics.siglog.org/lics23/) one of the most prestigious conferences on the topic. Attending LICS is not a prerequisite to attend LMW, but it is encouraged. *LICS Buddy* Is this the first conference you will attend in person? We have all been there. You might not feel comfortable if you don't know anyone. Join our Buddy Program, and we will help you to get in touch with another mentoring workshop attendee. Every newcomer will be assigned either a more experienced peer or another newcomer, so you are not alone. For those who are not attending a conference for the first time, being a buddy is a way for you to help the community to grow and introduce less experienced students to the field. If you are interested, write an email to steffen.van.bergerem(a)hu-berlin.de. *PRELIMINARY PROGRAM* 09:00–09:30 Meet & greet 09:30–10:00 PROcrastination is not for amateurs. Sonia Marin (University of Birmingham) 10:00–10:30 What makes theoretical research interesting–relevant–exciting? Martin Grohe (RWTH Aachen University) 10:30–11:00 Coffee break 11:00–11:30 Antonina Kolokolova (Memorial University of Newfoundland) 11:30–12:00 Nobody knows anything. Mikołaj Bojańczyk (University of Warsaw) 12:00–12:30 Finding Tenure. Anupam Das (University of Birmingham) 12:30–14:00 Lunch break 14:00–14:30 Marianna Girlando (ILLC, University of Amsterdam) 14:30–15:00 Igor Walukiewicz (CNRS, Université de Bordeaux) 15:00–15:30 Alëna Rodionova (Waabi) 15:30–16:00 Coffee break 16:00–17:00 Panel: Anuj Dawar (University of Cambridge), Alëna Rodionova (Waabi), Igor Waluckiwicz (CNRS, Université de Bordeaux), and Matthew Weaver (Princeton University) *ORGANIZING COMMITTEE* Arthur Azevedo de Amorim Steffen van Bergerem Ilina Stoilkovska K. S. Thejaswini

1 0

CALL FOR NOMINATION - FSCD Steering Committee Membership Election
by Carsten Fuhs 12 Jun '23

12 Jun '23

Formal Structures for Computation and Deduction (FSCD) Steering Committee Membership Election 2023 CALL FOR NOMINATION The FSCD SC consists of the SC Chair, 6 elected members, PC Chairs of the last 3 years, the Publicity Chair, Workshop Chair and former SC Chair. Every year the outgoing elected SC members are replaced by new members elected by a secret ballot. Each SC member normally serves for 3 years, unless exceptions apply (see the FSCD Rules of Business http://fscd-conference.org/organization/rules-of-business/ for details). The current steering committee composition, together with the serving time for each member, is available here: https://fscd-conference.org/organization/steering-committee/ Candidates for SC membership are requested to email the FSCD SC Chair an election statement (including a brief bio) on one a4 page, preferably in PDF, no later than * Monday 26 June 2023 (AoE) * The election statements will be posted on the FSCD webpage before the start of FSCD 2023. The election will take place at the General Meeting of FSCD 2023, 3-6 July 2023. Herman Geuvers herman at cs.ru.nl FSCD SC Chair

1 0

The Decision Problem for Effective Procedures - Celebration of the
by jean-yves beziau 12 Jun '23

12 Jun '23

The Decision Problem for Effective Procedures - Celebration of the 120th anniversary of Alonzo Church Nathan Salmon (University of California at Santa Barbara), Gary Mar (State University of New York, Stony Brook), Melvin Fitting (CUNY Graduate Center) Logica Universalis Webinar 2023 --------------------------------------------------------------------------------------------------------------------- June 14, 2023 at 4pm CET (Paris-Geneva-Rome) we will have one more session of the Logica Universalis Webinar (LUW). Nathan Salmón will present his recently published paper in Logica Universalis "The Decision Problem for Effective Procedures" https://www.springer.com/journal/11787/ Salmón was a former PhD student of the famous logician and founder of computer science Alonzo Church. Church was born June 14, 1903. We will therefore commemorate his 120th anniversary with a preliminary presentation by his last PhD student Gary R.Mar. The chair of the session will be Melvin Fitting. Nathan Salmón was also a long time friend and collaborator of Saul Kripke: https://www.simplycharly.com/read/interviews/naming-names-a-deep-dive-into-… At LUW we have before the main talk the presentation of an association related to the author or/and topic of the talk. The Kripke center was presented at the LUW session of August 11, 2021: https://youtu.be/piyvWZ5nOik This next LUW session June 14 will initiate a series where the preliminary talk is related to the anniversary of a famous logician. This is not indeed completely new, considering that the first session of LUW was for the celebration of the World Logic Day, January 14, 2021, the 120th anniversary of Alfred Tarski: http://www.logica-universalis.org/wld3 Everybody is welcome to attend the next LUW session June 14, register here: https://www.springer.com/journal/11787/updates/23910922 Jean-Yves Beziau Editor-in-Chief Logica Universalis President of LUA (Logica Universalis Association) http://www.logica-universalis.org/LUAD

1 0