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 2024 elections were:
The terms of the elected trustees Cláudia Nalon and Stephan Schulz ended in 2024. The term of office of Christoph Benzmüller as IJCAR 2024 program co-chair ended after the IJCAR conference, and Uwe Waldmann is joining the board of trustees as CADE-30 program co-chair.
In the 2024 elections, two new trustees had to be elected.
The following candidates were nominated and their statements, in alphabetical order, are below:
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 262 ballots were sent out on August 28. By September 15, 79 CADE members had voted through CIVS, which translates to a participation rate of 30.2% (as compared to 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 two candidates elected are Marijn Heule and Martin Suda.
The new board of trustees is therefore:
On behalf of CADE Inc., I would like to thank Cláudia Nalon and Stephan Schulz for their service for CADE over the last three resp. six years, and Cláudia Nalon for running in the 2024 elections. I would like to congratulate Marijn Heule and Martin Suda, who will join the board as new elected trustees.
CADE and IJCAR, along with SAT, are my favorite conferences due to their stimulation of exciting and important research. Since 2012, I have had the pleasure of participating in most CADE and IJCAR conferences and serving on several of their program committees, including co-chairing IJCAR'24. Additionally, I was honored to serve as a trustee from 2017 to 2022.
My research focuses on two significant challenges in automated deduction: validating the correctness of complex techniques developed by the community and leveraging the power of large computer clusters. Although my work primarily targets SAT and QBF solving, these challenges are also crucial for first-order logic and beyond. I am particularly interested in promoting the application of successful techniques from propositional logic to richer logics.
The community has developed powerful tools such as CaDiCaL, Vampire, and Z3, which have also found success in industry. I support encouraging paper submissions that demonstrate the impact of these tools on solving relevant problems, as such papers can have a broad impact. Furthermore, I advocate for the requirement that experimental evaluations be reproducible by reviewers and the wider community.
I strongly believe that all future publications in automated reasoning, including CADE/IJCAR proceedings and JAR articles, should be Open Access. This approach enhances accessibility and can expand the community. Although there are concerns about the financial impact on authors and participants, I believe we can address these through sponsorships and agreements with funding agencies. I favor using LIPIcs for conference proceedings over LNCS, due to ongoing issues with Springer, including typesetting. A recent community survey showed overwhelming support for LIPIcs, and as a trustee, I will push to implement this change.
The current structure of alternating yearly between CADE and IJCAR and joining FLOC every four years strikes the right balance between focusing on our community and maintaining visibility with related communities. I support coordinating the locations of CADE/IJCAR/FLOC conferences to improve geographic distribution. Despite most CADE attendees being from Europe, I am committed to encouraging participation from North American researchers. Thus, it is important to continue organizing CADE/IJCAR regularly in the US or Canada.
I am honoured and excited to be nominated once again to serve on the CADE's Board of Trustees. I have actively participated in both CADE and IJCAR for many years. I contributed both research and tool papers to either conference, served as a PC member several times, and helped with the organisation of the first edition of CADE in South America. I also have experience as a PC member, chair, SC member and organiser for other conferences in our field.
My research is focused on both the theoretical foundations and practical aspects related to the implementation of proof methods for non-classical logics and their combinations. CADE and IJCAR are (and should remain) welcoming venues for research encompassing a broad range of logics and techniques. I feel at home here and I am deeply committed to this community. As an enthusiastic implementer, I advocate for the increase of submission numbers of system and tool papers, and for introducing demo sessions for tools at the conference. This is not only important in my field, but more generally, as it encourages and celebrates the hard work of producing these tools.
I very strongly believe that a better geographical distribution of conference sites for CADE would be beneficial to our community. It will help to stimulate research and disseminate knowledge about automated reasoning and also attract talented individuals from regions that are not well represented in our field at present. We need to be sensitive to the fact that in those areas funding is often not available, and both researchers and students may have difficulties with meeting travel expenses and registration fees. I therefore support continuing the Bledsoe Award, to support students, and exploring options for reduced registration fees.
Costs are important. I support maintaining open access to the CADE proceedings to ensure the broad dissemination of our research. Open access is not for free, though, and we need to be mindful of what serves our community best and carefully evaluate cost-effective options. The consultation made by the current Board of Trustees already gives us a direction. However, it is also crucial to consider the impact of any changes to our sister conferences, TABLEAUX and FroCoS, which we join every two years to form IJCAR. I support therefore that we continue with discussions with their steering committees, as decided in our recent meeting in Nancy, before making any decision.
Thank you for considering my nomination. I am looking forward to the opportunity to continue contributing to our community.
I am honored to be nominated for the CADE Board of Trustees. CADE-22 (Montreal, 2009) was my very first serious conference and, with one exception, I took part at CADE and IJCAR ever since. I have served on the program committee of these conferences for the last six years. Since 2023, I am also a member of the steering committee of CADE's sibling FroCoS.
My current primary research interest is automated theorem proving and how it can be boosted through the techniques of machine learning. In the past, I also worked on temporal reasoning, SAT/QBF, and model finding. I am one of the main developers of the award-winning automatic theorem prover Vampire.
I am generally happy with the scope of CADE, catering for a wide range of topics, for both theoretical papers and those with focus on implementation. I like the regular merging with neighboring conferences on even years, which ensures we keep close contact with related fields. I also more than agree with the continuous support of young researchers, be it in the form of the Woody Bledsoe Student Travel Award, the Bill McCune PhD award, or in organizing the SAT/SMT/AR summer school.
The transition to the open access publication model was a step in the right direction. However, I believe that lower publication fees and less copy editing from the side of the publisher would improve our situation further. I understand that some funding agencies or career promotion committees may regard LNCS as prestigious, while they have not heard of LIPIcs yet, but that is a separate battle that we should fight elsewhere. For instance, by making sure CADE maintains or even improves on its current CORE ranking.
Principles of Programming Languages (POPL) is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation, or application of programming languages.
The early registration deadline is December 20, 2024. You can register here.
More information is available on the conference's web page.
CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including logical foundations, theory and principles, applications in and beyond computer science and mathematics, and implementations of automated reasoning systems are solicited. CADE-30 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction.
Important Dates (AoE)
More information is available on the conference's web page.
The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) brings together researchers interested in all aspects - theoretical foundations, implementation techniques, systems development and applications - of the mechanization of reasoning with tableaux and related methods.
Topics of interest include (but are not restricted to):
Important Dates (AoE)
More information is available on the conference's web page.
The symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly constructed. LICS 2025 invites submissions on topics that fit under that rubric.
Suggested, but not exclusive, topics of interest include:
Important Dates (AoE)
More information is available on the conference's web page.
The conference covers all aspects of formal structures for computation and deduction, from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logic, models of computation, semantics and verification in new challenging areas.
The suggested, but not exclusive, list of topics for submission is:
Important Dates (AoE)
FSCD also invites proposals for workshops on topics of interest to the FSCD community. Proposals must be
submitted as a PDF of at most three pages, not including references by email.
The workshop committee will determine the final list of accepted workshops based on thematic pertinence and
time/space
availability.
Important Dates (AoE)
More information is available on the conference's web page.
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry requires advanced technologies to address their specification, design, verification, validation, and certification. The NASA Formal Methods Symposium is a forum to foster collaboration between theoreticians and practitioners from NASA, other government agencies, academia, and industry, with the goal of identifying challenges and providing solutions towards achieving assurance for such critical systems. The focus of this symposium is on formal techniques for software and system assurance for applications in space, aviation, robotics, and other NASA-relevant critical systems.
The suggested, but not exclusive, list of topics for submission is:
Important Dates (AoE)
More information is available on the conference's web page.
The conference is the 37th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. CAV considers it vital to continue spurring advances in hardware and software verification while expanding to new domains such as machine learning, autonomous systems, and computer security. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. A selection of papers is expected to be invited to a special issue of Formal Methods in System Design and the Journal of the ACM.
Topics of interest include but are not limited to:
Important Dates (AoE)
More information is available on the conference's web page.
The SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software but does not exclude the analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, and empirical evaluation.
Topics of interest include, but are not limited to:
SPIN 2025 will feature artifact evaluation, performed by an Artifact Evaluation Committee (AEC). The AEC evaluates artifacts based on documentation, availability, reproducibility of results, and tool reusability (if applicable). Artifact submission is mandatory for Full Tool Papers. While artifact submission is optional for papers in other categories, we highly encourage authors of papers involving tool development and empirical evaluation to submit an artifact for evaluation. Papers with an accompanying artifact may be awarded one or more badges from the EAPLS artifact badging scheme.
Important Dates (AoE):
More information is available on the conference's web page.
TASE 2025 aims to bring together researchers and developers from academia and industry with interest in the theoretical aspects of software engineering. Modern society is increasingly dependent on software systems that are becoming larger and more complex. This poses new challenges to current software engineering methodologies that need to be enhanced using modern results from theoretical computer science. We invite submission of research papers on topics covering all theoretical aspects of software engineering, including those describing applications of theoretical computer science in industrial applications and software engineering methodologies.
Authors are invited to submit high quality technical papers describing original and unpublished work in 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.
WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers.
Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are:
Important Dates
More information is available on the workshop's web page.
Machine learning (ML) has been shown to be very successful in programming and translation talks, and creates new opportunities combining AI with proofs. Recently, various claims have been made that large language models (LLMs) will revolutionise these areas. However, many questions about the details of the applications of LLMs and their impact on theorem proving and mathematics remain open. At the workshop, we want to bring together researchers from a wide range of communities: mathematics, automated and interactive theorem proving, machine learning, natural language processing, and formal methods, in order to discuss the state-of the-art and future directions for this new area of research.
Examples of topics that we intend to discuss include, but are not limited to:
Important Dates
More information is available on the workshop's web page.
The Journal of Logical and Algebraic Methods in Programming (JLAMP) is an international journal that complements Elsevier's Science of Computer Programming and Theoretical Computer Science by its focus on the foundations and the application of logical, algebraic and categorical methods to programming and to the development of trustworthy computing systems. The aim of JLAMP special issues is to attract high-quality research papers in specific topics connected to logical and algebraic methods in the theory and practice of software development and computing systems.
The purpose of this special issue of JLAMP is to collect recent, original, and high-quality contributions on unification theory and its applications, as well as closely related topics. Unification is concerned with the problem of making two given terms equal, either syntactically or modulo an equational theory. It is a fundamental process used in various areas of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, knowledge representation, types, etc.
The International Workshop on Unification (UNIF) is the main international event on unification. This special issue is related to the research presented in the last four editions of the workshop, i.e., from UNIF 2021 to UNIF 2024. Nevertheless, submissions of high quality works on unification that were not presented at UNIF are also welcome. Thus, participants of UNIF, as well as other authors, are invited to submit contributions.
Following the tradition of UNIF, this special issue addresses the topic of unification in a broad sense. A non-exhaustive list of topics of interest includes:
Submitted manuscripts should be written in English and prepared following the guidelines of JLAMP. Papers should be submitted electronically by using the Editorial Manager for JLAMP. Please choose VSI:Recent Advances in Unification when you will be selecting the article type.
The submission deadline is: February 15, 2025.
This is a call for interest for postdoctoral research at Yoni Zohar’s group at Bar-Ilan University,
Israel.
The position focuses on Satisfiability Modulo Theories (SMT) and proofs.
The work will be done in collaboration with the University of Iowa and Stanford University.
This position can be fully remote.
Qualifications: The ideal applicants would have:
Interested applicants should send their CV, including a list of publications, in PDF to Yoni Zohar together with the names of at least two references.
The Department of Computer Science at ETH Zurich invites applications for an assistant professorship (tenure track) in computer science with focus on Theoretical Computer Science including:
The application deadline is January 15th, 2025.
More information is availablehere.
Hasuo Laboratory at the National Institute of Informatics, Tokyo, Japan invites applications for postdoc and senior researchers. The candidates will pursue collaboration with Bart Jacobs (Nijmegen), Joost-Pieter Katoen (Aachen), and Sam Staton (Oxford). The positions are for 4.5 years max.
We are particularly looking for sprofils in the following areas:
We are also looking ofr PhD students in related topics. You can find more information here. If you are interested, please contact Ichiro Hasuo.
The Formally Verified Security group at the Max Planck Institute is looking for candidates with an excellent research track record and publications at top conferences in programming languages (e.g., POPL and ICFP) and/or security (e.g., CCS and CSF).
Postdoctoral Researcher Position
Candidates are expected to work collaboratively on topics of joint interest and to help co-advise students,
but can also
dedicate some of their time to their own independent projects. My research interests include, but are not
limited to:
formal verification, proof assistants (particularly Coq and F*), type systems, effects, monads, functional
programming,
parametricity, PL semantics, property-based testing, secure compilation, security against speculative
side-channel
attacks, noninterference, compartmentalization, capability machines, etc. You can find more details here.
Tenure-track Position
The Max Planck Institutes (MPIs) for Informatics, for Security & Privacy, and for Software Systems invite
applications
for tenure-track faculty in all areas of computer science. We expect to fill several positions.
Application deadline is December 1st, 2024. You can find more details here.
MPI-SP is a relatively new research institute founded in 2019 and is part of the Computer Science research area of the Max Planck Society. We are located on the campus of Ruhr University Bochum, in the Rhein-Ruhr metropolitan region of Germany, one of Europe's largest academic hubs. The working language of MPI-SP is English, and no knowledge of German is required for this job.
Do not hesitate to contact Catalin Hritcu if you are interested in this position!
King’s College London is offering a PhD scholarship in the areas of programming language semantics and software verification. More details are available here.
Applications should be submitted by the end of December 2024 for a start in June 2025 and by the end of May 2025 for a start in October 2025.
Applications will be assessed as they arrive so submit as early as possible. For more information please contact Maribel Fernandez.
The Department of Computer Science and St John’s College are delighted to offer this opportunity for an outstanding researcher of high international standing with a track record of research that has significantly influenced the field of Computer Science, and who can demonstrate the vision, leadership and enthusiasm to maintain and develop an internationally leading research programme in computer science, and to further the academic and strategic development of the Department.
This post is a statutory professorship. Statutory professors have a world-leading research reputation and exercise broad academic leadership across their department and college, and more widely in their subject at national and international level. The previous holder of this chair was Georg Gottlob.
The University of Oxford’s Department of Computer Science has broad strengths across the spectrum of computer science from theoretical computer science to systems and applications. It is one of the country’s leading computer science departments and is ranked first in a number of international rankings.
The successful candidate will be an outstanding, internationally recognised researcher in computer science, with a proven record of research achievement. They will establish and lead a research team in their area of expertise and will also play a leading role in further developing computer science at Oxford.
The professorship is available with effect from September 1, 2025. The closing date for applications is 12:00 noon UK time on Monday 10 March 2025. Interviews are expected to be held on 22 and 23 May 2025.
More details are available here.
The Department of Computer Science at Aarhus University is looking for excellent and visionary tenure-track Assistant Professors and Associate Professors. Aarhus University — an international top-100 university — has an ambitious strategic investment in a recruitment plan to radically expand the Department of Computer Science. Applicants within all areas of computer science are welcome, including Programming Languages, Software Engineering, Logic and Semantics.
Application deadline is January 13, 2025 for an expected start on the June 1, 2025.
More details are available here.
The Department of Computer Science at Lund University invites applications for a tenure-track assistant professorship in the foundations of computer science with a focus on logic and automated reasoning.
The assistant professor will be working at the Department of Computer Science, where research into the foundations of computer science is conducted by professors Susanna de Rezende and Jakob Nordstrom. Jakob Nordstrom leads the research group Mathematical Insights into Algorithms for Optimization, which is also active at the University of Copenhagen. The research has a unique profile in that it spans a wide range of questions from the theoretical, mathematical foundations of efficient computation all the way to state-of-the-art practical algorithms for real-world problems. This creates a very special environment, where the research projects do not only go deep into different theoretical and applied topics, but where different lines of research cross-fertilise each other and unexpected and exciting synergies often arise.
This position focuses on algorithms for foundational problems within logic, automated reasoning, and combinatorial optimization. This includes design and implementation of algorithms for computational problems within Boolean satisfiability (SAT) solving, constraint programming, mixed integer linear programming, and/or satisfiability modulo theories (SMT) solving. In addition to algorithm construction, another topic of interest is to develop a scientific understanding of the practical performance of automated reasoning algorithms, and to investigate relations between empirical observations and theoretical results in algorithm analysis and computational complexity theory. Yet another related area concerns methods of ensuring that algorithms compute provably correct results, which can be used to develop trustworthy solvers for automated reasoning and combinatorial optimization.
The application deadline is January 8, 2025. See here for more information and instructions how to apply. Informal enquiries are welcome and may be sent to Jakob Nordström.
The research position is open to candidates proposing to join the LMV team (Languages, Models and Verification) at LIFO (Laboratoire d'Informatique Fondamentale d'Orléans). The overall objective of the Languages, Modeling, Verification (LMV) team is to advance the reliability and security of software, particularly in the context of the Internet of Things (IoT). This objective is part of the general field of cybersecurity. We aim to ensure that the software involved satisfies critical properties either by construction by leveraging the design of libraries and programming languages, or by using formal methods. Candidates are required to teach in the computer science department.
The person recruited will be member of the Laboratoire d'Informatique Fondamentale d'Orléans (LIFO, UR 4022). LIFO is a joint laboratory of the University of Orléans and INSA Centre Val de Loire, composed of approximately 89 active researchers or teacher-researchers, including 46 tenured faculty members. Located on two campuses, Orléans and Bourges, LIFO is made up of five research teams, the first four located in Orléans, the fifth located in Bourges: Constraints and Learning (CA), Graphs, Algorithms and Computational Models (GAMoC), Languages, Models and Verification (LMV), Parallelism and Data Management (PAMDA), Data and Systems Security (SDS). LIFO is a member of the research federation ''Informatique Centre Val de Loire'' (ICVL), which brings together researchers in computer science in the region.
The application deadline is April 4, 2025 for an expected start on the September 1, 2025. See here for more information and instructions how to apply. Informal enquiries are welcome and may be sent to Frédéric Loulergue.
Contact: Martin Suda, Automated Reasoning Group, CIIRC, CTU, Prague.
Looking for a PhD student (background in logic and/or machine learning an advantage) to help us enhance the award winning automatic theorem prover Vampire with a new generation of neural guidance, combining elements of reinforcement learning and efficient vectorial representations of formulas and states, targeting the main applications in program verification and proof assistants.
The position is available from January 2025. More details can be found at the project page.