Deepak Kapur passed away on April 11, 2026 in Albuquerque, New Mexico, aged 75. He was one of the pioneers of automated reasoning, with outstanding contributions in numerous areas, including inductive theorem proving, geometry theorem proving, term rewriting, unification theory, integration and combination of decision procedures, lemma and loop invariant generation, as well as his work to bridge the gap between computer algebra and automated deduction.
After graduating from the Indian Institute of Technology (IIT) in Kanpur, Deepak earned his Ph.D. in 1980 at MIT under the supervision of Barbara Liskov. From 1980 to 1987 he worked at General Electric's Research Laboratory in Schenectady, New York, while also serving as an adjunct professor at Rensselaer Polytechnic Institute. He was appointed full professor at the University at Albany, State University of New York in 1988. In 1998, Deepak moved to the University of New Mexico (UNM) in Albuquerque, where he was Chair of the Computer Science Department until 2006 and was awarded Distinguished Professor in 2007.
In automated deduction, Deepak introduced one of the most influential approaches for automated program verification by induction, the "proof by consistency" method. This approach had an enormous impact on the further development of the field. His research covered both deep theoretical contributions and practical aspects concerning the application of his results. His induction theorem prover "Rewrite Rule Laboratory (RRL)" was very influential and was successfully used for numerous applications, in particular in hardware verification. Deepak's work on the foundations of RRL forms the basis of many modern theorem provers, since RRL was one of the first tools that successfully combined theorem proving and decision procedures.
Another topic of Deepak's work was termination analysis, in particular for systems where certain functions have additional properties like associativity and commutativity. His results on techniques for termination proofs of such systems had a wide influence and remain among the most powerful ones today.
Moreover, Deepak made fundamental contributions to several other topics in automated deduction, such as methods for unification, for proving sufficient completeness, etc.
In the area of computer algebra, Deepak developed very substantial contributions on algebraic and geometric reasoning. Here, his focus was on developing methods for solving geometric problems and for determining geometric quantities. Moreover, Deepak found a fascinating way to combine results from both computer algebra and automated deduction by using methods from algebraic geometry to generate loop invariants automatically.
His position as one of the leaders of automated deduction is demonstrated by the fact that he was the editor-in-chief of the Journal of Automated Reasoning from 1993 to 2007, he served as CADE program chair in 1992, and he received the Herbrand Award in 2009 in recognition of his seminal contributions to automated reasoning.
Deepak was also a very devoted teacher and mentor for both students and younger researchers. I was fortunate to spend a year working with him as a visiting researcher at UNM in 1999/2000. His advice, suggestions, and friendship have guided me ever since.
Deepak is survived by his wife Roli Varma and their daughter Ila.
We plan to hold a memorial session at IJCAR during FLoC in Lisbon, July 2026, where everybody is welcome to share memories of Deepak. If you would like to speak a few words during this session, please contact Jürgen Giesl by June 26, 2026.
The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning is presented to
for contributions to the foundations of type theory and logical frameworks, and the development of theory, automated tools, and applications for classical and non-classical logics.
Presented at IJCAR 2026, the 13th International Joint Conference on Automated Reasoning.
The 2026 Herbrand Award Committee consisted of Nikolaj Bjørner (Chair), Amy Felty, Cynthia Kop, Cláudia Nalon, Andrew Reynolds, and Geoff Sutcliffe.The International Conference on Automated Deduction (CADE) Bill McCune PhD Award in Automated Reasoning is presented to
for his dissertation “Cylindrical Algebraic Decomposition Based Methods in Satisfiability Modulo Non-linear Real Arithmetic” supervised by Prof. Dr. Erika Ábrahám and Prof. Dr. James Davenport. The thesis was selected for its strong theoretical contributions to SMT solving for non-linear real arithmetic. The thesis provides a uniform presentation of available algorithms based on the cylindrical algebraic decomposition (CAD) method for satisfiability checking and quantifier elimination; the CAD projection is formalized as a proof system, which allows the design of fine-grained optimizations. These theoretical results are not only important for the understanding, improvement, and applicability of exploration-guided CAD-based algorithms, but also proved to have impact on the development of practically relevant software.
Presented at IJCAR 2026, the 13th International Joint Conference on Automated Reasoning.
The 2026 Bill McCune PhD Award Committee consisted of Viorica Sofronie-Stokkermans (chair), Pascal Fontaine, Carsten Fuhs, Ullrich Hustadt, Mikoláš Janota, Cezary Kaliszyk, Philipp Rümmer, and Sophie Tourret.An honorary mention is given to
for his dissertation “Cardinality Constraints in Boolean Satisfiability Solving” supervised by Prof. Marijn Heule and Prof. Randal Bryant. The thesis was selected for its impact on the theory and practice of SAT solving. The thesis introduces KNF (AtLeastK Conjunctive Normal Form), an extension of conjunctive normal form with native cardinality constraint support, and develops native cardinality propagation and an efficient form of cardinality-guided formula splitting for parallel solving. The thesis makes a convincing case for enriching the input of SAT solvers with cardinality constraints by demonstrating the substantial performance improvements that can be achieved through cardinality-aware reasoning, even without using cutting planes.
Presented at IJCAR 2026, the 13th International Joint Conference on Automated Reasoning.
The 2026 Bill McCune PhD Award Committee consisted of Viorica Sofronie-Stokkermans (chair), Pascal Fontaine, Carsten Fuhs, Ullrich Hustadt, Mikoláš Janota, Cezary Kaliszyk, Philipp Rümmer, and Sophie Tourret.After eight years of excellent service, Philipp Rümmer has resigned from the posts of CADE and AAR secretary. The CADE Board of Trustees and the AAR Board want to thank him for his outstanding service to the community!
Our new CADE and AAR secretary is Sophie Tourret. We welcome Sophie in her new role and look forward to working with her.
The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, choosing the Herbrand, Bill McCune, and Skolem Award selection committee, instituting new awards, etc.
Nominations for four CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2026.
The current members of the board of trustees are (in alphabetical order):
The terms of Jasmin Blanchette, Carsten Fuhs, and Renate Schmidt end. Jasmin Blanchette and Carsten Fuhs may be nominated for a second term, whereas Renate Schmidt has already served two consecutive terms and cannot be nominated this year.
The term of office of Armin Biere as IJCAR 2026 programme chair ends after the IJCAR conference. As outgoing ex-officio trustee, Armin Biere is eligible to be nominated as elected trustee.
Sophie Tourret has become CADE secretary. Her position as an elected trustee is thus also open.
In summary, we are seeking to elect four trustees.
Nominations can be made by any CADE member, either by e-mail or at the business meeting at IJCAR 2026; since nominators must be CADE members, they must have participated in at least one of the CADE or IJCAR conferences in the years 2023-2026. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. For further details please see the CADE Inc. bylaws at the CADE web site.
E-mail nominations can be provided up to the upcoming IJCAR business meeting, via email to
Jürgen Giesl, President of CADE Inc.with copies to
Sophie Tourret, Secretary of CADE Inc.
We invite proposals for sites to host the 14th International Joint Conference on Automated Reasoning (IJCAR) to be held in the summer 2028. Previous IJCAR meetings include IJCAR 2001 in Siena, Italy; IJCAR 2004 in Cork, Ireland; IJCAR 2006 as part of FLoC in Seattle, Washington; IJCAR 2008 in Sydney, Australia; IJCAR 2010 as part of FLoC in Edinburgh, Scotland; IJCAR 2012 in Manchester, UK; IJCAR 2014 as part of FLoC and the Vienna Summer of Logic in Vienna, Austria; IJCAR 2016 in Coimbra, Portugal; IJCAR 2018 as part of FLoC in Oxford, UK; IJCAR 2020 in Paris, France, as online event; IJCAR 2022 as part of FLoC in Haifa, Israel; IJCAR 2024 in Nancy, France; and IJCAR 2026 as part of FLoC in Lisbon, Portugal.
IJCAR is a merger of CADE (Conference on Automated Deduction), TABLEAUX (Conference on Analytic Tableaux and Related Methods), and FroCoS (Symposium on Frontiers of Combining Systems) and possibly other meetings. Usually, a considerable number of workshops are also affiliated with the conference.
The deadline for proposals is July 6, 2026. Proposals should be sent to the IJCAR Steering Committee Chair. We encourage proposers to register their intention informally as soon as possible.
Proposals should address the following points that also represent criteria for evaluation:
Information about the previous IJCAR conferences (including organizers, number of accepted papers, number of registrations) can be found at https://ijcar.org//conferences.
Please also take into account the Conference management notes at https://cadeinc.org//Schedule and the financial summaries of previous conferences at https://cadeinc.org//FinancialSummaries.
The Federated Logic Conference (FLoC) 2026 brings together major conferences, workshops, and summer schools in logic and computer science.
| Category | Early | Late |
|---|---|---|
| Conferences | May 15 | July 13 |
| Workshops | June 1 | July 13 |
| Summer School | June 1 | July 6 |
| Dates | Category | Events |
|---|---|---|
| July 13–17 | Summer Schools | FoPSS, SAT/SMT/AR Summer School |
| July 17–19 | 3-Day Workshops | DL, NMR |
| July 18–19 | Workshops | MW1, LSFA, ML4SP, FMQC, OVERLAY, TGD, TLLA, PoS, RocqWS, TERMGRAPH, ThEdu, WHOOPS, WPTE, ... |
| July 20–23 | Week 1 Conferences |
CP, FSCD, ICLP, KR, LICS, SAT |
| July 24–25 | Workshops | MW2, ARQNL, IWC, Isabelle, LFMTP, SMT, TPTPTP, UNIF, VAMPIRE, WiL, AR4Space, CompBench, HCVS, Lean, PAAR, TEAL, WST, Rocqshop, ... |
| July 26–29 | Week 2 Conferences | CAV, CSF, IJCAR, ITP |
The formal verification of multi-agent systems aimed at proving that such systems meet their specifications has given rise to a very active field of research at the crossroads of formal methods, knowledge representation and artificial intelligence. Alternating-time temporal logics are considered as one of the most popular and influential logical formalisms for strategic reasoning in multi-agent systems and have been introduced by Rajeev Alur, Thomas Henzinger and Orna Kupferman about 25 years ago.
This textbook provides a concise presentation of alternating-time temporal logics devoted to strategic reasoning in multi-agent systems. Dedicated mainly to the model-checking problem, the work examines developments about basic semantical properties of such logics, decision procedures and computational complexity. It provides results for solving optimally the model-checking problem on concurrent game structures by taking advantage of—or adapting proof methods from—temporal logics, games in theoretical computer science and automata theory.
Further information can be found here.
Nominations are invited for the 2026 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2025 and 31 December 2025 are eligible for nomination for the award.
The deadline for submission is July 1, 2026.
Nominations
Nominations should be submitted by the candidate or the
supervisor via Easychair.
Procedure
Please submit a pdf file containing:
The Award
The 2026 Ackermann award will be presented to the recipient(s)
at CSL 2027.
The award consists of a certificate, an invitation to present
the thesis at the CSL conference, the publication of the
laudatio in the CSL proceedings, and financial support to
attend the conference.
The Ackermann Award 2026 is sponsored by Amazon Automated Reasoning.
Ackermann Jury
The jury consists of:
For more information please contact Maribel Fernandez.
This prize was recently reestablished with support from the AI For Math Fund, which is run by Renaissance Philanthropy and funded by XTX Markets. The goal of the prize is to highlight and celebrate influential work and to encourage formal verification throughout mathematics and its applications. The work can be published in a recognized journal or code repository or other comparable database of record.
Nominations are accepted from March 20 to June 30, 2026.
More information is available on the prize's web page.
FMPSI'26 is a two-week meeting aiming at gathering experts in formal mathematics and proof systems interoperability in order to discuss recent advances and make concrete progress on the formalization of advanced mathematics, the management of collaborative development of large libraries of proofs, the certification of proofs generated by automated theorem provers, the translation of definitions, theorems and proofs between different interactive theorem provers, and the use of proof assistants in teaching. There will be three working groups: one on proof systems interoperability, one on formal mathematics, and one on computer algebra.
In the second week (June 29–July 2), the 2nd edition of PAT 2026 (Proof Assistants for Teaching) is co-organised. PAT aims to bring together researchers, teachers, students, and stakeholders interested in the use of proof assistant for teaching. PAT seeks to offer a broad spectrum of current research in the field of didactic of proof, the impact of the use of proof assistants in education, formalization of mathematics and user interfaces for theorem proving. The objective is to gather three audiences: researchers in didactics of mathematics or informatics who would like to learn how and why use proof assistants in class; mathematicians who would like to learn how to use proof assistants for their research and teaching; specialists of proof assistants, who want to learn more about the didactic of proof and proving in mathematics. Remote participation is possible.
More information is available on the FMPSI and PAT web pages.
Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
The Alpine Verification Meeting (AVM) is an informal meeting on current problems in formal verification, bringing together researchers from the Alpine and surrounding regions to discuss ongoing work and foster collaborations. The format encourages short presentations and discussion of work in progress.
More information is available on the event's web page.
ICFEM is an internationally leading conference series in formal methods and software engineering. Since 1997, ICFEM has served as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners from industry, academia, and government are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, as well as in theoretical work that promises to bring practical and tangible benefits.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
The International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is an academic conference aimed at discussing cutting-edge results in the fields of automated reasoning, computational logic, programming languages and their applications. Papers from previous proceedings are listed in DBLP. LPAR's slogan is "To boldly go where no reasonable conference has gone before". LPAR brings first class research and researchers to interesting places, and exposes the conference attendees to interesting cultures.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
The Working Formal Methods Symposium (FROM) aims to bring together researchers and practitioners working on formal methods by contributing new theoretical results, methods, techniques, and frameworks, and/or by creating or using software tools that apply theoretical contributions. The program includes invited lectures and regular contributions.
Areas of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the symposium's web page.
The ICTAC conference series aims at bringing together researchers and practitioners from academia, industry, and government to present research and exchange ideas and experiences within theoretical aspects of computing through methods and tools for system development. ICTAC also aims to promote research cooperation between developing and industrial countries.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
The aim of ICTCS is to foster cross-fertilization of ideas across different areas of theoretical computer science and to provide an environment where junior researchers and PhD students can interact with senior researchers.
Topics of interest include (but are not limited to):
ICTCS 2026 includes three special tracks devoted to significant application domains of theoretical computer science. The aim is to solicit contributions that, while not primarily situated within theoretical computer science, address substantive theoretical questions emerging from applied research problems. The three special tracks are as follows:
Important Dates (AoE)
More information is available on the conference's web page.
SEFM aims to bring together researchers and practitioners from academia, industry, and government to advance the state of the art in formal methods, to facilitate their uptake in the software industry, and to encourage their integration within practical software engineering methods and tools.
Topics of interest include (but are not limited to):
Software development methods:Important Dates (AoE)
More information is available on the conference's web page.
The aim of the symposium is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The symposium covers an ample spectrum of themes, ranging from theory to applications, and encourages cross-fertilization. Papers focused on formal methods are especially welcome. Papers discussing new ideas that are at an early stage of development are also welcome.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the symposium's web page.
RP is specifically aimed at gathering together scholars from diverse disciplines and backgrounds interested in reachability problems that appear in:
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
The Colloquium Logicum is organized every two years by the DVMLG (Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften). The next edition will be held in Würzburg and will cover the whole range of mathematical logic and the foundations of the exact sciences. In addition to the keynote talks, there will be a PhD Colloquium with invited presentations of excellent recent PhD graduates.
The submission deadline for abstracts is June 30, 2026 (AoE).
More information is available on the conference's web page.
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.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation.
VSTTE 2026 welcomes submissions describing significant advances in the production of verified software, i.e. software that has been proved to meet its functional specifications. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We also welcome papers describing novel experiments and case studies evaluating verification techniques and technologies.
Following its success in VSTTE 2025, we also welcome submissions on in-progress verified software projects to a "work-in-progress (presentation-only)" track.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
Trends in Logic is the conference series of the journal Studia Logica. This year's edition is dedicated to recent developments in non-classical logics, non-classical mathematics and related philosophical questions.
Important Dates (AoE)
Submissions of extended abstracts (up to three pages) should be sent as PDF to Sara Ayhan and Hitoshi Omori.
More information is available on the conference's web page.
ETAPS 2027 is the thirtieth edition of one of the primary fora for academic and industrial researchers working on topics relating to software science. ETAPS is a confederation of four annual conferences accompanied by satellite workshops taking place during the weekend before the main conferences (April 10–11, 2027).
A new development in 2027 is the introduction of iFS (International Conference on Foundations and Formal Methods for Software and Systems), formed through the merger of FASE and iFM.
Main Conferences (April 12–15, 2027)
Important Dates (AoE)
More information is available on the conference's web page.
David Basin is turning 65 in December 2026, and this has to be celebrated! A Festschrift and a one-day Fest are organized to celebrate his birthday and his extensive research contributions.
Contributions are welcome in all areas close to David's research and interests, including but not limited to security, privacy, formal methods, logic, automated reasoning, model checking, theorem proving, software engineering, bridge, juggling, biking and more. Research articles are of course welcome, but short personal articles celebrating the history and friendship with David will be very much appreciated as well. Articles will be lightly reviewed by the Festschrift committee, and the proceedings will be published in the LNCS series.
Important Dates (AoE)
More information is available on the event's web page.
The annual meeting Deduktionstreffen is the prime activity of the Interest Group for Deduction Systems (FGDedSys) of the AI Chapter (FB KI) of the German Informatics Society (Gesellschaft für Informatik). It is a meeting with a familiar, friendly atmosphere, where everyone (not only the German community) interested in deduction can report on their work in an informal setting.
A special focus of the Deduktionstreffen is on young researchers and students, who are particularly encouraged to present their ongoing research projects to a wider audience. Another goal of the meeting is to stimulate networking effects and to foster collaborative research projects.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the workshop's web page.
The Workshop on Proof Mining is the second instance of a workshop series dedicated to providing opportunities for people from the diverse areas connected to proof mining to meet, present work in progress, and exchange ideas and knowledge. The meeting is interdisciplinary in nature, with a particular focus on:
If you are interested in participating in the workshop, please contact Nicholas Pischke or Thomas Powell for registration. The meeting will take place in person. Please note that talks are by invitation only.
Important Dates (AoE)
As an ASL sponsored workshop, graduate students who are members of the ASL are eligible to apply for modest student travel awards to attend the meeting. Please read the ASL guidelines here.
More information is available on the workshop's web page.
FMAS is a 2-day peer-reviewed international workshop that brings together researchers working on a range of techniques for the formal verification of autonomous systems to present recent work in the area, discuss key challenges, and stimulate collaboration between autonomous systems and formal methods researchers.
Autonomous systems present unique challenges for formal methods. They are often embodied in robotic systems that can interact with the real world, and they make independent decisions. Amongst other categories, they can be viewed as safety-critical, cyber-physical, hybrid, and real-time systems.
Key challenges for applying formal methods to autonomous systems include:
FMAS welcomes submissions that use formal methods to specify, model, or verify autonomous systems; in whole or in part. We are especially interested in work using integrated formal methods, where multiple (formal or non-formal) methods are combined during the software engineering process. We encourage submissions that are advancing the applicability of formal methods for autonomous systems, for example improving integration or explainability, automation or knowledge transfer of these technique.
Autonomous systems are often embedded in robotic or cyber-physical systems, and they share many features (and verification challenges) with automated systems. FMAS welcomes submissions with applications to automated systems, semi-autonomous systems, or fully-autonomous systems.
Topics of interest include (but are not limited to):
In addition to the topics above, we would like to invite work on formal methods for intersymbolic AI. Intersybolic AI refers to the combination of symbolic AI (logic, knowledge graphs, etc.) and subsymbolic AI (neural networks, reinforcement learning, etc.).
Important Dates (AoE)
More information is available on the workshop's web page.
Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR) continue to make rapid advances and find novel uses in a wide variety of applications, in computer science and beyond. The SAT/SMT/AR Summer School aims to bring a select group of students up to speed quickly in this exciting research area.
Limited financial support is available for students. To be considered, please fill out this additional short form.
Important Dates (AoE)
More information is available on the school's web page.
An international autumn school "Proof and Computation" will be held at Aurachhof in Fischbachau near Munich. Its aim is to bring together young researchers in the fields of Foundations of Mathematics, Computer Science and Philosophy.
Scope:
Courses:
Celebrating the 10th edition, there will be 3 additional evening lectures:
There will be an opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of constructing correct programs from proofs.
Important Dates (AoE)
More information is available on the school's web page.
The 2026 Foundations of Programming and Software Systems (FoPSS) Summer School brings together students and researchers to explore "Emerging Approaches for Reasoning about Programs and Proofs." This year's edition is dedicated to recent methodologies spanning advanced type systems, proof assistants and logic, and neurosymbolic approaches that are actively shaping the frontier of software verification and program semantics.
The program features a distinguished series of lectures designed to equip participants with both a solid grounding in established foundations and a forward-looking perspective on the field's future. By diving into highly active research areas, attendees will gain the theoretical tools necessary to reason rigorously about complex, modern programs. Through engaging instruction and collaborative discussions, the school aims to inspire the next generation of researchers to push the boundaries of what is possible in formal reasoning and program verification.
Early registration deadline is June 1, 2026 (AoE).
More information is available on the school's web page.
The school is aimed at master and PhD students, researchers and practitioners interested in the study of rewriting concepts and their applications. The school offers two different tracks:
Early registration deadline is June 2, 2026 (AoE).
More information is available on the school's web page.
MOVEP'26 is a five-day school at the intersection of concurrency, model checking, and formal verification. It will feature 6 tutorials (long courses) and 4 technical presentations (short courses) by world-leading researchers, as well as sessions allowing participants to present and discuss their own work.
Speakers and courses:
Important Dates (AoE)
More information is available on the school's web page.
The Scottish Programming Languages and Verification Summer School is a collaborative effort between the Universities of Edinburgh, Glasgow, Heriot-Watt, Strathclyde and St Andrews. This summer school provides core and advanced classes that cover foundational as well as state of the art knowledge on the underlying principles needed to use or design new languages and verifying program correctness.
This school aims to:
The early registration deadline is June 30, 2026 (AoE).
More information is available on the school's web page.
The summer school offers intensive courses by leading researchers covering foundational and applied topics at the intersection of programming languages, formal methods, and software security. It is aimed at PhD students and advanced B.Sc./M.Sc. students active in the areas of programming languages, logic, semantics, and software security.
Courses and Speakers:
Application deadline is June 7, 2026 (AoE).
More information is available on the school's web page.
This special issue celebrates the 10th anniversary of the Women in Logic Workshop and aims to highlight a decade of contributions by women to the development of logic and its applications. The first author must be a female researcher or a researcher identifying as female. Submissions should be written in English (maximum 25 pages including references and appendices) and prepared using the template available here. The PDFs of the submissions should be sent via e-mail to Jane Spurr with "JLC Submission - WiL10" in the subject line by August 15, 2026 (AoE). Submissions must present original, unpublished work.
Topics of interest include but are not limited to:
All submissions will be subject to the standard peer-review process of the Journal of Logic and Computation and must comply with the journal's author guidelines.
For any enquiries regarding suitability or submission, please feel free to contact the guest editors: Huimin Dong, Anela Lolic and Elaine Pimentel.
During the 90's a number of new, powerful termination methods was developed. Thus, at the beginning of the millennium many research groups started to develop tools for fully-automated termination analysis.
After a tool demonstration at the Termination Workshop 2003 (Valencia), the community then decided to install an annual termination competition, and to collect benchmarks, to spur the development of tools and new termination techniques.
The competition will be run on the RWTH Aachen High Performance Computing Cluster. Test runs will take place right after the submission deadline, followed by a bug/conflict reporting phase. Bug fixes will be possible until shortly before the full run. A live run on a subset of the benchmark collection, and a presentation of the final results will take place at WST.
Important Dates (AoE)
More information is available on the competition's web page.
ProoVer-2026 is the first edition of the annual competition for automatic proof verifiers. In ProoVer, verifiers are given a mix of valid proofs and evil proofs in which tricky errors have been deliberately introduced. The goal is to correctly identify which proofs are valid and which are flawed.
Participants submit proof verifier systems that receive FOF (First-Order Form) problems paired with TSTP-format proofs, and must determine whether each proof is valid or flawed. For this first edition, only a limited set of inference rules and formula roles will be used: Axiom, Conjecture, NegatedConjecture, Skolemization, as well as plain steps whose correctness should be delegated to an external ATP. Each system is evaluated on 100 problems: 50 valid proofs and 50 evil proofs, with a time limit of 30 seconds per problem (wall-clock). The competition infrastructure is shared with CASC (StarExec).
As ProoVer is held jointly with CASC, we will have a shared dinner and if you participate in both competitions, registration fees are charged only once.
Important Dates (AoE)
More information is available on the competition's web page.
The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-J13 will be held on the 27th July 2026, during the 13th International Joint Conference on Automated Reasoning.
CASC evaluates the performance of sound, fully automatic ATP systems in terms of:
in the context of:
The competition organizer is Geoff Sutcliffe. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event.
Registration of systems for CASC-J13 is now invited. System registration deadline is June 29, 2026 (AoE). Please register early so that adequate resources can be allocated.
DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW!
More information is available on the competition's web page.
Department of People and Technology, Roskilde University (RUC), invites applications for a position as assistant professor of Computer Science from the 1st of November 2026 or as soon as possible thereafter. The position is limited to a period of 3 years.
Department of People and Technology is the largest department at Roskilde University and covers a range of subject areas, broadly focused on human – society – technology interactions and covering topics as sustainable transitions of society, social entrepreneurship, urban planning, computer science, digitalization, healthcare, welfare studies, etc. The position is linked to the research group Programming, Logic, and Intelligent Systems (PLIS). In PLIS, basic research in computer science is combined with innovative applications. The research in the PLIS group concerns the following topics:
Applicants must hold a PhD degree within computer science or a closely related field. The successful candidate will become a member of the PLIS research group and must relate their research to that of the PLIS group. Specifically, we are seeking applicants with a research and teaching profile in more than one of the following scientific areas:
The candidate is expected to master Danish (or Swedish/Norwegian) to a degree sufficient to teach and supervise in Danish and participate in administrative and collegial cooperation. Applicants not mastering Danish are expected to follow classes and reach an acceptable level of Danish during the assistant professorship. Applicants are also required to be able to research, teach, and supervise in English.
The application deadline is June 1, 2026.
For further information about the position, please contact head of the PLIS group Torben Braüner, head of studies Maja Hanne Kirkeby, or head of section Morten Hertzum, or see the job offer.
A PhD position is available in the newly formed group CALM (Coalgebra, Algebra, and Logical Methods) at the Department of Computer Science, University of Salzburg.
The position is a university assistant position for 4 years, with all benefits (and a small teaching obligation in year 2 and year 3). The topic of research will be fixed based on the joint interests of the candidate and the supervisor, within the mentioned areas.
The intended (yet flexible) starting date is October 1, 2026. A prerequisite is a Master's degree in Computer Science or Mathematics or a related field, and a strong background in theory (formal methods, semantics).
Applications are considered on a rolling basis until the position is filled, ideally before August 2026. Please send an informal application with a CV and a statement of research interests to Ana Sokolova.
A one-year postdoctoral position (renewable) is available in the CAPP group at the Computer Science Laboratory of Grenoble (LIG). The position focuses on the formalization of protocols in decentralized finance within the proof assistant Isabelle/HOL, with the goal of developing rigorous theoretical results and certified tools for optimizing decentralized finance transactions. The LIG is one of the leading computer science research laboratories in France, located on the University Grenoble Alpes campus, at the foot of the Alps. The CAPP group research lies at the intersection of logic, programming languages, and proofs.
Automated Market Makers are the cornerstones of Decentralized Finance (DeFi), eliminating the need for traditional order books. In this ecosystem, Liquidity Providers stake tokens to facilitate swaps for Liquidity Takers in exchange for fees. Concentrated Liquidity Market Makers (CLMMs), introduced by Uniswap v3, have revolutionized this space by allowing providers to allocate liquidity within specific price intervals. This model significantly improves capital efficiency compared to uniform distribution models and has been adopted by several major protocols. Despite implementation variations (fees, tick spacing), these protocols share core principles. Consequently, liquidity takers often face multiple pools for the same token pair with different characteristics. A critical challenge is to rigorously understand how these pools can be combined, both conceptually and computationally, for liquidity takers to perform transactions with the least slippage (recovering as many tokens as possible in exchange for those they provide).
Decentralized finance refers to a set of peer-to-peer exchange protocols designed to minimize the dependence on intermediaries and central authorities. As DeFi becomes increasingly important in modern economies, establishing rigorous theoretical foundations for its core mechanisms is essential. The project aims to develop a rigorous formal framework for reasoning about the behavior of Concentrated Liquidity Market Makers and optimizing execution of transactions across multiple pools. A significant formalization effort regarding the behavior of CLMMs in Isabelle/HOL has already been initiated within the group. The recruited postdoctoral researcher will be responsible for advancing this work.
The primary objectives are:
Candidates should have a strong background in Logic, Formal Methods, Proof Theory, or Semantics. Experience with proof assistants (e.g., Coq, Lean, Isabelle/HOL) or formal verification tools, as well as familiarity with DeFi concepts (AMMs, Smart Contracts) are also welcomed.
The start date is flexible, but ideally, as soon as possible. Interested candidates should send their CV, a cover letter, links to their thesis and/or relevant papers, and contact information for two references to Mnacho Echenim and Nicolas Peltier.
A PhD position is open on the formal verification of distributed systems with respect to liveness properties using reinforcement learning techniques.
Mitsubishi Electric R&D Centre Europe and Irisa / Inria Rennes are interested in developing algorithms for automatically proving the absence of livelocks or detecting livelocks bugs in distributed protocols using reinforcement learning algorithms. We suggest developing deep RL algorithms to analyze maximal wait times in distributed protocols. The wait time is the number of steps a process is executed before it gains access to a resource. There are no livelocks if the wait times are always finite. The work consists in modeling this problem as an RL problem, choosing the right rewards and RL algorithms, and making sure it scales to real implementations of distributed algorithms.
Because the overall goal is formal verification, the computed neural policy must be formally verified at the end. This can be achieved using SMT solvers or specific abstract interpretation techniques for neural networks.
The model and RL algorithms can be chosen either to attempt to prove the absence of livelocks and compute bounds on wait times, or to detect livelock bugs. The precise direction to be taken and the weight given to RL versus formal verification in this work can be chosen according to the student’s background and preferences.The work also includes an extensive bibliographic study, the development of the above algorithms, implementation and experiments.
The successful candidate must have an excellent theoretical background in formal methods (or alternatively in reinforcement learning), good programming skills, knowledge (course work, internship, or master's thesis) in at least one of the two fields: reinforcement learning, and formal verification or logic, previous research experience (e.g., internships), strong references, and a strong motivation to learn.
For more information or to apply, see the job offer .
The Automated Reasoning Group at AWS in Cambridge is seeking internship candidates to work on formal verification of low-level systems software. Among other things, the hosting team is responsible for the formal verification of the Nitro Isolation Engine, a new separation kernel for Graviton cloud instances.
The ideal candidate is a student towards the end of their PhD with a strong background in interactive theorem proving, ideally but not necessarily Isabelle, and some familiarity with systems programming, ideally in Rust. Details are TBD, but potential topics include hands-on proof development, refining our large-scale separation logic proof automation, or improving AI / ITP integration.
Interested candidates should reach out directly to Hanno Becker.
Nectry is building the governance layer for AI-generated code in regulated enterprises. Our core technology, NectryCore, is a purpose-built DSL and compiler that makes formal verification and policy enforcement structurally guaranteed, not bolted on. We're a small, ambitious team, and we're looking for an engineer who loves type systems, takes ownership, and wants to use AI tools to build things that actually have to be correct.
You'll work across our stack on language design, tooling, and product engineering. Most of our application code is written in Ur/Web, a statically-typed functional language for web programming. We don't expect you to know Ur/Web on day one, but we expect you to be the kind of engineer who picks up an unfamiliar functional language quickly.
This is a senior, high-autonomy role: you'll scope your own work, own systems end-to-end, and shape technical direction alongside our co-founders, including our Chief Scientist Adam Chlipala (MIT professor, creator of Fiat Cryptography and Ur/Web).
To apply, send a short note about what you have been working on, why functional programming matters to you, and anything you are proud of (code, papers, projects). More information is available on the job offer page.