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:
At most one Herbrand Award will be given in each year.
Nominations for the Herbrand Award 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. The following rules apply:
Nominations for the Herbrand award can be submitted at any time by email to
Jürgen Giesl, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.
The deadline for nominations to be considered for the Herbrand Award 2026, which will be given at IJCAR'26, is
March 10 2026Nominations pending from previous years must be resubmitted in order to be considered.
In 2026, 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.
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
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 made by March 10, 2026 (Anywhere on Earth).
Nominations should proceed in two steps:
In a first step, the supervisors planning to make a nomination should send an email to Viorica Sofronie-Stokkermans to obtain
a link at which to submit all the documents.
In a second step they should upload a zip file containing the following documents:
Procedure
The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of Automated
Reasoning.
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 2026 consists of the following researchers:
After eight years of excellent service, AAR and CADE Secretary Philipp Rümmer has informed the CADE Board of Trustees and the AAR Board of Directors that he wishes to step down. Philipp did incredible work during these eight years and deserves heartfelt thanks from all our field! Thus, the two corporations are seeking a new Secretary.
The role of Secretary is an important one, and most precious to our organizations. Former secretaries include Bill McCune, Bob Veroff, Maria Paola Bonacina, Amy Felty, Wolfgang Ahrendt, and Martin Giese. The two roles of Secretary of AAR and Secretary of CADE have been filled by the same person since 1999, because AAR and CADE are strongly interconnected: CADE is a subcorporation of AAR, and the members of AAR elect the board of trustees of CADE. Thus, this call is for candidates to be the Secretary of both AAR and CADE.
The Secretary is a full-right member of both the AAR Board of Directors and the CADE Board of Trustees. The Secretary shares with the other members of these boards the responsibility, and opportunity, to influence and shape the core community work and decisions. In addition, the Secretary has the following distinguished duties:
Clearly, this is a very important job, which may give a lot of reward: the new Secretary will inherit all necessary documents and historical records from the outgoing Secretary and will be welcomed by the two boards. As CADE President I'll be happy to welcome the new Secretary and help towards a smooth transition.
Interested applicants should send an e-mail message with a brief statement, highlighting motivation and previous organizational experience, if any, and the url of their web page, to
Jürgen Giesl, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.no later than March 10, 2026. The Secretary will be appointed by the two boards as soon as possible and all applicants will be informed of the outcome.
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.
The members of the board of trustees until the 2025 elections were:
The terms of Pascal Fontaine, Jürgen Giesl, André Platzer, and Sophie Tourret ended in 2025. The term of office of Uwe Waldmann as CADE-30 program co-chair ended after the CADE conference, and Armin Biere is joining the board of trustees as IJCAR 2026 program co-chair.
In the 2025 elections, four new trustees had to be elected.
The following candidates were nominated; their statements were given in the September newsletter:
The election was carried out using the Condorcet Internet Voting Service (CIVS) and the Condorcet completion Minimax-PM. Participants of the last three CADE/IJCAR conferences (who paid registration fees at at least one of the conferences) were invited to vote, and a total of 254 ballots were sent out on October 3. By October 17, 67 CADE members had voted through CIVS, which translates to a participation rate of 26.4% (as compared to 30.2% in 2024, 26.2% in 2023, 26.7% in 2022, 26.7% in 2021, 34.5% in 2019, 21.1% in 2018, 9.1% in 2017, 11.2% in 2016).
The results of the election can be viewed on CIVS:
The four candidates elected are Jürgen Giesl, Sophie Tourret, Uwe Waldmann, and Cláudia Nalon.
In the first meeting of the new board of trustees, Jürgen Giesl was unanimously reelected as the President of CADE Inc.
The new board of trustees is therefore:
On behalf of CADE Inc., I would like to thank Pascal Fontaine and André Platzer for their service for CADE over the last six resp. three years, and Viorica Sofronie-Stokkermans for running in the 2025 elections. I would like to congratulate Cláudia Nalon and Uwe Waldmann, who will join the board as new elected trustees, and Jürgen Giesl and Sophie Tourret on getting reelected!
We are pleased to announce the call for proposals for hosting and organising TABLEAUX 2027 and FroCoS 2027, on their 34th and 16th editions, respectively.
Tableaux and FroCoS have co-located for quite a number of editions. In 2027 we intend to continue this partnership. We expect the 2027 edition to have around 100 participants.
Bids should be sent to Elaine Pimentel and should include at least the following information:
The deadline for bids is March 31, 2026. The bids will be analysed by the TABLEAUX and FroCoS Steering committees and the result will be made public by mid April 2026.
ETAPS is a primary forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of four annual conferences accompanied by satellite workshops.
ETAPS 2026 will feature four invited speakers and two invited tutorials, covering a wide range of topics including data privacy, digital twins, large language models, model checking, probabilistic programming, symbolic reasoning, theorem proving, and more.
In addition to its main conferences, ETAPS 2026 will also host fifteen satellite events and three collocated events, including the ETAPS Industry Day. We strongly encourage you to submit to and attend these events.
More information is available on the conference’s web page.
ICALP 2026 is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). The conference brings together researchers in all areas of theoretical computer science.
Papers presenting original research on all aspects of theoretical computer science are sought. Typical, but not exclusive, topics of interest include:
Important Dates (AoE)
More information can be found on the conference's web page.
IJCAR is the premier international venue on all aspects of automated reasoning. It is held biannually as a merger of leading events in automated reasoning:
IJCAR 2026 invites submissions related to all aspects of automated or interactive logical reasoning, including foundations, implementations, and applications. Original research papers and descriptions/evaluations of working automated deduction systems or proof assistant systems are solicited.
IJCAR topics include (but are not limited to):
Important Dates (AoE, tentative)
More information will appear on the conference'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.
In addition to the Main Track, KR 2026 will include two special thematic tracks:
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.
Typical topics of interest include the following, but the list is not exhaustive. The conference welcomes all topics concerned with the explicit representation or management of knowledge, and with the automated inference on the basis of such knowledge.
KR 2026 will also include a Recently Published Research Track, a Video Track, tutorials, workshops, and a Doctoral Consortium.
Important Dates (AoE)
More information is available on the conference's web page.
Now in its 20th edition, TASE is an international symposium that aims to bring together researchers and developers from academia and industry with interests in the theoretical aspects of software engineering. We invite submissions of research papers on topics covering all theoretical aspects of software engineering.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
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 17th 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:
Important Dates (AoE)
More information can be found on the conference's web page.
PACMPL issue ICFP 2026 seeks original papers on the art and science of functional programming. Submissions are invited on all topics from principles to practice, from foundations to features, and from abstraction to application. The scope includes all languages that encourage functional programming, including both purely applicative and imperative languages, as well as languages with objects, concurrency, or parallelism.
ICFP welcomes submissions on all aspects of functional programming. Suggested topics include, but are not limited to, the following:
Important Dates (AoE)
More information can be found on the conference's web page.
SAT is the premier annual meeting for researchers focusing on the theory and applications of propositional satisfiability, broadly construed. That includes Boolean optimization, such as MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), model counting, and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information can be found on the conference's web page.
MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to the 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):
We also welcome contributions that address applications of semantics to novel areas.
Important Dates (AoE)
More information is available on the conference's web page.
PLS is a biennial scientific event established in 1997 to promote interaction and cross-fertilization among different areas of logic. Originally created to bring together logicians of Hellenic descent around the world, it has since grown into an international forum for the communication of state-of-the-art advances in logic. The symposium is open to researchers worldwide working in logic, broadly construed.
Areas of interest include (but are not limited to):
Important Dates (AoE)
More information can be found on the conference's web page.
The aim of the FMICS conference series is to provide a forum for researchers an practitioners who are interested in the development and application of formal methods in industry. FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.
FMICS is the ERCIM Working Group conference on Formal Methods for Industrial Critical Systems, and it is the key conference in the intersection of industrial applications and Formal Methods.
We encourage submissions on cross-cutting approaches that bring together formal methods and industrial applications. Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference’s web page.
SCML 2026 is dedicated to research combining Symbolic Computation (SC) and Machine Learning (ML) as two major approaches to Artificial Intelligence. The conference focuses on applying ML to SC, applying SC to ML, and hybrid approaches that integrate both paradigms to solve challenging problems.
SCML 2026 provides a forum to exchange ideas and discuss recent advances in this emerging research area, with ample opportunities to initiate new research projects, form collaborations, and identify funding opportunities.
SCML 2026 is a presentation-oriented conference. Submissions are solicited in the form of extended abstracts (1–2 pages), which are briefly reviewed for relevance. Accepted abstracts are published collectively as a conference booklet within the SCML publication forum. At least one author of each accepted abstract must register as a presenter.
Authors are also encouraged to submit related full papers to the SCML Publishing Forum. Papers are refereed independently and may be submitted at any time, before or after the conference. Acceptance of a presentation does not depend on acceptance of a full paper.
Topics of Interest
Important Dates (AoE)
More information is available on the conference web page.
RuleML+RR 2026 is the leading international conference in the field of rule-based reasoning. A primary goal of RuleML+RR is to build bridges between academia and industry in the area of semantic reasoning.
RuleML+RR 2026 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. This year, we particularly encourage contributions at the intersection of databases and AI, reflecting the growing importance of data-centric and hybrid approaches to rule-based reasoning.
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):
The conference will also include the following events:
Important Dates (AoE)
More information is available on the conference's web page.
The 15th International Workshop on Confluence (IWC 2026) aims at promoting further research in confluence and related properties. Confluence provides a general notion of determinism and is a central concept in rewriting. It relates to many topics in rewriting and computation, including completion, modularity, termination, and commutation, and has been studied in a wide range of rewriting formalisms. Recent advances have led to new techniques, tool support, certification efforts, and novel applications.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the workshop’s web page.
ARCH 2026 brings together researchers and practitioners to establish a curated set of benchmarks for continuous and hybrid systems and to test them in a friendly competition. The workshop focuses on verification techniques for these systems, emphasizing the transfer from theory to practice.
Topics of interest include, but are not limited to:
Important Dates (AoE)
More information is available on the workshop's web page.
Logical and semantic frameworks are formal languages used to represent logics, languages, and systems. These frameworks provide foundations for the formal specification of systems and programming languages, supporting tool development and reasoning.
We invite submissions on topics including, but not limited to:
Following LSFA tradition, in addition to the proceedings, a special issue LSFA 25+26 is being considered.
Important Dates (AoE)
More information is available on the symposium’s web page.
NMR is the premier forum for results in the area of nonmonotonic reasoning. Its aim is to bring together active researchers in this broad field within knowledge representation and reasoning (KR), including belief revision, uncertain reasoning, reasoning about actions, planning, logic programming, preferences, argumentation, causality, and many other related topics including systems and applications.
NMR 2026 aims to foster connections between the different subareas of nonmonotonic reasoning and provide a forum for emerging topics. We especially invite papers on systems and applications, as well as position papers addressing benchmark issues. The workshop will be structured by topical sessions fitting to the scopes of accepted papers.
Important Dates (AoE)
More information is available on the workshop's web page.
SD26 is the sixth international workshop on Structures and Deduction. It brings together researchers from different areas of proof theory, with a particular focus on new algebraic and geometric results that enhance our ability to manipulate proofs, reduce bureaucracy in deductive systems, and lead to new methods for proof search and novel forms of proof certificates.
Themes of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the workshop’s web page.
The Workshop on Termination traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether practical or theoretical, primary or derived.
The workshop provides a forum for cross-fertilization of ideas from different communities interested in termination, including computational mechanisms, programming languages, software engineering, constraint solving, and related areas. Its friendly atmosphere encourages fruitful exchanges leading to joint research and subsequent publications.
WST 2026 welcomes contributions on all aspects of termination. Papers investigating applications of termination—for example in complexity analysis, program analysis and transformation, theorem proving, program correctness, and modeling of computational systems— are particularly encouraged.
Topics of interest include (but are not limited to):
Termination Competition
Since 2003, the effect of WST to stimulate new research on termination
has been enhanced by the Termination Competition
and its continuously developing Problem Databases containing thousands
of programs as challenges for termination analysis in different
categories. In 2026, the Termination Competition will run during WST.
Important Dates (AoE)
More information is available on the workshop’s web page .
TEAL welcomes work on tools for learning about logic. Tools can be of many forms: tutors, restricted versions of standard logic tools, and more. They can be used at many levels: university, industrial, and more. If in doubt, you can always reach out to the chairs to check whether your work is in scope.
Our goal is to take advantage of the many groups of people who will be coming together for FLoC. Our anti-goal is to create yet another publication venue. We want to have a lively, interactive event that focuses on exchanging knowledge and helping grow this community. Therefore, we have many kinds of activities and corresponding submission formats.
TEAL is not limited to papers! You can submit in any of the following categories:
Important Dates (AoE)
More information is available on the workshop’s web page.
WiL 2026, the 10th International Workshop for Women in Logic, will take place in Lisbon on 24–25 July 2026 as a satellite event of FLoC 2026. The workshop highlights and increases awareness of the valuable contributions made by women in logic and computer science. Its goal is to promote excellent research led by women and strengthen visibility and representation within the community.
Topics of interest include, but are not limited to: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, games and logic, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security and privacy, rewriting, type systems and type theory, and verification.
Important Dates (AoE)
A limited number of travel grants is available for students and young researchers who would otherwise lack resources to attend WiL, and whose attendance would benefit both the applicant and the event.
More information is available on the workshop's web page.
This informal workshop will bring together users and developers of the interactive theorem prover Isabelle. The year 2026 is special as it marks the 40th anniversary of Isabelle, and therefore the workshop will span two full days.
The workshop aims to foster interaction between Isabelle users and developers, and to provide a forum for presenting new ideas, tools, applications, and ongoing work related to Isabelle and its ecosystem.
Important Dates (AoE)
More information is available on the workshop's web page.
The Vampire 2026 workshop will discuss recent developments in the implementation, application, evaluation, and comparison of first-order theorem provers, including but not limited to Vampire, and their interaction with other systems.
We seek submissions reporting on, but not limited to:
Submissions can range from work in progress to completed work. In particular, authors are invited to submit:
Papers may be of any length, ranging from 1-page abstracts to full papers of up to 20 pages. Submissions should use the EasyChair templates available at https://easychair.org/publications/for_authors .
Important Dates (AoE)
More information is available on the workshop's submission web page.
Term rewriting is a powerful model of computation that underlies much of declarative programming and which is heavily used in symbolic computation in mathematics, theorem proving, and protocol verification.
The International School on Rewriting (ISR) is aimed at Master and PhD students and provides an intensive introduction to rewriting techniques, as well as advanced courses on recent developments and applications. The school is held in the week before FLoC 2026, allowing participants enough time to reach Lisbon for the first workshop day. Accommodation and catering will be provided.
Tracks and TopicsScholarships may be available for students without their own funding, though this cannot be guaranteed. Early expressions of interest (by email) are encouraged to help set pricing and planning.
More information is available on the school's web page.
VerifyThis 2026 will take place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2026) on 11 and 12 April 2026. It is the 14th event in the VerifyThis competition series. Information on previous events and participants can be found here.
The aims of the competition are:
The competition will offer a number of challenges presented in natural language. 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. 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 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.
Submission Criteria:
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!
Submissions should be sent by email to Sacha Ayoun and Thibault Dardinier. The submission deadline is February 8, 2026. We look forward to receiving your ideas!
More information is available on the competition’s web page.
Static program analysis has matured to the point where many of our research tools can tackle substantial real-world code. What we lack are opportunities to exercise these tools on real software together, compare approaches, and learn from one another. Real-world audits require careful modeling and domain understanding, which can be time-consuming and scientifically unglamorous. AnalyzeThat creates a focused venue to make this work visible, collaborative and fun!
AnalyzeThat complements existing initiatives in the verification landscape. The Software Verification Competition (SV-Comp) provides rigorous evaluation on benchmarks with known outcomes, while VerifyThis offers a two-day challenge focused on deductive verification of intricate algorithms. AnalyzeThat instead emphasizes open-ended exploration of real software without predefined ground truth.
The aim of AnalyzeThat is to gather static analysis developers around a challenge: spending limited time auditing an open-source project. This event is built around two goals:
What kind of open-source project? To gather a significant number of interested parties, this first event will target analysis of real-world, non-concurrent C programs/libraries. You can find example projects that could be considered here.
Important dates (AoE)
Participation and coordination take place via Zulip.
More information is available on the competition's web page.
As a follow-up to the very successful workshop at CADE, we invite contributions to the Festschrift in Honor of Christoph Weidenbach's 60th Birthday. This Festschrift comes in the form of a topical collection (akin to a special issue) in the Journal of Automated Reasoning.
Christoph Weidenbach heads the Automation of Logic group at Max-Planck-Institut für Informatik, Saarbrücken. 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.
Contributions are invited in areas close to Christoph's research, including but not limited to:
Submissions should be 15 to 50 pages long. The submission deadline is February 28, 2026.
More information can be found on the journal's web page.
To celebrate the 25th year of Counterexample Guided Abstraction Refinement (CEGAR), we solicit papers for a special issue on its theoretical foundations and applications. This issue provides an overview of the current state of the CEGAR approach and its many applications.
Topics of interest include, but are not limited to:
The submission deadline is February 28, 2026. Please submit your manuscript to Formal Methods in System Design (FMSD) as a regular submission. Once you enter the details of the manuscript, you will have the option of choosing a collection. There, choose "Special issue on 25 years of CEGAR".
More information can be found on the journal's web page.
Proof-theoretic semantics (P-tS) offers a foundational shift in logic by prioritizing inference over truth conditions and emphasizing the centrality of proof in the assignment of meaning. This inferential perspective is naturally aligned with computational approaches; however, the intersection of proof-theoretic semantics and computation remains comparatively underexplored.
This special issue of the Journal of Logic and Computation aims to address this gap by bringing together contributions at the interface of logic, computer science, and philosophy. We invite submissions that explore how computational interpretations of logic interact with proof-theoretic approaches, both conceptually and practically.
Topics of interest include, but are not limited to:
Submissions must engage substantively with the ideas of proof-theoretic semantics and their relevance to computational practice. Submissions that address computational topics in isolation, without a clear connection to proof-theoretic semantics, will not be considered.
The submission deadline is March 31, 2026.
More information and submission instructions are available on the journal’s web page.
For enquiries, please contact Sara Ayhan, Alexander V. Gheorghiu, or Will Stafford.
This special issue aims to collect state-of-the-art research on Constrained Horn Clauses (CHCs). Many program verification and synthesis problems of interest can be modeled directly using Horn clauses, and recent advances in constraint logic programming and computer-aided verification have focused on efficiently solving problems presented as Horn clauses. CHCs are thus an enabling technology for modern verification and synthesis techniques, relevant to multiple communities including constraint / logic programming, program verification, and automated deduction.
Topics of interest include, but are not limited to:
The submission deadline is April 1, 2026.
More information can be found on the journal's web page.
String is a basic data type in almost every programming language and has been widely used in many scenarios, especially web programming. String constraint solving is a classical topic in theoretical computer science. In the last decade, it has received a lot of attention as a result of the momentum from formal verification of string-manipulating programs. Various string constraint solvers have been developed and used within verification and testing tools. Nevertheless, the area still poses many open questions, ranging from the fundamental decidability and complexity questions to devising powerful heuristics that can quickly handle real-world string constraints, to the design of algorithms that efficiently reason about string-manipulating programs.
The objective of this topical collection is to highlight recent advances in the area of string constraints, including, but not limited to, decidability and complexity results for fragments of string constraints, decision procedures, heuristics for solving, as well as tools and systems for analysing string-related properties in programs.
We welcome original research and extended versions of conferences submissions that are well-suited to the topic of the journal.
The submission deadline is April 1, 2026.
More information can be found on the journal's web page.
The Theoretical Computer Science group at FAU Erlangen–Nürnberg has an opening for a PhD position within the new German–French DFG–ANR project "Advancing the Theory of Quantitative Universal Algebra".
The principal investigators are Stefan Milius and Henning Urbat on the German side, and Matteo Mio (CNRS & ENS Lyon) on the French side. The project aims to advance the theory and applications of quantitative universal algebra towards a comprehensive body of results, constructions, and tools for the mechanizable deductive and algorithmic treatment of specifications with quantitative aspects.
The position is funded at salary level TV-L 13 (full time) for a period of three years, commencing in April or May 2026.
Complete application documents should be submitted by email until February 6, 2026.
ProfessorshipsFriedrich-Alexander-Universität Erlangen-Nürnberg is seeking applicants for a full professorship in Programming Languages. Areas of particular interest include verification and other topics in programming languages.
For more information and the full call, please see here.
The Department of Computer Science at Royal Holloway, University of London invites applications for a postdoctoral research associate position.
The position is funded by the EPSRC project INDIMO (Invariant Discovery and Monitoring for Message-Passing Programs) joint with the University of Kent. The project focuses on developing new techniques and tools to automatically detect bugs such as deadlocks in message-passing concurrent systems (in languages such as Go and Erlang), with particular emphasis on programs with statically unknown parameters (e.g., channel bounds, number of processes). We will adopt a hybrid approach to software verification combining the high coverage of static approaches with the high precision of dynamic approaches.
The successful candidate will join the Systems & Software Security Lab (S3Lab) at Royal Holloway, a dynamic research group of 3 academics, 7 PhD students, and 1 postdoc. The project involves collaboration with leading industry partners (Uber and WhatsApp), the University of Kent, and the University of Aarhus.
The position is full-time for three years, with a flexible start date around March 2026. The application deadline is February 19, 2026.
For informal enquiries, please contact Julien Lange. Full details and application instructions are available here.
Inria Rennes (France) invites applications for a postdoctoral researcher position with a strong background in either Artificial Intelligence (AI) or Formal Methods (FM).
The successful candidate will join a collaboration between Inria and Mitsubishi Electric R&D Centre Europe (MERCE) on formal reasoning applied to AI for software engineering.
The objective of the project is to propose new AI techniques for generating correct and informative formal code annotations directly from program source code.
The application deadline is February 19, 2026, with a possible start date from February 2, 2026. Full details of the position and application instructions are available here.
For informal enquiries, please contact Thomas Genet.
A job vacancy under the title "Formal Methods at the crossroads of Hardware and Software" is open within the ACES team of Télécom Paris. The position aims at strengthening the team's expertise in hardware/software systems, where the interplay between hardware elements and software code is essential to ensure correct system operation. Applications include cyber-security (e.g., side channels and information leakage), critical real-time systems (avionics, railways, automotive), and energy-constrained systems such as IoT infrastructures.
More generally, the position targets systems that must satisfy both functional and non-functional properties, with a strong emphasis on formal methods (broadly construed) to increase trust in system correctness.
Télécom Paris, an international multidisciplinary center for education, research, and innovation, is a leader in the digital world. We are looking for a teacher-researcher in formal methods in the field of hardware and software to join the ACES (Autonomous, Critical, Embedded Systems) team within the INFRES department.
Applicants should hold a PhD and be fluent in English, with strong theoretical or applied expertise at the crossroads of hardware and software, embedded systems, software engineering, or cybersecurity. Postdoctoral or international experience is appreciated.
The application deadline is February 27, 2026. More information about the job offer is available here .
The Institute of Computer Science of the Czech Academy of Sciences is opening a tenure track research position in computer science. Automated reasoning is explicitly mentioned as a relevant research keyword. The position is research-only, with teaching at local universities possible but not mandatory.
Application deadline is March 31, 2026. Further details about the position can be found here. For additional information, you may contact Stefan Ratschan.
We invite applications for a postdoctoral research position in programming languages and semantics, with a focus on NetKAT and related formalisms for reasoning about networks and systems.
The position is jointly sponsored by:
The successful candidate will work on foundational and applied aspects of NetKAT and related languages, including (but not limited to) semantics, logics, compilation, and connections to automata theory, category theory, and formal methods. The exact research direction is flexible and will be shaped jointly with the postdoc based on their interests and expertise.
The position offers a high degree of intellectual freedom and a unique opportunity to collaborate closely with researchers across EPFL, ETH Zürich, and Cornell University. The postdoc may spend extended time at one or more of these institutions, and flexible arrangements are possible to support sustained collaboration.
Candidates should have (or be close to completing) a PhD in Computer Science or a closely related field, with a strong background in programming languages, semantics, logic, verification, or formal methods. Experience with NetKAT or network verification is welcome but not required.
The position is expected to start in spring or fall 2026 (flexible). The initial appointment is typically for one year, with the possibility of renewal subject to performance and funding.
To apply, please send a CV, a brief statement of research interests, and the names of at least two references to: Nate Foster, Jules Jacobs, Dexter Kozen, Alexandra Silva.
Review of applications will begin immediately and continue until the position is filled.
Mistral AI is building a new formal mathematics team following our $2B funding round. We are looking for researchers and engineers at the intersection of formal math (Lean, Rocq, etc.) and AI.
The team works on creating a state-of-the-art prover, autoformalizer, and automatic proof agent, all integrated into a single model. Team members will join world-class researchers including Simon Sorg, Albert Jiang, Maxime Darrin, and Jason Rute, with support from Guillaume Lample.
Work environment highlights include:
To apply, send your CV and best work on AI and/or formal math to jason.rute@mistral.ai and aj@mistral.ai, using <formal> in the email title.
The Automated Reasoning Group in the AWS Neuron Compiler team is looking for an Applied Scientist to work on the intersection of Artificial Intelligence and program analysis to raise the code quality bar in our state-of-the-art deep learning compiler stack. This stack is designed to optimize application models across diverse domains, including Large Language and Vision, originating from leading frameworks such as PyTorch, TensorFlow, and JAX. Your role will involve working closely with our custom-built Machine Learning accelerators, Inferentia and Trainium, which represent the forefront of AWS innovation for advanced ML capabilities, and is the underpinning of Generative AI.
In this role as an Applied Scientist, you'll be instrumental in designing, developing, and deploying analyzers for ML compiler stages and compiler IRs. You will architect and implement business-critical tooling, publish cutting-edge research, and mentor a brilliant team of experienced scientists and engineers. You will need to be technically capable, credible, and curious in your own right as a trusted AWS Neuron engineer, innovating on behalf of our customers. Your responsibilities will involve tackling crucial challenges alongside a talented engineering team, contributing to leading-edge design and research in compiler technology and deep-learning systems software. Strong experience in programming languages, compilers, program analyzers, and program synthesis engines will be a benefit in this role.
A background in machine learning and AI accelerators is preferred but not required.
Basic qualifications include:
Preferred qualifications include:
More information and the full job posting can be found here .
A fully funded PhD position is available in the research group of Vineet Rajani at the University of New South Wales (UNSW) Sydney.
The candidate will broadly work in the area of programming languages and formal analysis, broadly construed. Depending on the interest of the applicant, possible research directions include building new methods (e.g. type theories or program logics) to reason about interesting properties (e.g. pertaining to security or privacy, secure and verified compilation, complexity/cost analysis) of programs (e.g. higher-order functional, imperative and/or probabilistic), including their mechanisation. More information about my work and research interests can be found here.
Information about the UNSW PhD program and the application process is available at here. The position is available immediately, and interested applicants are encouraged to contact Vineet Rajani before submitting a formal application.
We are seeking a highly-motivated Postdoctoral Fellow to join our team for the DARPA Bus-based Local Attack Detection and Elimination (BLADE) program, a groundbreaking collaborative project between UNC Charlotte, Electric Power Research Institute (EPRI) and NVIDIA, to secure critical hardware bus systems. This position will lead the formal methods and verification thrust, focusing on providing mathematical assurances for the security of bus-based communications.
Key Responsibilities:
Required Qualifications:
Preferred Qualifications:
To apply, please email the following materials to Dr. Meera Sridhar:
The LII team at ENAC is seeking a candidate for a PhD thesis on the formally verified compilation of the interaction-oriented programming language Smala in the Rocq prover. The work aims at developing an end-to-end verified compilation toolchain for interactive programs, with applications to critical systems such as avionics and air traffic control interfaces.
The ultimate goal of this research project is to provide an end-to-end formally verified toolchain for Smala, a fully-featured interaction-oriented language. To do so, we have identified several avenues to build on this preliminary work, at the level of semantics, verified compilation, and verification of source properties
The position is for a period of three years (starting in fall 2026) and may be preceded by an internship starting in spring 2026. Please check the offer description or contact Basile Pesin, Stéphane Conversy and Celia Picard for more information.