Association for Automated Reasoning

Newsletter No. 146
January 2025

Herbrand Award 2025: Call for Nominations

Philipp Rümmer
Secretary of CADE Inc.
On behalf of the CADE Inc. Board of Trustees

Call for Nominations

The Herbrand Award for Distinguished Contributions to Automated Reasoning is the award established by CADE Inc. to honour a person or group of people for their exceptional work in the field of Automated Deduction. The award is named after the french mathematician Jacques Herbrand, and is given out annually at the respective CADE or IJCAR conference.

The Herbrand Award has been given in the past to:

  • Larry Wos (1992)
  • Woody Bledsoe (1994)
  • Alan Robinson (1996)
  • Wu Wen-Tsun (1997)
  • Gerard Huet (1998)
  • Robert S. Boyer and J Strother Moore (1999)
  • William W. McCune (2000)
  • Donald W. Loveland (2001)
  • Mark E. Stickel (2002)
  • Peter B. Andrews (2003)
  • Harald Ganzinger (2004)
  • Martin Davis (2005)
  • Wolfgang Bibel (2006)
  • Alan Bundy (2007)
  • Edmund Clarke (2008)
  • Deepak Kapur (2009)
  • David Plaisted (2010)
  • Nachum Dershowitz (2011)
  • Melvin Fitting (2012)
  • Greg Nelson (2013)
  • Robert L. Constable (2014)
  • Andrei Voronkov (2015)
  • Zohar Manna and Richard Waldinger (2016)
  • Lawrence C. Paulson (2017)
  • Bruno Buchberger (2018)
  • Nikolaj Bjørner and Leonardo de Moura (2019)
  • Franz Baader (2020)
  • Tobias Nipkow (2021)
  • Natarajan Shankar (2022)
  • Moshe Vardi (2023)
  • Armin Biere (2024)

At most one Herbrand Award will be given in each year. Nominations for the Herbrand award can be submitted at any time; the deadline for nominations to be considered for the Herbrand Award 2025, which will be given at CADE'30, is

February 28 2025
Nominations pending from previous years must be resubmitted in order to be considered.

Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contributions (including the relationship to CADE), along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent via e-mail to

Jürgen Giesl, President of CADE Inc.
with copies to
Philipp Rümmer, Secretary of CADE Inc.

The Herbrand Award Committee 2025

In its meeting on December 16 2024, the CADE Inc. board of trustees has decided to update the procedure for deciding on the Herbrand award. The new award procedure, which applies from 2025, has two stages: nomination and decision by the Herbrand award committee. The award committee is established by the CADE Inc. board of trustees ahead of the nomination deadline.

The following rules apply for the nomination phase:

  • Current members of the board of trustees of CADE Inc., of the IJCAR steering committee (in IJCAR years), of the Herbrand award committee, as well as the chairs of the current CADE or IJCAR conference cannot be nominated for the Herbrand award.
  • Current members of the Herbrand award committee cannot be nominators, and cannot provide letters of endorsement for nominations.

In 2025, the Herbrand award committee consists of the following people, listed here in alphabetical order:

The board of trustees reserves the option to exclude or replace committee members after receiving the nominations, in case a conflict of interest involving nominees and members of the award committee is identified.

For more details, please check the Herbrand Award webpage.

Bill McCune PhD Award in Automated Reasoning 2025: Call for Nominations

Automated Reasoning is the area of Computer Science dedicated to applying reasoning in the form of logic to computing systems. The Bill McCune PhD Award in Automated Reasoning distinguishes each year a PhD thesis defended the previous year, for its substantive contributions to the field of Automated Reasoning, its theory, its implementation, and/or its application on important problems. The award is named after the American computer scientist William Walker McCune, known for his contributions in the fields of Automated Reasoning, Algebra, Logic, and Formal Methods. He was the implementer of OTTER, Prover9 and Mace 4, automated tools for first-order reasoning which are known to this day for their accuracy and robustness. He was also known for his generosity towards research colleagues and as a great supporter of young researchers in the field.

Eligibility
Eligible for the award are those who successfully defended their PhD

  • at an academic institution;
  • in the field of Automated Reasoning; and
  • in the period from 1 January 2024 - 31 December 2024.
The PhD students supervised or co-supervised by the Expert Committee members are not eligible.

Nomination
Candidates for the award must be nominated by their supervisor(s) and one additional independent researcher who reviewed/examined the thesis. Nominations are to be submitted via email, by February 24, 2025 (Anywhere on Earth).

The nomination must consist of one compressed file (.zip) containing:

  • a letter from the supervisor(s) describing why the thesis should be considered for the award and the relationship of the contributions to CADE/IJCAR;
  • a report from the nominating additional independent researcher who reviewed/examined the thesis;
  • the thesis itself;
  • a copy of the PhD diploma; and
  • a copy of relevant papers by the nominee, if any, containing results published in the thesis.

Procedure
The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of Automated Reasoning.

  • The nominations will be evaluated and compared by an international Expert Committee (see below).
  • The procedure to be followed is analogous to the review phase of a conference. The justification by the supervisor and the nominating additional independent researcher report will play an important role in the evaluation.
  • The final decision is made by the Expert Committee at least one month before CADE/IJCAR is being held.
  • The award consists of a certificate announcing the winner to have received the Bill McCune PhD Award in Automated Reasoning. The award will be announced at the respective year's CADE/IJCAR. The nominators of the winner will also receive a copy of this certificate. The recipient of the award is expected to attend the award ceremony.
  • The decision of the Expert Committee is final and cannot be appealed.

Expert Committee
The Expert Committee, consisting of leading researchers in Automating Reasoning, is formed by the board of CADE Trustees with the aim to reflect the broad diversity in the area of Automated Reasoning. It is announced with the call for nominations, and thus formed before this call. The decision on the award is taken by the Expert Committee. The Expert Committee can seek additional expertise, even after the submission deadline for nominations. Expert Committee members cannot nominate a PhD student. Expert Committee members cannot contribute an independent report seconding a nomination.

The Expert Committee for the Bill McCune PhD Award 2025 consists of the following people:

  • Haniel Barbosa, Universidade Federal de Minas Gerais
  • Pascal Fontaine, University of Liege
  • Carsten Fuhs, Birkbeck, University of London (chair)
  • Claudia Nalon, University of Brasilia
  • Philipp Ruemmer, University of Regensburg
  • Martina Seidl, Johannes Kepler University
  • Viorica Sofronie-Stokkermans, University of Koblenz
  • Sophie Tourret, Inria - LORIA

Events

CSL 2025: 33rd EACSL Annual Conference on Computer Science Logic 2025, call for participation

February 10-14, 2025, Amsterdam, the Netherlands

CSL is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.

Co-located workshops
Two workshops are co-located with CSL, and will take place on Monday, February 10:

More information is available on the conference's web page.

Conferences

CADE-30: 30th international Conference on Automated Deduction, call for papers

July 28 - August 2, 2025, Stuttgart, Germany

CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including logical foundations, theory and principles, applications in and beyond computer science and mathematics, and implementations of automated reasoning systems are solicited. CADE-30 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction.

Important Dates (AoE)

  • Abstract submission: February 17, 2025
  • Full papers: February 24, 2025
  • Rebuttal period: April 14-18, 2025
  • Author notification: April 28, 2025
  • Final version deadline: May 30, 2025
  • Main conference: July 28-31, 2025
  • Satellite events: August 1-2, 2025

More information is available on the conference's web page.

TYPES 2025: 31st International Conference on Types for Proofs and Programs, call for papers

June 9 - 13, 2025, Glasgow, Scotland, UK

The TYPES meetings are a forum to present new and ongoing work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming.

Topics of interest include (but are not restricted to):

  • foundations of type theory and constructive mathematics
  • applications of type theory
  • dependently typed programming
  • industrial uses of type theory technology
  • meta-theoretic studies of type systems
  • proof assistants and proof technology
  • automation in computer-assisted reasoning
  • links between type theory and functional programming
  • formalizing mathematics using type theory

Important Dates (AoE):

  • Submission of 2-page abstract: March 3, 2025
  • Author notification: April 11, 2025
  • Camera-ready version of abstract: May 9, 2025

More information is available on the conference's web page.

ITP25: 16th International Conference on Interactive Theorem Proving, call for papers

September 27 - October 3, 2025, Reykjavik, Iceland

The ITP conference series is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics. This will be the 16th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988.

ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include, but are not limited to, the following:

  • Formalizations of computational models
  • Improvements in interactive theorem prover technology
  • Formalizations of mathematics
  • Integration with automated provers and other symbolic tools
  • Verification of security algorithms
  • Industrial applications of interactive theorem provers
  • Formal specification and verification of hardware and software
  • User interfaces for interactive theorem provers
  • Use of theorem provers in education
  • Concise and elegant worked examples of formalizations (proof pearls)

Important Dates (AoE):

  • Abstract submission deadline: March 12, 2025
  • Paper submission deadline: March 19, 2025
  • Author notification: May 23, 2025
  • Camera-ready copy due: June 27, 2025

More information is available on the conference's web page.

TbiLLC 2025: 15th International Tbilisi Symposium on Logic, Language, and Computation, call for papers

September 8-12, 2025, Kutaisi, Georgia

The Programme Committee invites submissions for contributions on all aspects of logic, language, and computation. Work of an interdisciplinary nature is particularly welcome. The programme will include two plenary tutorials, four plenary invited lectures and two parallel tracks of contributed talks. In addition, there will be two topical workshops. More details will soon be made available via the TbiLLC website (see top).

Topics of interest include (but are not restricted to):

  • Natural language syntax, semantics, and pragmatics
  • Linguistic typology and semantic universals
  • Language evolution and learnability
  • Variability in language
  • Sociolinguistics
  • Historical linguistics, history of logic
  • Natural logic, inference and entailment in natural language
  • Natural language processing
  • Distributional and probabilistic models of information, meaning and computation
  • Logic, games, and formal pragmatics
  • Logic and cognition
  • Logics for artificial intelligence and computer science
  • Knowledge representation
  • Foundations of machine learning
  • Formal models of multiagent systems
  • Logics for social networks
  • Logics for knowledge, belief, and information dynamics
  • Computational social choice
  • Information retrieval, query answer systems
  • Constructive, intuitionistic, modal and other non-classical logics
  • Algebraic and coalgebraic logic and semantics
  • Categorical logic
  • Foundations of mathematics and mathematical logic
  • Models of computation
  • Formal languages and automata theory

Important Dates (AoE):

  • Submission deadline: March 14, 2025
  • Notification: 23 May 23, 2025

More information is available on the conference's web page.

SAT 2025: 28th International Conference on Theory and Applications of Satisfiability Testing, call for papers and workshop proposals

August 10-15, 2025, Glasgow, Scotland, UK (co-located with CP)

The scope of SAT 2025 includes all aspects of the theory and applications of propositional satisfiability broadly construed. This includes paradigms such as Boolean optimization using, e.g., MaxSAT and pseudo-Boolean (PB) solving, quantified Boolean formulas (QBF), satisfiability modulo theories (SMT), model counting, constraint programming (CP), and integer linear programming (ILP) for problems with clear connections to Boolean-level reasoning. This year the 31st International Conference on Principles and Practice of Constraint Programming (CP) will be co-located with SAT and will have deadlines and reviewing process synchronized with SAT 2025.

Call for Papers

Topics of interest include (but are not restricted to):

  • Theoretical advances (including algorithms, proof complexity, parameterized complexity, and other complexity issues)
  • Practical search algorithms
  • Knowledge compilation
  • Implementation-level details of SAT and SMT solving tools and SAT/SMT-based systems
  • Problem encodings and reformulations
  • Applications (including both novel applications domains and improvements to existing approaches)
  • Case studies and reports on scientific findings based on rigorous experimentation

Important Dates (AoE):

  • Abstract registration: March 20, 2025 AoE
  • Full paper submission: March 27, 2025 AoE
  • Author response: May 5-9, 2025 AoE
  • Notification of decisions: May 29, 2025 AoE
  • Camera-ready version submission: Early June
  • Workshops and Doctoral Program: August 10-11, 2024
  • Conference: August 12-15, 2024

Call for Workshop Proposals

We invite proposals for workshops to be held immediately before the main conferences in Glasgow, UK. Workshops offer an opportunity for in-depth discussions, hands-on experiences, and focused exploration of specific areas connected to constraint programming, SAT solving, and related topics.

Given the co-location of the CP and SAT conferences, we especially encourage proposals for workshops of interest to both communities. Some example topics from recent years are pragmatics of constraint reasoning, constraint modelling and SAT/SMT encodings, counting and sampling, logic-based methods in ML, CP-SAT solving, proof complexity, certifying algorithms, and logic and search. Proposals of interest to a single community, either on previously covered topics or new topics, are also welcome.

While you are free to have a traditional workshop with submitted papers, we also encourage new ideas and formats that could foster more interaction from your audience. We encourage in particular short papers and position papers, a lightweight review process, and poster sessions.

Important Dates (AoE):

  • Proposal submission: March 20, 2025
  • Notification of decisions: March 30, 2025
  • Workshops: August 10-11, 2025
  • Main conferences: August 12-15, 2025

For inquiries and submissions, please contact the workshop chairs Zeynep Kiziltan and Marc Vinyals.

More information is available on the SAT and CP web pages.

MFPS XLI: 41st Conference on Mathematical Foundations of Programming Semantics, call for papers

June 16-20, 2025, Glasgow, Scotland, UK (Joint with CALCO)

MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.

Topics of interest include (but are not restricted to):

  • bio-computation
  • concurrent qualitative and quantitative distributed systems
  • process calculi
  • probabilistic systems
  • constructive mathematics
  • domain theory and categorical models
  • formal languages
  • formal methods
  • game semantics
  • lambda calculus
  • programming language theory
  • quantum computation
  • security
  • topological models
  • logic
  • type systems
  • type theory
  • denotational and operational semantics
  • rewrite theory
  • proof theory

Important Dates (AoE):

  • Abstract Submission: March 27, 2025
  • Paper Submission: April 3, 2025
  • Notification: May 12, 2023
  • Pre-proceedings: May 24, 2023
  • Final (post-proceeding) versions: Autumn 2025

More information is available on the conference's web page.

ICLP 25: 41st International Conference on Logic Programming, call for papers

September 12-19, 2025, University of Calabria, Rende, Italy

Since the first conference In Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to:

  • Theoretical Foundations: Formal and operational semantics, Non-monotonic reasoning, Reasoning under uncertainty, Knowledge representation, Semantic issues of combining logic and neural models, Complexity results.
  • Language Design and Programming Methodologies: Concurrency and parallelism, Mobility, Interacting with ML, Logic-based domain-specific languages, Hybrid logical and imperative/functional languages, Programming techniques, Answer Set Programming, Inductive Logic Programming, Coinductive Logic Programming
  • Program Analysis and Optimization: Analysis, Transformation, Verification, Debugging, Profiling, Visualization, Logic-based validation of generated programs.
  • Implementation Methodologies: Compilation, Parallel/distributed execution, Constraint implementation, Tabling, Logic-based prompt engineering, User interfaces.

Affiliated Events

  • Workshops: September 12-14, 2025
  • Doctoral Consortium: September 12-14, 2025
  • Autumn School in Computational Logic: September 12-14, 2025
  • Thematic Tracks (to be announced)
  • International Symposium on Principles and Practice of Declarative Programming (PPDP 2025)
  • Logic-based Program Synthesis and Transformation (LOPSTR 2025)

Important Dates (AoE):

  • Paper registration (regular papers): April 13, 2025
  • Paper submission (regular papers): April 18, 2025
  • Notification to authors (regular papers): May 25, 2025
  • Paper submission (short papers): June 15, 2025
  • Revision submission (regular papers): June 15, 2025
  • Final notification to authors: July 6, 2025
  • Main conference: September 15-19, 2025

More information is available on the conference's web page.

FMCAD 2025: 25th International Conference on Formal Methods in Computer-Aided Design, call for papers

October 6-10, 2025, SRI Headquarters, Menlo Park, CA, US

FMCAD 2025 is the twenty-fifth edition in a series of conferences on the theory and applications of formal methods in hardware and system verification. The conference encompasses a wide range of topics related to formal aspects of computer-aided system design, including verification, specification, synthesis, and testing and provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems.

FMCAD 2025 includes the FMCAD Student Forum and is co-located with VSTTE 2025.

FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods and their applications to computer-aided design. Topics of interest include (but are not restricted to):

  • Model checking, theorem proving, equivalence checking, abstraction and reduction, compositional methods, decision procedures at the bit- and word-level, probabilistic methods, combinations of deductive methods and decision procedures.
  • Synthesis and compilation for computer system descriptions, modeling, specification, and implementation languages, formal semantics of languages and their subsets, model-based design, design derivation and transformation, correct-by-construction methods.
  • Application of formal and semi-formal methods to functional and non-functional specification and validation of hardware and software, including timing and power modeling, verification of computing systems on all levels of abstraction, system-level design and verification for embedded systems, cyber-physical systems, automotive systems and other safety-critical systems, hardware-software co-design and verification, and transaction-level verification.
  • Experience with the application of formal and semi-formal methods to industrial-scale designs; tools that represent formal verification enablement, introduce new features, or substantially improve the automation of formal methods.
  • Application of formal methods to verifying safety, connectivity and security properties of networks, distributed systems, smart contracts, block chains, and IoT devices.
  • Application of formal methods to the analysis of machine learning systems, and applications of machine learning to enhance formal methods techniques.

Important Dates (AoE):

  • Abstract Submission Deadline: April 20, 2025
  • Paper Submission Deadline: April 27, 2025
  • Author Response: June 17 - June 19, 2025
  • Author Notification: July 1, 2025

More information is available on the conference's web page.

CICM 2025: 18th Conference on Intelligent Computer Mathematics and LSFA 2025: 20th International Symposium on Logical and Semantic Frameworks, with Applications, call for papers

October 6-11, 2025, Brasilia, Brazil

More and more mathematical information is digitally processed, generated, communicated, stored, and curated. CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration. Besides the CICM main program soliciting formal CICM submissions there will be associated workshops with separate submission options.

Topics of interest include (but are not restricted to):

  • theorem proving and computer algebra
  • mathematical knowledge management
  • digital mathematical libraries

Important Dates (AoE):

  • Abstract deadline: April 28, 2025
  • Full paper deadline: May 5, 2025
  • Reviews sent to authors: June 16, 2025
  • Rebuttals due: June 20, 2025
  • Notification of acceptance: July 4, 2025
  • Camera-ready copies due: July 18, 2025

20th International Symposium on Logical and Semantic Frameworks, with Applications

LFSA 2025 is a satellite event of CICM 2025. LSFA is an International Symposium on Logical and Semantic Frameworks with Applications launched in 2006. Logical and semantic frameworks are formal languages that represent logics and languages, as well as computational, AI and deductive systems. These frameworks provide mathematical foundations for the formal specification of systems and programming languages, supporting tool development and reasoning.

The LSFA series is a platform that fosters collaboration, bringing together theoreticians and practitioners. LSFA aims to promote techniques and results from the theoretical side, ranging from well-established ones such as lambda calculus and type theory to state-of-the-art ones such as machine learning, and provide feedback on integrating, implementing and using such methods and results from the practical side.

Important Dates (AoE):

  • Abstract deadline: May 5, 2025
  • Full paper deadline: May 12, 2025
  • Notification of acceptance: June 27, 2025
  • Camera-ready copies due: July 18, 2025

More information is available on CICM 2025 and LSFA 2025 web pages.

ECAI-2025: 28th European Conference on Artificial Intelligence, call for papers

October 25-30, 2025, Bologna, Italy

We invite all members of the international AI research community to submit their best work to the 28th European Conference on Artificial Intelligence, which will take place in the historic city of Bologna from October 25 to 30, 2025.

We welcome submissions on all aspects of AI. Submissions will be subject to double-blind peer review by the programme committee. They will be evaluated based on relevance, clarity, significance, originality, soundness, reproducibility, scholarship, and quality of presentation.

The conference is planned as an in-person event. Each accepted paper will get assigned either an oral presentation slot or a combined poster/spotlight presentation slot. The presentation modality is not intended to reflect perceived scientific quality of the paper, so this assignment will be made in a randomised fashion (subject to programme constraints).

Submissions on all aspects of AI are welcome. This includes in particular:

  • Computer Vision
  • Constraints and Satisfiability
  • Data Mining
  • Fairness, Ethics, and Trust
  • Game Theory and Economic Paradigms
  • Humans and AI
  • Intelligent Robotics
  • Knowledge Representation and Reasoning
  • Machine Learning
  • Multiagent Systems
  • Natural Language Processing
  • Planning and Search
  • Uncertainty in AI
  • Multidisciplinary Topics

Important Dates (AoE):

  • Submission site opening: April 10, 2025
  • Abstract deadline: April 29, 2025
  • Paper deadline: May 6, 2025
  • Rebuttal period: June 23-25, 2025
  • Author notification: July 10, 2025
  • Camera-ready deadline: August 26, 2025

More information is available on the conference's web page.

JELIA 2025:19th European Conference on Logics in Artificial Intelligence, call for papers

September 1-5, 2025, Kutaisi International University, Kutaisi, Georgia

The aim of JELIA 2025 is to bring together active researchers interested in the use of logics in Artificial Intelligence, in order to discuss current research, results, problems, and applications of both theoretical and practical nature. JELIA strives to foster links and facilitate cross-fertilization of ideas among researchers from various disciplines, among researchers from academia and industry, and between theoreticians and practitioners.

Topics of interest include (but are not restricted to):

  • Abductive and inductive reasoning
  • Applications of logic-based AI systems
  • Argumentation
  • Automated reasoning including satisfiability checking and its extensions
  • Causality and logics
  • Computational complexity and expressiveness
  • Deontic logic and normative systems
  • Description logics and other logical approaches to ontologies
  • Knowledge representation, reasoning, and compilation
  • Learning and reasoning
  • Logic programming, answer set programming, constraint logic programming
  • Logics in machine learning
  • Logics for uncertain and probabilistic reasoning
  • Logics in multi-agent systems, games, and social choice
  • Neural networks and logic rules
  • Non-classical logics, such as modal, temporal, epistemic, dynamic, spatial, paraconsistent, and hybrid logics
  • Nonmonotonic logics, default logics, conditional logics
  • Planning and diagnosis based on logic
  • Preferences and optimization
  • Reasoning about actions
  • Updates, belief revision and nonmonotonic reasoning

Important Dates (AoE):

  • Abstract submission: May 2, 2025
  • Paper submission: May 9, 2025
  • Notification of acceptance: July 1, 2025
  • Camera-ready due: July 10, 2025

More information is available on the conference's web page.

TABLEAUX 2025: 33rd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, call for papers

September 30 - October 2, 2025, Reykjavik, Iceland

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):

  • Analytic tableaux for various logics (theory and applications)
  • Related techniques and concepts (e.g., model checking and BDD’s)
  • Related methods (e.g., model elimination, sequent calculi, connection method)
  • New calculi and methods for theorem proving in classical and non-classical logics (e.g., modal, intuitionistic, linear, temporal)
  • Systems, tools, implementations and applications (e.g., verification)

Important Dates (AoE)

  • Submission of title and abstract: May 9, 2025
  • Paper submission deadline: May 14, 2025
  • Notification of acceptance: July 9, 2025
  • Final version: July 31, 2025
  • Conference date: September 30 - October 2, 2025

More information is available on the conference's web page.

RuleML+RR 2025: 9th International Joint Conference on Rules and Reasoning, call for papers

September 22-24, 2025, İstanbul, Türkİye (Co-located with Declarative AI 2025)

RuleML+RR 2025 is a leading international joint conference in the field of rule-based reasoning. One of the main goals of RuleML+RR is to build bridges between academia and industry in the area of semantic reasoning.

RuleML+RR 2025 aims to bring together researchers and practitioners interested in the foundations and applications of rules and reasoning. It provides a forum for stimulating cooperation between different communities focused on the research, development, and applications of rule-based systems. We solicit high-quality papers related to theoretical advances, novel technologies, and applications that involve rule-based representation and reasoning or other declarative forms of artificial intelligence.

Topics of interest include (but are not restricted to):

  • Ontology/Semantic Web
  • Rules for AI and AI for Rules
  • Rules and Reasoning / Logics
  • Rules-Based Systems
  • Rules and Interoperability
  • Constraints and Schema
  • System Descriptions, Applications and Experiences of Ontologies and Rules

The conference will also include the following events:

Important Dates (AoE):

  • Abstract submission: June 2, 2025
  • Paper submission: June 9, 2025
  • Notification: July 28, 2025
  • Conference: September 22–24, 2025

More information is available on the conference's web page.

Workshops

VSS 2025: First International Workshop on Verification of Scientific Software, call for papers

May 04, 2025, Hamilton, ON, Canada (co-located with ETAPS)

Software plays an increasingly important role in scientific and engineering disciplines. Climate modeling, weather prediction, drug discovery, the design of buildings, vehicles, and aircraft, simulations of astrophysical phenomena, and prediction of seismic activity are some of the many applications. Verification of such software presents numerous challenges, e.g.: the programs are large, complex, and utilize multiple CPU and GPU concurrency interfaces; precise reasoning about real or floating-point operations is often required; there is often no oracle; and correctness may require reasoning about deep mathematical concepts such as convergence and stability. This workshop will focus on verification techniques that address these challenges, including approaches based on deductive reasoning, model checking, symbolic execution, abstract interpretation, and static analysis.

The workshop will take place as part of ETAPS 2025, on Sunday, May 4, 2025, at McMaster University in Hamilton, Canada. We aim to bring together researchers from both the scientific computing and the software verification communities. Through invited talks and presentations of peer-reviewed papers, participants will learn about the correctness challenges developers face, as well as a variety of verification approaches for tackling those challenges.

We are interested in all aspects of the verification problem for scientific software, including, but not limited to:

  • Ways to specify scientific software
  • Reasoning about mathematical concepts realized in software, including linear algebra, differential equations, convergence, stability, and order of accuracy
  • Effective verification techniques for programs that use MPI, OpenMP, CUDA, or other CPU or GPU concurrency interfaces used in scientific computing
  • Precise reasoning about floating-point computations
  • Techniques to reason about discretization in time and space, such as discrete grids and adaptive mesh refinement
  • Case studies applying verification tools to scientific software
  • Methods to decompose verification problems for scientific programs, such as function contracts

Important Dates

  • Submission deadline: February 1, 2025
  • Notification: March 1, 2025
  • Titles/abstracts of accepted papers published on workshop web site: March 15, 2025
  • Papers published on workshop web site: May 1, 2025
  • Workshop: May 4, 2025
  • Final versions of papers due: June 4, 2025

More information is available on the workshop's web page.

FMBC 2025: 6th International Workshop on Formal Methods for Blockchains, call for papers

May 04, 2025, Hamilton, ON, Canada (Co-located with ETAPS)

Blockchain is a novel technology to store data in a decentralized way. Although the technology was originally invented to enable cryptocurrencies, it quickly found applications in several other domains.

Blockchains may also provide support for Smart Contracts. Smart Contracts are scripts of an ad-hoc programming language that are stored on the blockchain and that run on the network. They can interact with the ledger’s data and update its state. These scripts can express the logic of possibly complex contracts between users of the blockchain. Thus, Smart Contracts can facilitate the economic activities of blockchain participants.

Since blockchains are often used to store financial transactions, bugs may result in huge economic losses and thus it is now of utmost importance to have strong guarantees of the behaviour of blockchain software. These guarantees can be brought by using Formal Methods. Indeed, Blockchain software encompasses many topics of computer science where using Formal Methods techniques and tools is relevant: consensus algorithms to ensure the liveness and the security of the data on the chain, programming languages specifically designed to write smart contracts, cryptographic protocols, such as zero-knowledge proofs, used to ensure privacy, etc.

Topics of interest include (but are not restricted to):

  • Formal models of blockchain applications or concepts
  • Formal methods for consensus protocols
  • Formal methods for blockchain-specific cryptographic primitives or protocols
  • Formal languages for Smart Contracts
  • Verification of Smart Contracts
  • Zero-knowledge proof and its applications in a blockchain setting

Important Dates

  • Abstract submission: February 3, 2025
  • Full paper submission: February 10, 2025
  • Notification: March 14, 2025
  • Camera-ready: March 31, 2025

More information is available on the workshop's web page.

Workshop in Programs from Proofs Meets Formal Mathematics, call for papers

July 28 - August 1, 2025, Ruhr University Bochum, Germany (part of ESSLLI 2025)

The aim of this workshop is to bring together experts in proof theory with specialists in formal mathematics and automated theorem proving, in order to facilitate an interdisciplinary exchange of ideas on the mutual benefit that these areas can have on one another. On the one hand, the workshop will focus on how methods from proof theory, such as advanced techniques aimed at extracting computational content from large scale nonconstructive proofs in mainstream mathematics, can be implemented and partially automated within theorem provers. In the other direction, we will explore whether the rich variety of logical systems developed by proof theorists could benefit the world of formal mathematics by both simplifying and streamlining the formalisation process.

We welcome 30 minute contributed talks on any topic broadly within the scope of the workshop. We are particularly interested in work that explores the following themes and their intersection:

  • Proof theory and its applications, particularly the extraction of programs from proofs.
  • Logical systems for reasoning about mathematics or the sciences.
  • Proof assistants (e.g. Agda, Coq, Isabelle, Lean).
  • Applications of AI and machine learning to formal mathematics.

Presentations from research students and early career researchers are particularly encouraged. To propose a talk, please submit your title and abstract by email to one of the organizers. We put no restrictions on the originality or publication status of submissions. There will be no formal proceedings.

Important Dates

  • Abstract submission deadline: April 15, 2025
  • Notification of acceptance: May 1, 2025
  • ESSLLI early registration deadline: May 31, 2025

Details about registration, along with local information, are available from the main ESSLLI webpages. As a part of ESSLLI, our workshop benefits from the funding opportunities offered for PhD students for the whole event. More information is available on the workshop's web page.

Seasonal Schools

OPLSS 2025:24th annual Oregon Programming Languages Summer School

June 23 - July 5, 2025, University of Oregon, Eugene, Oregon, USA

For 23 years, the Oregon Programming Languages Summer School has been devoted to teaching the principles of programming languages to students and professionals. Although the topics vary from year to year, the unifying theme is the importance of fundamental theory to the design and implementation of programming languages, the development of program verification tools, and the application of advanced programming languages to practice. The summer school attracts participants from around the world, and is often able to subsidize the participation of qualified attendees with limited resources. More than a thousand participants have attended OPLSS since its inception in 2002. The summer school is sponsored by the National Science Foundation, and by generous grants from numerous companies over the years.

The program takes place over two weeks, with ample time for group and private study, and to take advantage of the many recreational opportunities around Eugene. The sessions are non-overlapping, so participants will have the opportunity to attend all lectures. Each lecture is 80 minutes, including time for questions.

The registration deadline is March 14, 2025.

More information is available on the school's web page.

AAAI 2025 Tutorial on Machine Learning for Solvers

February 26, 2025, Philadelphia, PA, USA

Machine learning (ML) and logical reasoning have been the two foundational pillars of AI since its inception, yet it is only in the past decade that interactions between these fields have become increasingly prominent. Notably, ML has had a dramatic impact on SAT and SMT solvers, as demonstrated by the award-winning SATzilla, MapleSAT, and Z3alpha solvers. Our tutorial aims to inspire new interdisciplinary research by bridging the gap between ML and logical reasoning research communities. We will introduce the broader AI community to ML techniques that have been used in the context of logical reasoning solvers, with a sharp focus on approaches that are successful and promising. We will also host a panel discussion on how LLMs may shape this area going forward.

Rather than pure end-to-end learning, successful ML approaches tend to be tightly integrated with symbolic solvers. The central thesis of our tutorial, supported by numerous successful cases, is that ML excels best when it is used to sequence, select, initialize, and configure proof/rewrite rules that solvers implement. One prominent example that we will highlight is the use of ML for learning branching heuristics, both online for particular instances using reinforcement learning (RL) and offline training a neural network policy across representative instances from a particular application.

There will be theory, hands-on lab, and panel discussion on the use of ML for solvers.

More information is available on the tutorial's web page.

Meetings

AAAI North American ASL Meeting: Special Session on Proof Assistants

May 15 & 16, 2025, New Mexico State University, Las Cruces, NM, USA

A Special Session on Proof Assistants will be held as part of the 2025 North American Annual Meeting of the Association for Symbolic Logic. The whole ASL meeting will take place May 13-16, while the special session on proof assistants will take place on the last two days May 15 & 16.

There is some limited capacity for contributed talks (duration approx. 20 minutes). The deadline for contributed talk submissions is Thursday, February 27, 2025. Abstracts should be sent to Jonathan Weinberger and Patricia Johann. Reviewing of abstracts will be lightweight.

More information is available on the meeting's web page.

Competitions

VerifyThis 2025, call for problems

May 3-8, 2025, Hamilton, ON, Canada (at ETAPS)

VerifyThis is a series of program verification competitions, which has taken place annually since 2011 (with the exception of 2020). Previous competitions in the series have been held at FoVeOOS 2011, FM 2012, Dagstuhl (April 2014), and ETAPS 2015-2024. The challenge problems and solutions of previous competitions are available in the archive.

The aims of the competition are:

  • to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion.
  • to evaluate the usability of program verification techniques and tools.

The competition will offer a number of challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.

There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behavior of programs in focus. Solutions will be judged for correctness, completeness, and elegance.

To be able to offer a broad and diverse set of verification challenges, we are collecting submissions of ideas for verification challenges and problems. We welcome both problems of academic interest as well as challenges based on themes that are relevant in industry.

The competition proceeds in three rounds. In each round, participants are given 60 - 120 minutes to implement and prove specified properties of a given algorithm and/or data structure. They are free to use any verification tools they choose. Challenges are typically concerned with proving functional properties of the code in question (at least some part of a challenge involves expressing and proving properties specific to the algorithm/data structure in question). It is common for problems to have multiple parts, e.g. to prove some basic properties first, perhaps for a simplified case, and to progress to more-advanced goals.

We are currently looking for problem submissions! If you have recently encountered an interesting challenge in your work where formal techniques could be applied, please don't hesitate to submit it. Typical challenges have clear input-output specifications and often incorporate one or more of the following: heap allocation, concurrency, arithmetic reasoning. A challenge usually describes a problem using natural language together with some pseudocode, and then provides a list of properties or "verification tasks" of varied levels of difficulty. Contributors are encouraged to look at the Archive of previous problems.

An award will be given for any submission used in the competition. To avoid spoiling the competition for others, we ask that you keep the subject of your submission private. However, note that problem authors are allowed to participate in the competition!

A submission should consist of:

  • A brief yet precise problem description, specifically identifying verification sub-tasks.
  • A solution to the challenge is strongly encouraged, otherwise please provide a sketch of correctness.
  • The description document can use any reasonable format, including plain text or PDF.

Contributors are encouraged to look at the archive of previous problems. Submissions should be sent by email to Jenna DiVincenzo and Thomas Wies. The submission deadline is February 7th, 2025. We look forward to receiving your ideas!

More information can be found on the competition website.

Open Positions

Faculty Associate - Research of Computer Science, Naval Postgraduate School, Monterey, CA

The Naval Postgraduate School (NPS) is accepting applications for a Faculty Associate - Research in the Department of Computer Science (non-tenure track). We are especially interested in candidates with strong recent experience in software development for data science/AI/ML, especially with background and/or interest in natural language processing and linguistics. In particular, the work is centered around representation and reasoning in first-order logic and beyond.

We seek applicants with the following skills and experience:

  • Recent (past 5 years) experience with applied computer programming in Java, use and/or research, and using machine learning approaches in natural language processing.
  • Recent (past 5 years) demonstration of possession of three or more of the following skills (significant experience in one area may be balanced with lesser experience in another):
    • Excellent written and verbal communication skills
    • Strong organizational and planning skills
    • Java programming
    • Machine learning for natural language processing
    • Formal logic and automated theorem proving

We aim to fill the position by July 2024 and will begin reviewing applications starting 01 June 2024. Please find more information about the requirement and how to apply on this link.

Feel free to contact Adam Pease for more information.

PhD Position on Model Checking of Functional Programs at University of Sheffield, UK

We are pleased to announce that a PhD project is open with Dr. Charles Grellois (primary supervisor) and Dr. Harsh Beohar at the University of Sheffield. The title is the following: “Model-Checking of Functional Programs: from Theory to a Theorem Prover Implementation” (3.5 years). For more details on the project and how to apply, please visit this link.

Candidates are encouraged to get in touch by email. The application deadline for applicants is 5pm Wednesday 29th January 2025.

PhD Studentship at UCL Computer Science, UK

We invite applications for a four-year PhD studentship on the Leverhulme-funded project "ECUMENICAL: Proof-theoretic semantics for non-classical and modal logics," led by Dr. Elaine Pimentel, Prof. David Pym, and Prof. Luiz Carlos Pereira at UCL Computer Science, UK.

This interdisciplinary studentship, situated at the intersection of informatics, mathematics, and philosophy, is open to UK (home) students. The research will focus on developing proof-theoretic semantics for non-classical and modal logics, constructing the necessary abstract mathematical meta-theory, and investigating the implications of inferentialist semantics for systems verification. The project will build on recent advancements at UCL, including connections between the proof-theoretic foundations of logic programming and base-extension semantics, with potential exploration of applications to simulation modelling and its inferentialist interpretation.

The successful candidate will work closely with Dr. Elaine Pimentel (Computer Science), Prof. David Pym (Computer Science and Philosophy), and Prof. Luiz Carlos Pereira (Philosophy, UERJ Brazil). The student will be based within the Programming Principles, Logic, and Verification group at UCL Computer Science.

Application deadlines are the 3rd of February 2025 (for a May 2025 start) and the 1st of July 2025 (for an October 2025 start). More information can be found on the University's web page.

Two PhD Positions at the Computer Science and Engineering Department at the University of South Carolina, USA

The department has expertise in quantum programming languages and quantum computing, with a strong focus on leveraging methods from type systems, programming language theory, category theory, and theorem proving.

Interested candidates are encouraged to contact Frank (Peng) Fu directly. The application deadline for Fall 2025 is February 1, 2025.

For more information about the Ph.D. application process, see the admission page.

Two PhD Positions in Formal Semantics and Verification (with a focus on Rust) at ETH Zürich, Switzerland

The Programming Language Foundations Lab at ETH Zürich is looking for strong students that want to do research at the foundations of programming language theory, in program verification and separation logic, with a focus on Rust. Some experience with formal methods and PL theory is expected (e.g. from a suitable course); knowledge of interactive theorem provers or Rust is greatly appreciated but not required. Candidates need to have a master's degree.

Interested candidates should send an email to Refl Jung. Please explain why you are interested in a PhD in this field and what your prior experience is. Also include a CV and possible contacts for recommendation letters. Applications are considered on a rolling basis, so there is no fixed end date for this call, but if you want to be sure the position is still open then please submit your applications until the end of February, 2025.

See the Group's webpage for further information.

Several Postdoctoral Positions on Formal Methods for Security and Privacy at the Universitat Rovira i Virgili, Spain

We seek to hire a full-time postdoctoral researcher in the area of formal methods for security and privacy. The University offers:

  • A 2.5-year contract at an exciting international environment located in Tarragona, Spain.
  • Generous travel funds.
  • Possibility to co-supervise PhD students.

The successful candidate is expected to contribute to the PROVTOPIA project, which focuses on counteracting disinformation via Secure and Private Provenance Verification of Media Content. The candidate will work under the umbrella of the Crises research group under the direction of Dr. Rolando Trujillo. Include in your application the following documents:

  • Curriculum Vitae
  • Research statement
  • Contact information for 3 referees

Deadline for applications is 15 February 2025. Early applications are highly encouraged, though, as they will be processed upon reception. You can contact Dr. Rolando Trujillo for more information.

Internship at Virginia Tech's Systems Software Research Group, USA

Virginia Tech's Systems Software Research Group (https://www.ssrg.ece.vt.edu) invites applications for paid internships from undergraduate and graduate students on a verified compilation project. The project goals include building a formally verified framework for the Linux eBPF mechanism, including language, type system, and a verified compiler, for writing safe and correct eBPF programs.

Preferred qualifications:

  • Expertise with Coq theorem prover (Rocq)
  • Background in type system and programming languages
  • Good understanding of CompCert
  • Undergraduate or graduate student in Computer Science/Engineering, Mathematics, Electrical Engineering, or a related field

The starting date and time frame is flexible. Please contact Swarn Priya with a resume or for any questions.

Associate Professor Position at LIRMM, Montpellier, France

The MaREL research team (part of the LIRMM laboratory, a leading French research laboratory) specializing in Software Engineering is looking to recruit a new permanent member holding a PhD or an equivalent doctoral degree. The MaREL team aims to recruit for an Associate professor/Lecturer-Researcher (Maître de conférences) - Affiliated with the University of Montpellier, part of the MaREL team and the Computer Science Department of the Faculty of Sciences at the University of Montpellier.

The MaREL team is a research group within the LIRMM laboratory. It focuses on software engineering, particularly the automation of tasks related to all stages of the software lifecycle. The team seeks to strengthen its research areas, especially in the application of statistical and symbolic artificial intelligence techniques to address challenges in software development, maintenance, and evolution. Expertise in applying these techniques to problems such as software re-engineering for migration towards software product lines or microservices, or program verification, will be highly valued. The team is also actively involved in industry transfer activities.

Please contact please contact Abdelhak-Djamel Seriai (head of the MaREL team) if you want more information about the application's process.

PhD, Postdoc & Senior Researcher Positions in Tokyo, Japan

Hasuo Laboratory at the National Institute of Informatics, Tokyo, Japan invites applications for postdoc and senior researchers. The candidates will pursue collaboration with Bart Jacobs (Nijmegen), Joost-Pieter Katoen (Aachen), and Sam Staton (Oxford). The positions are for 4.5 years max.

This is a call for researchers at the JST ASPIRE project without specified topics. Relevant backgrounds include (but are not restricted to) formal methods, mathematical semantics, category theory, software science, programming languages, mathematical logic, control theory, machine learning, and optimization. Familiarity with formal logic is mandatory.

Please consult the project's webpage for scopes, details, and how to apply.

Ph position are also available. Please consult this webpage for more information.

We look forward to applications from junior and senior researchers with aspiring minds. Thanks a lot for your consideration!

Research Fellow in Verification or Security or Concurrent/Distributed Systems at University of Surrey, UK

The Department of Computer Science at the University of Surrey is seeking to recruit a full-time postdoctoral research fellow to work on a range of topics in the areas including:

  • Emerging hardware architectures (weak memory, RDMA, persistent memory, CXL)
  • Formal modelling, verification and/or logic
  • Interactive and automated tools, such as theorem provers and model checkers
  • Proofs of safety and/or security properties
  • Programming languages and/or type systems
  • Concurrent and/or distributed algorithms Related topics

The successful applicant will work in a multidisciplinary team, as well as a large team of academic (Imperial, MPI-SWS, Cornell, IMDEA) and industrial collaborators (Arm, NVIDIA, Galois), researchers and PhD students.

Applicants must have or be close to obtaining a PhD in Computer Science.

The application deadline for applicants is January 31st, 2025. You can apply on the University's web page. For informal enquiries and further information please contact Brijesh Dongol or Gregory Chockler.

Full-time Academic Position in Computer Science at Université libre de Bruxelles (ULB), Belgium

The Faculty of Sciences of the Université libre de Bruxelles (ULB) invites applications for a full-time academic position in Computer Science to begin October 1st, 2025. All areas of Computer Science will be considered. Candidates who can strengthen an existing team within our department are particularly encouraged to apply.

The Computer Science Department of ULB is a leading research and dynamic education center. Located in the capital of Europe, it offers a wide range of funding and research opportunities. Brussels is a cosmopolitan city with an excellent quality of life and easy access to all major cities in Europe. The position involves both teaching and research and some commitment to administrative tasks.

For more information, (e.g. concerning courses to be taught or the research carried out in the Department), please contact Mr John Jacono, Head of the Computer Science Department.

The application deadline for applicants is March 15, 2025. You can apply on the University's web page.

Multiple Job Openings at the University of Warsaw, Poland

The Faculty of Mathematics, Informatics and Mechanics of the University of Warsaw (MIM UW) invites applications for the positions of Assistant Professor in Computer Science, starting on 1st October 2025 or 1st February 2026.

MIM UW is one of the leading Computer Science faculties in Europe. It is known for talented students (e.g., two wins and multiple top tens in the ACM International Collegiate Programming Contest) and strong research teams, especially in algorithms, logic and automata, algorithmic economy, and computational biology. There is also a growing number of successful smaller groups in diverse areas including cryptography, databases and knowledge representation, distributed systems, and machine learning. Seven ERC grants in Computer Science are running at MIM UW at the moment.

In the current call, 7 positions are offered (follow the links for more details):

The deadline for applications is February 14, 2025. For further information about the procedure, requirements, conditions, etc., please contact Filip Murlak or Oskar Skibski.

Proof Engineer at Cryspen, France and Germany

Cryspen is on a mission to build high-assurance software and formal verification tools that make the world a safer place. We're looking for passionate Proof Engineers to join our collaborative team and help us achieve that goal.

Are you proficient in Rocq (ex Coq) or F* or Lean or HOL? Have you built or maintained large proof artifacts? Do you have experience in improving proof automation or developing verification tools? Are you eager to apply formal verification to real-world software?

If your answer is yes, apply and tell us more about your experience and your interests.

  • Shape the Future of Security: You'll develop and maintain correctness and security proofs for formally verified software solutions, primarily in Rust, and help improve a state-of-the-art software verification toolchain.
  • Work with the Best: Collaborate closely with reputed research scientists and experienced engineers to develop proofs for cutting-edge applications.
  • Make a Difference: You'll play a key role in the entire development process, from design and development to verification and testing.
  • Open Source Enthusiast? Cryspen embraces open source and actively contributes to the community. Prior open-source experience is valued, but not required.

For more information about the jobs, please visit the job offer's page.