The first CADE I attended was CADE-10 in 1990, in Kaiserslautern, Germany. I was very very green in the ATP world, and completely in awe of the founders who were there: Alan Bundy, Wolfgang Bibel, Peter Andrews, Woody Bledsoe, and more. Bob Boyer and J Moore gave the keynote, and Woody gave the banquet talk. That’s when I really noticed Bob. The banquet was in a church with a high vaulted ceiling, and thus had awful acoustics. Woody was using one of those old projectors with plastic slides and a 6’x6’ screen. Woody never had a loud voice, and it was very hard to follow his talk. I was seated at the second to back table, and people were starting to chatter. In one of those coincidental moments when everyone stops talking, a loud voice called out from the table behind me: “Waiter, more red wine at this table!”. I turned around … it was Bob Boyer. I knew two things immediately: (i) Bob Boyer was my kind of guy, (ii) I was going to attend many more CADE conferences.
Early in February 2025 I went to Austin to visit Bob, to collect one of Larry Wos’ bowling balls, which Bob had won from Larry in a bet (it’s a whole other story). I had arranged with the CADE trustees that the ball was to become the prize for the Best Student Paper at CADE/IJCAR. Sadly Bob was ill when I visited, so Grant Passmore took me to visit Bob in the recuperation hospital. What a pleasure chatting with Bob, with his sharp mind and sharp wit. Warren Hunt dropped in too, so it was a grand time. The visit reminded me of the incident at CADE-10, so I told Bob the story! It was just one of many memorable moments at CADE/IJCAR conferences, prompting me to write down some of those memories. Thanks Bob for starting me off on this personal and intermittent history of “Memories of CADE”.
Looking back on what I have written, it feels horribly self-centred. Maybe so, and I hope it brings back some personal memories for others — write them down … I’ll read them!
We invite proposals for sites around the world to host the International Conference on Automated Deduction (CADE) to be held in summer 2027. CADE typically merges into IJCAR (the International Joint Conference on Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome.
The deadline for proposals is July 27 2025.
CADE's/IJCAR's recent location history is as follows:
The upcoming CADE/IJCAR events will be:
We encourage proposers to register their intention informally as soon as possible. We will try to do the final selection of the site within two months after the proposal deadline.
Proposals should address the following points that also represent criteria for evaluation:
Prospective organizers are encouraged to get in touch with the CADE Secretary and the CADE President for informal discussion, and to study the CADE management notes. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers are encouraged.
The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, choosing the Herbrand, Bill McCune, and Skolem Award selection committee, instituting new awards, etc.
Nominations for four CADE trustee positions are being sought, in preparation for the elections to be held after CADE-30.
The current members of the board of trustees are (in alphabetical order):
The terms of Pascal Fontaine, Jürgen Giesl, André Platzer, and Sophie Tourret end in 2025. Pascal Fontaine has served two consecutive terms and cannot be nominated again this year, whereas Jürgen Giesl, André Platzer, and Sophie Tourret may be nominated for a second term.
The term of office of Uwe Waldmann as CADE-30 programme chair ends after the CADE conference. As outgoing ex-officio trustee, Uwe Waldmann is eligible to be nominated as elected trustee.
In summary, we are seeking to elect four trustees.
Nominations can be made by any CADE member, either by e-mail or at the CADE business meeting at CADE-30; since nominators must be CADE members, they must have participated at at least one of the CADE or IJCAR conferences in the years 2022-2025. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. For further details please see the CADE Inc. bylaws at the CADE web site.
E-mail nominations can be provided up to the upcoming CADE business meeting, via email to
Philipp Rümmer, Secretary of CADE Inc.
Nominations are now invited for the 2025 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2024 and 31 December 2024 are eligible for nomination for the award.
The deadline for submission is July 1, 2025. Nominations should be submitted by the candidate or the supervisor via Easychair.
Please submit a pdf file containing:
The 2025 Ackermann award will be presented to the recipient(s) at CSL 2026.
The award consists of a certificate, an invitation to present the thesis at the CSL conference, the publication of the laudatio in the CSL proceedings and financial support to attend the conference.
The jury consists of:
For more information please contact Maribel Fernandez.
The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work on ACL2 and the other theorem provers in the Boyer-Moore family.
The 2025 ACL2 Workshop will be held in Austin, Texas, USA and online. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend. An invited keynote talk will be given by Swarat Chaudhuri (University of Texas at Austin), "Scaling Formal Verification with Machine Learning"; a second invited keynote talk is anticipated. See the above website for accepted papers as well as updates, which will include a program with details on a pre-workshop reception on May 11 and a banquet on May 12.
More information is available on the workshop's web page.
The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed.
Attending a conference such as LICS can be a transformative experience. It exposes participants to cutting-edge research and can open up new research avenues and collaboration opportunities. 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.
Students (undergrad, master's, and PhD alike) can apply to have their costs (some or all) covered by our sponsors, the National Science Foundation (NSF) and Jane Street. Application deadline is May 10, 2025 (applications are accepted after that date if funds allow). Please apply by filling out this form.
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. We will have a Buddy Program, where 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.
More information is available on the workshop's web page.
The Dutch Formal Methods Day is a full-day event dedicated to formal methods in the Netherlands. This event is an opportunity for people in academia, industry, and education who are interested in formal methods, in the broadest sense, to come together, learn, and network. There will be numerous talks, giving a broad overview formal methods in the Netherlands. Upon registering, you will have the opportunity to offer a talk.
Coffee and lunch will be provided; there will be ample opportunity for networking with your colleagues and meeting new people. Experts and newcomers to the field are equally welcome. All the talks will be given in English.
Important Dates (AoE):
More information is available on the workshop's web page.
Knowledge Representation and Reasoning (KR) is a well-established and vibrant field of research within Artificial Intelligence. KR builds on the fundamental thesis that knowledge can often be represented in an explicit declarative form, suitable for processing by dedicated symbolic reasoning engines. This enables the exploitation of knowledge that would otherwise be implicit through semantically grounded inference mechanisms. KR has contributed to the theory and practice of various areas of AI, including agents, automated planning, robotics, and natural language processing, and to fields beyond AI, including data management, semantic web, verification, software engineering, computational biology, and cybersecurity.
The KR conference series is the leading forum for timely, in-depth presentation of progress in the theory and practice of the representation and computational management of knowledge.
KR 2025 will include three special thematic tracks, a Recently Published Research Track, tutorials, workshops, and a Doctoral Consortium. Details about all these events and the corresponding calls can be found on the website.
For the main track, we solicit papers presenting novel results on the principles of KR, which clearly contribute to the formal foundations of the field or show the applicability of KR techniques to implemented or implementable systems. We welcome papers from other areas that demonstrate clear use of, or contributions to, the principles or practice of KR. We also encourage "reports from the field" of applications, experiments, developments, and tests.
Important Dates (AoE):
As a complement to the traditional KR Main track focusing more on theoretical advances in KR, the KR in the Wild track aims to showcase successful deployments of KR formalisms in all types of application domains as well as recent developments in the state-of-the-art in automated reasoning systems which form the basis for successful deployment of declarative problem solving in an ever-increasing number of practical settings.
Towards these goals, the KR in the Wild Track welcomes contributions from areas that are sometimes considered as not core KR research. This includes (but is not restricted to) state-of-the-art reasoning systems and solvers developed in the various vibrant declarative programming communities as well as insightful applications of such systems. As further goals, the track aims to foster interactions between practical and theoretical advances, and to encourage the discussion of new ideas, research experiences, emerging results and open challenges that can inspire novel research directions and influence the future of KR research.
We invite submissions of papers on all aspects of the development, deployment, and evaluation of KR tools and techniques to solve application problems, including:
Important Dates (AoE):
More information is available on the conference's web page.
FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis. The first FroCoS symposium was held in Munich, Germany, in 1996. Initially held every two years, since 2004 it has been organized annually with alternate years forming part of IJCAR.
FroCoS 2025 will be hosted by the theoretical computer science lab of Reykjavik University, collocating with the 16th International Conference on Interactive Theorem Proving (ITP 2025) and with the 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2025). The three conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions.
In various areas of computer science, such as logic, computation, program development and verification, artificial intelligence, knowledge representation, and automated reasoning, there is an obvious need for using specialized formalisms and inference systems for selected tasks. To be usable in practice, these specialized systems must be combined with each other and integrated into general purpose systems. This has led to the development of techniques and methods for the combination and integration of dedicated formal systems, as well as for their modularization and analysis.
FroCoS traditionally focuses on these types of research questions and activities. Like its predecessors, FroCoS 2025 seeks to offer a common forum for research in the general area of combination, modularization, and integration of systems, with emphasis on logic-based methods and their practical use. Topics of interest for FroCoS 2025 include (but are not restricted to):
Important Dates (AoE):
More information is available on the conference's web page.
The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions to logic-based program development in any programming language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress.
Topics of interest include all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large, including, but not limited to:
Important Dates (AoE):
More information is available on the conference's web page.
The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) brings together researchers interested in all aspects - theoretical foundations, implementation techniques, systems development and applications - of the mechanization of reasoning with tableaux and related methods.
Topics of interest include (but are not restricted to):
Important Dates (AoE)
More information is available on the conference's web page.
Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.
Areas of interest include (but are not limited to):
There will be several focused sessions on AI for ATP, ITP, mathematics, relations to general AI (AGI), Formal Abstracts, linguistic processing of mathematics/science, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. AITP'25 is planned as an in-person conference.
Important Dates (AoE):
More information is available on the conference's web page.
The PPDP 2025 symposium brings together researchers from the declarative programming communities, including those working in the functional, logic, answer-set, and constraint handling programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for analyzing, performing, specifying, and reasoning about computations, including mechanisms for concurrency, security, static analysis, and verification.
Submissions are invited on all topics related to declarative programming, from principles to practice, from foundations to applications. Topics of interest include, but are not limited to:
Important Dates (AoE):
More information is available on the conference's web page.
The COST action EuroProofNet organizes in September a symposium at the Institut Pascal, Orsay, France, with various great events:
Important Dates (AoE):
More information is available on the symposium's web page.
The aim of the symposium is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The symposium covers an ample spectrum of themes, ranging from theory to applications, and encourages 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:
Important Dates (AoE):
More information is available on the conference's web page.
In the last decades, we have witnessed a proliferation of approaches that integrate several modelling, verification and simulation techniques, facilitating more versatile and efficient analysis of software-intensive systems. These approaches provide powerful support for the analysis of different functional and non-functional properties of the systems, complex interaction of components of different nature as well as validation of diverse aspects of system behaviour. The iFM conference series is a forum for discussing recent research advances in the development of integrated approaches to formal modelling and analysis. The conference covers all aspects of the design of integrated techniques, including language design, verification and validation, automated tool support and the use of such techniques in software engineering practice. To credit the effort of tool developers, we use EAPLS artifact badging.
Areas of interest include (but are not limited to):
Important Dates (AoE):
The 7th International Workshop on Formal Methods for Autonomous Systems and the iFM PhD Symposium will be co-located with iFM 2025.
More information is available on the conference's web page.
The Working Formal Methods Symposium (FROM) aims to bring together researchers and practitioners working 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 includes invited lectures and regular contributions.
Areas of interest include (but are not limited to):
Important Dates (AoE):
More information is available on the symposium's web page.
The IEEE International Conference on Tools with Artificial Intelligence (ICTAI) is a leading IEEE-CS annual scientific meeting for more than three decades. It provides a major international forum where the creation and exchange of ideas related to artificial intelligence are fostered among academia, industry, and government agencies. The conference facilitates the cross-fertilization of these ideas and promotes their transfer into practical tools, for developing intelligent systems and pursuing artificial intelligence applications. The ICTAI encompasses all technical aspects of specifying, developing and evaluating the theoretical underpinnings and applied mechanisms of the AI-based components such as algorithms, architectures and languages.
Topics include (but not limited to):
Important Dates (AoE):
More information is available on the conference's web page.
The Polish Association of Logic and Philosophy of Science is organizing the Polish Congress of Logic, which will take place on September 22–26, 2025, at the Nicolaus Copernicus University in Toruń.
The conference aims to honour the legacy of outstanding Polish logicians, particularly those associated with the Lvov-Warsaw School and the Polish Mathematical School. The conference focuses on topics from various areas of logic and its applications, in particular, in the foundations of mathematics, computer science and linguistics. Submissions in the area of philosophy of science are also welcomed.
The Congress will feature plenary sessions, sections, and the following workshops:
We are pleased to announce the panel discussion “Logic in the Development of Artificial Intelligence”, which will take place during the Congress.
Submissions should be prepared using the provided latex template and sent by email. For workshop submissions, please include the workshop name in the email subject line. For regular submissions, please select relevant tags (at most three) from the list below:
Important Dates (AoE):
More information is available on the conference's web page.
The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation.
The Verified Software Initiative (VSI), spearheaded by Tony Hoare and Jayadev Misra, is an ambitious research program for making large-scale verified software a practical reality. The International Conference on Verified Software: Theories, Tools and Experiments (VSTTE) is the main forum for advancing the initiative. VSTTE brings together experts spanning the spectrum of software verification in order to foster international collaboration on the critical research challenges. The theoretical work includes semantic foundations and logics for specification and verification, and verification algorithms and methodologies. The tools cover specification and annotation languages, program analyzers, model checkers, interactive verifiers and proof checkers, automated theorem provers and SAT/SMT solvers, and integrated verification environments. The experimental work drives the research agenda for theory and tools by taking on significant specification/verification exercises covering hardware, operating systems, compilers, computer security, parallel computing, and cyber-physical systems.
VSTTE 2025 welcomes submissions describing significant advances in the production of verified software, i.e. software that has been proved to meet its functional specifications. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We also welcome papers describing novel experiments and case studies evaluating verification techniques and technologies.
In addition to regular papers, we welcome submissions on in-progress verified software projects to a “work-in-progress (presentation-only)” track. Work-in-progress contributions will not appear in the post-proceedings of the conference. Submissions describing work of interest to the software verification community, but that could not be accepted for publication in the conference proceedings, may be invited to the “work-in-progress (presentation-only)” track, on a case-by-case basis.
Topics of interest for this conference include, but are not limited to:
Important Dates (AoE):
More information is available on the conference's web page.
FM 2026 is the 27th international symposium on Formal Methods in a series organized by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The FM symposia have been successful in bringing together researchers and industrial users around a program of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral research. FM 2026 will be both an occasion to celebrate and a platform for enthusiastic researchers and practitioners from a diversity of backgrounds to exchange their ideas and share their experiences.
FM 2026 will highlight the development and application of formal methods in a wide range of domains including:
Important Dates (AoE):
FM 2026 features a special track on Tests and Proofs (TAP) as a part of the conference.
TAP promotes research in verification and formal methods that targets the interplay of static and dynamic analysis techniques with the ultimate goal of improving software and system dependability.
Research in verification has seen an increase in heterogeneous techniques and a synergy between the traditionally distinct areas of dynamic and static analysis. There is growing awareness that dynamic techniques such as testing and static techniques such as proving are complementary rather than mutually exclusive. Notable examples that provide evidence for the potential of a combination of static and dynamic analysis are counterexample generation based on symbolic execution, the integration of SAT/SMT-solving in model checking, or the combination of predicate abstraction with exhaustive enumeration. The verification of systems based on machine learning spurs novel combinations of dynamic and static analyses, e.g., property verification of surrogate models that are generated through testing.
TAP's scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Topics of interest center around the combination of static techniques such as proving and dynamic techniques such as testing.
More information is available on the conference's web page.
GALOP is an international workshop on formal models for program interaction. It has a broad interest, in both the foundational aspects of these models as well as their practical applications.
The central focus of GALOP is game semantics, a set of techniques used to represent the interaction of a program and its environment as a formal game. This is a powerful framework for reasoning about programs and interactive systems, and game semantics is relevant to many aspects of programming language theory. Game semantics also has deep connections to logic and other fields of mathematics.
GALOP aims to gather researchers with a range of expertise who share an interest in reasoning about the interactive behaviour of programs using formal mathematical methods, in any context including proof theory, denotational semantics, or program verification. Specific areas of interest include, but are not limited to:
Important Dates (AoE):
More information is available on the workshop's web page.
UNIF 2025 is the 39th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of making two given terms equal, either syntactically or modulo an equational theory. It is a fundamental process used in various areas of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, knowledge representation, types, etc.
The International Workshop on Unification (UNIF) is a forum for researchers in unification theory and related fields to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for students, young researchers and scientists working in related areas to get an overview of the current state of the art in unification theory.
A non-exhaustive list of topics of interest includes:
Important Dates (AoE):
More information is available on the workshop's web page.
Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation, and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems, have been the focus of considerable research over the past three decades.
The annual LFMTP workshop brings together designers, implementors, and practitioners to discuss various aspects of the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques, and qualitative aspects of reasoning including expressivity and lucidity.
LFMTP 2025 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
Important Dates (AoE):
More information is available on the workshop's web page.
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of a new software generation and to discuss existing systems.
Topics of interest include:
Important Dates (AoE):
More information is available on the workshop's web page.
This workshop aims at providing a forum for the general area of Knowledge Representation and Reasoning (KR), which is a well-established and active area of research within Artificial Intelligence. KR is about the declarative representation of knowledge and develops methods for automated reasoning under vagueness, uncertainty, incompleteness, and inconsistency.
We welcome contributions from all areas of KR, in particular including the following topics:
Important Dates (AoE):
More information is available on the workshop's web page.
The aim of WPTE is to bring together researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.
Topics of interest include but are not limited to:
Important Dates (AoE):
More information is available on the workshop's web page.
The aim of the Pragmatics of SAT (PoS) workshop series is to provide a venue for researchers working on designing and/or applying Boolean satisfiability (SAT) solvers and related solver technologies, including but not restricting to satisfiability modulo theories (SMT), answer set programming (ASP), and constraint programming (CP) as well as their optimization counterparts, to meet, communicate, and discuss latest results.
Topics of interest include but are not limited to:
Important Dates (AoE):
More information is available on the workshop's web page.
Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and combination methods that allow one to obtain more versatile SMT tools. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification efforts.
The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to:
Important Dates (AoE):
More information is available on the workshop's web page.
HOR is a forum to present work concerning all aspects of higher-order rewriting. The aim is to provide an informal and friendly setting to discuss recent work and work in progress concerning higher-order rewriting, broadly construed. This includes rewriting systems that have functional variables or bound variables, the lambda-calculus and combinatory logic being paradigmatic examples.
The following is a non-exhaustive list of topics for the workshop:
Important Dates (AoE):
More information is available on the workshop's web page.
Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses.
This series of workshops aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis.
Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences.
Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:
Important Dates (AoE):
HCVS 2025 is planning to host the 8th competition on constraint Horn clauses (CHC-COMP), which will compare state-of-the-art tools for CHC solving for performance and effectiveness on a set of publicly available benchmarks.
More information is available on the workshop's web page.
Symbolic Computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions.
The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces for tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop is to provide an opportunity to discuss, share knowledge and experience across both communities.
The workshop series has emerged from an H2020 FETOPEN CSA project "SC-Square", which ran from 2016 to 2018. It has been continued aiming at building bridges between Satisfiability Checking and Symbolic Computation. It is open for submission and participation to everyone interested in the topics, whether or not they were members or associates of the original project.
The topics of interest include but are not limited to:
Important Dates (AoE):
More information is available on the workshop's web page.
Linear Logic is not only a proof theoretical tool to analyze or control the use of resources in logic and computation. It is also a corpus of tools, approaches, and methodologies (proof nets, exponential decomposition, geometry of interaction, coherent spaces, relational models, etc.) that, even if developed for studying Linear Logic syntax and semantics, have been applied in several other fields (analysis of lambda-calculus computations, game semantics, computational complexity, program verification, etc.)
The TLLA international workshop aims at bringing together researchers working on Linear Logic or applying it or its tools. The main goal is to present and discuss trends in the research on Linear Logic and its applications by means of tutorials, invited talks, open discussions, and contributed talks.
The purpose is to gather researchers interested in the connections between Linear Logic and various topics such as:
Important Dates (AoE):
More information is available on the workshop's web page.
We invite you to contribute to Weidenbach'60, a workshop in celebration of Prof. Christoph Weidenbach's 60th birthday.
Christoph is the leader of the Automation of Logic group at Max-Planck-Institut für Informatik, Saarbrucken. He is a well-known figure in the automated reasoning community, a former president of CADE Inc, and the main developer of the automatic prover SPASS.
We invite contributions in areas close to Christoph's research, including but not limited to:
Important Dates (AoE):
More information is available on the workshop's web page.
The Description Logic workshop is the major annual event of the Description Logic research community. It is the forum in which those interested in description logics, both from academia and industry, meet to discuss ideas, share information, and compare experiences.
We invite contributions on all aspects of description logics, including, but not limited to:
Important Dates (AoE):
More information is available on the workshop's web page.
RADICAL proposes a workshop aligned within the intersection between concurrency and logic, broadly construed. Admittedly broad, such an intersection has been explored from very diverse angles for many years now. More recently, the interplay of concurrency and logic with areas/applications such as, for instance:
As an unfortunate side effect, however, the important unifying role that concurrency plays in all of them seems hard to find in a single scientific event. Indeed, there do not seem to exist appropriate venues in which different research communities interested in concurrency and logic can meet closely, cross-fertilize, and share their most exciting recent results. RADICAL intends to fill a gap between CONCUR researchers that now also typically publish and interact in other different venues; it also aims at attracting researchers from neighboring communities whose work naturally intersects with CONCUR.
Important Dates (AoE):
More information is available on the workshop's web page.
Building on the ideas of Floyd-Hoare logic, dynamic logic was introduced in the 70's as a formal tool for reasoning about, and verify, classic imperative programs. Over time, its aim has evolved and expanded; DL can be seen now as a general set of ideas and tools devised for representing, describing and reasoning about diverse kind of actions, including (but not limited to) frameworks tailored for specific programming problems/ paradigms (e.g., separation logics), settings for modelling new computing domains (e.g., probabilistic, continuous and quantum computation), frameworks for reasoning about information dynamics (e.g., dynamic epistemic logics) and systems for reasoning about long term information dynamics (e.g., learning theory).
Both its theoretical relevance and practical potential make DLs a topic of interest in a number of scientific venues, from wide-scope software engineering conferences to modal logic specific events. The aim of the DaLí 2025 workshop is to bring together, in a single place, researchers with a shared interest in the formal study of actions (from Academia to Industry and more, from Mathematics to Computer Science and beyond) to present their work, foster discussions and encourage collaborations.
Submissions are invited on the general field of dynamic logic, its variants and applications, including (but not restricted to):
Important Dates (AoE):
More information is available on the workshop's web page.
The 21st Doctoral Consortium (DC) on Logic Programming provides students with the opportunity to present and discuss their research directions, and to obtain feedback from both peers and experts in the field. The DC will take place during the 41st International Conference on Logic Programming (ICLP), hosted by the University of Calabria, Italy. The best paper from the DC will be given the opportunity to make a presentation in a session of the main ICLP conference.
The DC is designed for students currently enrolled in a Ph.D. program, though we are also open to exceptions (e.g., students currently in a Master's program and interested in doctoral studies). Students at any stage in their doctoral studies are encouraged to apply for participation in the DC. Applicants are expected to conduct research in areas related to logic and constraint programming.
Topics of interest include (but are not limited to):
Important Dates (AoE):
More information is available on the consortium's web page.
The Women in Logic workshop (WiL) provides an opportunity to increase awareness of the valuable contributions made by women in the area of logic in computer science. Its main purpose is to promote the excellent research done by women, with the ultimate goal of increasing their visibility and representation in the community. Our aim is to:
Topics of interest include but are not limited to:
Important Dates (AoE):
More information is available on the workshop's web page.
The TPTP Tea Party (TPTPTP) brings together developers and users of the TPTP World, including (but not limited to):
The meeting aims to elicit feedback, suggestions, criticisms, etc, of these resources, in order to ensure that their continued development of the TPTP World meets the needs of successful automated reasoning. The 2025 TPTPTP will focus on "Representation, Verification, and Visualization of TPTP Format Proofs and Models" (but other topics might sneak in).
More information is available on the workshop's web page.
The EuroProofNet School on Natural Theorem Proving will be held from the 3rd to the 5th of June 2025 at the Mathematics Centre in Bonn, Germany. The programme will include talks on topics related to natural formal mathematics and hands-on tutorials. Related topics include:
The school is free of charge, but registration is required.
More information is available on the school's web page.
The Marktoberdorf Summer School is a 10-day event for young computer scientists and mathematicians, typically doctoral and postdoctoral researchers. It provides mini-courses on state-of-the-art topics in specification and verification and leaves ample room for interaction between participants and speakers.
Cybersecurity has become of fundamental importance for society. Today, computer systems are part of almost every artifact, from connected social media platforms to autonomous cars, internet commerces, or power plants. While the explosion in applications of computer systems leads to great increases in productivity and wealth, there are increasingly many scenarios showcasing that our complex cyberspace is not secure: software crashes, data breaches, and security vulnerabilities have become a fact of our daily life. Ensuring a secure cyberspace requires a multidisciplinary approach to specifying and verifying existing infrastructures. Computer science has therefore emerged into a social discipline, continuously developing new technologies for (dis)proving system security and examining user privacy, mechanically and efficiently.
Since 1970 the Marktoberdorf Summer School has attracted the best researchers on cybersecurity in the world. The Marktoberdorf Summer School 2025 will focus on presenting the latest developments toward the specification and verification of secure cyberspaces. The summer school will feature 12 courses by top researchers in the area.
The registration deadline is May 5, 2025
More information is available on the school's web page.
The European Summer School in Logic, Language and Information (ESSLLI) is a yearly recurring event, organized under the auspices of the Association for Logic, Language and Information (FoLLI), and has been running since 1989. The ESSLLI Summer School provides an interdisciplinary setting in which courses and workshops are offered in logic, linguistics and computer science, also from wider scientific, historical, and philosophical perspectives.
ESSLLI attracts around 400 participants from Europe, the Middle East, Asia and Africa, as well as from North America and Latin America. ESSLLI has become the main meeting place for young researchers and students in logic, linguistics and computer science to discuss current research and to share knowledge. The event is unique in its interdisciplinary set-up, with no equivalents in Europe.
The early-registration deadline is May 31, 2025.
More information is available on the school's web page.
The Vrije Universiteit Brussel and KU Leuven are pleased to announce their 4th Summer School on Security Testing and Verification. It is aimed at researchers and PhD students who are interested in the fields of:
The early-registration deadline is May 31, 2025.
More information is available on the school's web page.
European Summer School on Artificial Intelligence (ESSAI) intends to serve as a central hub for PhD students and young researchers working in all aspects of AI. The ESSAI Summer School covers one week of courses in the summer, at different sites around Europe, for both beginning and advanced students, and junior and senior researchers. ESSAI provides introductory and advanced courses in all areas of AI, emphasizing topics that allow students to gain a broad view of AI and understand connections between subdisciplines. ESSAI also offers several social activities for students and researchers alike. One of the tracks of ESSAI consists of advanced tutorials on a specific subject and corresponds to the traditional ACAI school organized by EurAI since 1989.
The ESSAI 2025 will offer an intensive 5-day program featuring various AI courses and tutorials. With over 30 lecturers from multiple fields, participants will have the opportunity to engage in 5+ parallel tracks of sessions each day. Mornings will include two courses, followed by a course and tutorial in the afternoon, ensuring comprehensive exposure to cutting-edge topics in AI.
Regular registration remains open until June 28, 2025, or until tickets sell out (whichever comes first).
More information is available on the school's web page.
The school is open to PhD students and early career researchers. Women and anyone currently underrepresented in the field of Computer Science are especially welcome to apply. You can register by completing this short form
The school has a focus on the theory and practice of verification, and students can expect talks and tutorials on the theory of verification, (e.g., Program Synthesis, Algebraic effects, Advanced theorem proving, Model checking, and Functional programming) and the use of industrial strength tools. You can find this year programme here and see the kind of talks we offer on this page with details of previous editions of the School.
We want to make the school as inclusive as we can, and we will cover the registration fee and accommodation of all accepted participants. Breakfast, lunches and refreshments for the three days will also be covered, as well as one evening meal. Regrettably, travel to and from the summer school is not included with the registration and we would expect supervisors or institutions to cover this. If you are not able to secure travel support to attend the conference, please let us know, as there may be some travel grants available.
The number of students attending the Summer School is limited and previous editions have been oversubscribed, we encourage you to apply early.
More information is available on the school's web page.
We are pleased to invite submissions to our upcoming collection for Discover Networks (A Springer Nature Journal) focusing on "Bridging Formal Verification and Neural Networks: Ensuring Reliable Networked Systems," which explores advancements in the formal verification of networks and the use of neural networks to optimize verification processes.
This collection aims to bring together cutting-edge research at the intersection of formal verification methods and networked systems, spanning a broad range of applications and approaches. The scope of this collection includes, but is not limited to, the formal verification of networks particularly in the context of safety-critical systems. We also seek innovative methods and techniques that leverage neural networks and machine learning to optimize and accelerate the formal verification process. Hybrid approaches that combine symbolic methods, model checking, and neural network-based strategies are of particular interest.
This collection welcomes original research and review articles in the following areas:
Important Dates (AoE):
More information is available on the journal's web page.
The 2025 pseudo-Boolean competition is organized as a special event of the SAT 2025 conference. The goal is to assess the state of the art in the field of pseudo-Boolean solvers, in the same spirit as the previous competitions and evaluations
We encourage the submission of any kind of pseudo-Boolean solver (complete or incomplete solvers, sequential or parallel, working on linear or non-linear constraints, etc.). There are a few simple requirements to ensure that a submitted solver will correctly operate in the competition environment. It is expected that any pseudo-Boolean solver can be easily modified to conform to these requirements. People interested in submitting a solver can contact the organizers to get some help.
Benchmarks may be submitted in any reasonable format. The organizers will do their best to translate the submitted benchmarks to the input format adopted for the competition. A benchmark submitted in the format of the competition will still be normalized to ensure consistency among all the input files. We would particularly appreciate the submission of:
Important Dates (AoE):
More information is available on the competition's web page.
The Chair of Theoretical Computer Science and Theorem Proving at Ludwig-Maximilians-Universität (LMU) München has an open postdoc position related to the use or development of automatic or interactive theorem provers. The chair includes specialists in theorem proving (including Isabelle), formalized mathematics, type theory, programming languages, and other areas of theoretical computer science.
We seek strong candidates with expertise in theorem proving and who are willing to pursue their own research agenda aligned with the chair's research. The position is available for three years and is open now. The start date can be negotiated. To apply, please send the following to me:
For further details, please contact Jasmin Blanchette.
The candidate will be part of the collaborative project SAIF, “Safe AI through Formal methods”, that involves renowned research labs in CS : Inria, CEA-List, LIX, LaBRI, LMF.
The objective of this PhD is to explore the way various NN-based architectures manage to approximate formal languages, i.e. learn surrogate automata from their traces. Beyond well established results on the expressive power of these models, the focus will be on the capabilities of the pair model + learning algorithm. Several authors have shown that almost discrete behaviors emerge naturally when NN are trained by automata traces, despite their definition as continuous state space systems, whence the name "soft automata." Another objective will be to assess the robustness and reliability of such NN-based models as automata approximators, by means of appropriate formal methods.
Several research directions are envisioned, that will be adapted to the skills and wishes of the candidate. We mention some of them below.
Further details can be found here.
The Technical University of Munich (TUM) invites applications for an Associate or Full Professor position in Logic and Verification in Computer Science, to begin as soon as possible.
TUM seeks to appoint an expert with significant contributions to one or more of the following areas:
Application deadline is May 31, 2025.
Further details can be found here.
We are seeking a highly motivated PhD student to work on formal verification of security mechanisms against fault-injection attacks. This PhD is part of the TwinSec national research project and a collaboration between CentraleSupélec and CEA, focusing on hardware/software security.
Research Areas:
Required Skills/Interests:
Starting date is before the end of 2025 (possibility of a Master’s internship before the PhD).
Further details can be found here.
Successful applicants will work on exciting projects at the intersection of security and artificial intelligence with Automated Reasoning at the core. Each doctoral students will be working with and will be supervised by two faculty members who are internationally renowned experts in their respective fields.
The doctoral college is designed to educate the next generation of experts on Automated Reasoning. It targets foundational questions such as rigorously defining the notion of safety and security across domains and applications, the development of automated techniques and analyses to ensure safety and security of electronic systems, and explores synergies between the fields of security and artificial intelligence.
TU Wien is located in the heart of Vienna, Austria, which has been repeatedly ranked as one of the most liveable city. The Faculty of Informatics is home to world-renowned researchers in a wide range of Areas including Logic and Computation, Information Systems Engineering, Computer Engineering, and Visual Computing and Human-Centered Technology. Numerous initiatives such as the Cybersecurity Center and the Center for Artificial Intelligence and Machine Learning demonstrate the Faculty's strong focus on collaboration and interdisciplinarity.
Application deadline is May 18, 2025. Successful applicants are expected to start in October 2025 (or soon after) and will receive funding for up to 4 years.
Further details can be found here.
The Ph.D. Programme in Computer Science of the GSSI aims to provide students with the main results, theories, techniques and methodologies regarding algorithms, models, languages, software and services to cope successfully with the challenges of the present and future Information and Communication Technology.
The deadline for applications is May 30, 2025. Further details can be found here.
The student will work on the project "Symbolic Reactive Synthesis on Planning Domains” with Professor Nir Piterman. The student will join the formal methods unit, with currently 6 active PhD students. This position is supported by WASP (Wallenberg AI, Autonomous Systems, and Software Program) alongside 4 other positions to work with my colleagues Fredrik Johansson (Machine Learning), Hazem Torfah (Autonomous Systems), Gregory Gay (Software Testing), and Muoi Tran (Secure Networks).
Research scope: formal methods, reactive synthesis, planning, automata, games, temporal logics.
The successful candidate will work on the project “Symbolic Reactive Synthesis on Planning Domains”. Reactive synthesis - automatic production of programs from high-level descriptions of their desired behavior - is emerging as a viable tool for the development of robots and reactive software. In high level, this is like telling a robot what you would like it to do and automatically planning how to do it. Planning domain description language (PDDL) is a standard language used to specify planning problems and domains in artificial intelligence. It provides a way to define objects, actions, and goals for automated planning systems to solve complex tasks. The project will seek to combine usage of PDDL in reactive synthesis. This will include both theoretical and practical contributions.
More concretely, the work will include the study of temporal logic, planning domains and planning techniques, automata, and two player games. Temporal logic and planning domains are used for describing in a high level the required behavior of a program, planning techniques are used to extract information about the problem, automata are used as an algorithmic tool for manipulation of logic formulae, and two-player games enable to consider strategies and programs. We will study these formalisms, analyze their properties, devise algorithms to manipulate and translate between them, as well as implement tools that will show the applicability of the developed techniques.
The aim of the doctoral (third-cycle) education is to acquire the knowledge and skills necessary to conduct independent research within computer science, and to contribute to the development of knowledge by writing a scholarly thesis.
PhD (third-cycle) education is through a fixed-term employment contract for 5 years. During these 5 years, most of the student’s time will be devoted to their research. They will also be assisting the department’s education by working 20% of their time on a teaching or supporting role. The 20% support component may be concentrated in certain parts of the year according to department’s needs (in consultation with the student). In addition, the student will have to undertake 60 Higher Education Credits (HECs) in courses enriching their knowledge in computer science, supporting their research, and gaining general (scientific) skills.
This project is supported by WASP and the appointed student will also belong to the WASP graduate school. Some of the required HECs will be specialized WASP courses about autonomous systems and AI. The appointed student will also be eligible to participate in other WASP supported programs (such as visits to universities abroad or short-term research visits to other universities).
The deadline for applications is May 15, 2025. Further details can be found here.
CEA List’s offices are located at the heart of Université Paris-Saclay, the largest European cluster of public and private research. Within CEA List, the Software Safety and Security Lab has an ambitious goal: help designers, developers and validation experts ship high-confidence systems and software.
This PhD will be a collaboration between CEA List and Université d’Orléans in the context of a recently accepted research project. Therefore, the PhD student will also be a member of the Languages, Modeling, Verification (LMV) team of LIFO, the Laboratory of Fundamental Computer Science in Orléans, Université d’Orléans. The overall objective of the LMV team is to advance the reliability and security of software, particularly in the context of the Internet of Things (IoT). We aim to ensure that the software involved satisfies critical properties either by construction by leveraging the design of libraries and programming languages, or by using formal methods.
The goal of the PhD consists in designing, formalizing, implementing, and proving correct new solutions for runtime checking of as many multi-state properties as possible. Currently, for the at construct, the state-of-the-art solutions for languages in which the size of any allocated blocks is statically known require to copy large pieces of program memory, which is not efficient. For languages in which the size of allocated block is not necessarily statically known, such as C, an equivalent solution would require to copy the whole program memory, which is not reasonable. In such a context, a solution might consist in including a static analysis that would approximate soundly the memory locations that would be copied at runtime. There is currently no solution for multi-state function/predicate calls.
The designed solution will be implemented in E-ACSL and experimented in concrete use cases. In particular, supporting such constructs is required to support runtime verification of MetAcsl’s high-level properties, such as confidentiality and integrity properties. Among others, Thales uses MetAcsl to verify security properties of smard card’s virtual machine: this PhD thesis would help Thales to include E-ACSL in its verification toolchain.
The formalization work and the proof of soundness will be done on a subset of C and ACSL, including the key constructs. Optionnally, they could be done within a proof assistant, such as Coq.
Knowledge in the following fields is appreciated:
This position will be filled as soon as possible; yet a 3+-month procedure for administrative and security purposes is required. In order to appky, please contact Jan Rochel, Julien Signoles and Frédéric Loulergue, and join a detailed CV, and a motivation letter.
Further details can be found here.
We invite candidates for multiple PhD student positions (graduate researchers) to start in 2025 in Melbourne. The research group focuses on automated reasoning, formal proof, and learning-assisted proof guidance and advice.
A background in formal proof, machine learning, or automated reasoning is an advantage. Candidates for a PhD position must hold a MSc or BSc with Honors in computer science or mathematics.
The city of Melbourne, consistently ranked as one of the world's most livable cities, is nicely located along the Yarra River and the beautiful coastline of Port Phillip Bay. The combination of urban culture and accessible natural landscapes, from pristine beaches to scenic parks, offers an exceptional quality of life. The University of Melbourne is renowned for its academic excellence and is regularly ranked as one of the best in the world.
For more information about the PhD positions can be found on this page and this page.
More information about the research topics can be found on this page and this page.
Please contact Cezary Kaliszyk for further information.
A PhD position available on automated reasoning for knowledge representation. In this project we will investigate new practical algorithms for a problem called interpolation. The results of the project will have applications in ontology engineering, logic-based machine learning and explainable AI. Applicants should have an interest in automated reasoning, computational logic or knowledge representation. Programming experience could be an advantage as well.
The project will be supervised by Patrick Koopmann and Stefan Schlobach, in the Knowledge in Artificial Intelligence group at the Vrije Universiteit Amsterdam. Submission deadline is 23 May. Also students who have not submitted their Master thesis yet can apply, provided that they submit their thesis by September. The project is planned to start in September, with some flexibility.
Further information can be found on this website. For questions, please contact Patrick Koopmann.