The Association for Automated Reasoning (AAR) is seeking a new AAR Newsletter Editor.
The AAR publishes an electronic newsletter, sent to all members, with a frequency of three to five times a year. The AAR newsletter is the major information channel for the automated reasoning community. Among other things, it can contain:
Earlier issues of the AAR newsletter can be found here.
The role of the newsletter editor is to collect and select information for inclusion in the newsletter, to solicit contributions, to technically edit the letter as a webpage, and to send out an announcement with link and summary. All this is done in close collaboration with the following people and roles:
Acting as the AAR newsletter editor is an excellent opportunity for a deep and visible involvement in the AR community, as the role connects to all kinds of AR activities. The newsletter is a cornerstone for the community identity and development.
If you are interested in taking up this role, please reply to Philipp Rümmer, secretary of AAR (secretary (at) aarinc (dot) org), until March 29th, 2024. Please include (links to) information about your connection to automated reasoning. A decision will be taken by the boards of AAR and CADE.
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 two CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2024.
The current members of the board of trustees are (in alphabetical order):
The terms of Cláudia Nalon and Stephan Schulz end. Cláudia Nalon may be nominated for a second term, whereas Stephan Schulz has already served two consecutive terms and cannot be nominated this year.
The term of office of Christoph Benzmüller as IJCAR 2024 programme chair ends after the IJCAR conference. As outgoing ex-officio trustee, Christoph Benzmüller is eligible to be nominated as elected trustee.
In summary, we are seeking to elect two trustees.
Nominations can be made by any CADE member, either by e-mail or at the CADE business meeting at IJCAR 2024; since nominators must be CADE members, they must have participated at at least one of the CADE or IJCAR conferences in the years 2021-2024. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. For further details please see the CADE Inc. bylaws at the CADE web site.
E-mail nominations can be provided up to the upcoming CADE business meeting, via email to
Jürgen Giesl, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.
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 submitted via email, by 5 April 2024 (Anywhere on Earth).
The nomination must consist of one compressed file (.zip) containing:
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 2024 consists of the following people:
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 can be submitted at any time; the deadline for nominations to be considered for the Herbrand Award 2024, which will be given at IJCAR 2024, is
March 11 2024Nominations pending from previous years must be resubmitted in order to be considered.
For more details, please check the Herbrand Award webpage.
Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contributions (including the relationship to CADE), along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent via e-mail to
Jürgen Giesl, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.
An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Goedel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see here, here, and here.
The 2023 Alonzo Church Award was jointly to Lars Birkedal, Aleš Bizjak, Derek Dreyer, Jacques-Henri Jourdan, Ralf Jung, Robbert Krebbers, Filip Sieczkowski, Kasper Svendsen, David Swasey and Aaron Turon for the design and implementation of Iris, a higher-order concurrent separation logic framework.
Eligibility and Nominations
The contribution must have appeared in a paper or papers published within
the past 25 years. Thus, for the 2024 award, the cut-off date is January 1,
1999. When a paper has appeared in a conference and then in a journal, the
date of the journal publication will determine the cut-off date. In
addition, the contribution must not yet have received recognition via a
major award, such as the Turing Award, the Kanellakis Award, or the Goedel
Prize. (The nominee(s) may have received such awards for other
contributions.) While the contribution can consist of conference or journal
papers, journal papers will be given a preference.
Nominations for the 2024 award are now being solicited. The nominating letter must summarise the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness. Nominations for the 2024 award are automatically considered for all future editions of the award, until they receive the award or the nominated papers are no longer eligible.
Nominations should be submitted to Igor Walukiewicz by March 1, 2024.
Presentation of the Award
The 2024 award will be presented at the Thirty-Ninth Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS) which is scheduled to take place in
Tallinn, Estonia during 8–12 July 2024. The award will be accompanied by
an invited lecture by the award winner, or by one of the award winners.
The awardee(s) will receive a certificate and a cash prize of USD 2,000.
If there are multiple awardees, this amount will be shared.
We are pleased to announce the call for proposals for hosting and organising FroCoS-ITP-TABLEAUX 2025, on their 15th, 16th and 33rd editions, respectively.
FroCoS and Tableaux have co-located for quite a number of editions, and in 2017 we had a very successful edition of the three conferences running together. In 2025 we intend to resume this partnership. We expect the 2025 edition of FroCoS+Tableaux to have around 100 participants. ITP tends to have 75-100 participants.
Bids should be sent by email and should include at least the following information:
The deadline for bids is Monday, 15 April 2024. Shortly after, all admitted bids will be made public and the voting phase will take place. The people eligible to vote are those who are seriously considering attending FroCoS-ITP-TABLEAUX 2025. The voting system used will be single transferable vote between all received bids.
The editors invite submissions for a Special Issue on "Combining Probability and Logic", to be published with Journal of Logic and Computation.
Classically, logic and probability offer competing representations of partial or incomplete information, with the former assuming a qualitative perspective on uncertainty and the latter focusing on a quantitative account. Both provide their own policies for updating on new information, combining evidence from different sources, and acting under partial information.
We solicit submissions of original papers that bridge these two perspectives. These could, for instance, apply probabilistic or other quantitative tools to the study of logical systems or use logical frameworks, classical or substructural, for understanding probabilistic approaches. They may also apply to specific sub-areas, such as game theory, network theory, causal modelling or machine learning. We especially invite submissions that combine probability and logic for knowledge representation and reasoning broadly construed.
The Special Issue is related to the topics of the conference Progic 2023: The Eleventh Workshop on Combining Probability and Logic. Workshop participants, as well as other authors are invited to submit contributions.
Submissions should be written in English and are expected to contain relevant new logical results that are of significant interest to a substantial number of logicians. All submissions must comply with the submission guidelines of Journal of Logic and Computation and will be peer reviewed according to the standards of the Journal.
How to submit
Submissions should be sent to Jane Spurr with "JLCs-Progic submission" in the subject line.
The deadline for submitting full manuscripts is March 31, 2024.
For more information, please contact the Guest Editors: Dominik Klein (Utrecht University) and Dragan Doder (Utrecht University).
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
New results in the fields of computational logic and applications are welcome.
Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices.
Topics of interest include, but are not limited to: Abduction, Answer set programming, Automated reasoning, Constraint programming, Computational proof theory, Decision procedures, Description logics, Formalizing mathematics, Foundations of security, Hardware verification, Implementations of logic, Interpolation, Interactive theorem proving, Knowledge representation and reasoning, Logic and computational complexity, Logic and databases, Logic and games, Logic and language models, Logic and machine learning, Logic and the web, Logic and types, Logic in artificial intelligence, Logic programming, Logical foundations of programming, Logics of knowledge and belief, Modal and temporal logics, Model checking, Non-monotonic reasoning, Ontologies and large knowledge bases, Probabilistic and fuzzy reasoning, Program analysis, Rewriting, Satisfiability checking, Satisfiability modulo theories, Software verification, Unification theory.
Deadlines
More information is available on the conference's web page.
TASE 2024 aims to provide a forum for people from academia and industry to communicate their latest results on innovative advances in software engineering. Modern society is increasingly dependent on software systems that are becoming larger and more complex. This poses new challenges to the various aspects of software engineering, for instance, software dependability in trusted computing, interaction with physical components in cyber physical systems, quality assurance in AI-embedded systems, distribution in cloud computing applications, security and privacy in general. Hence, new concepts and methodologies are required to enhance the development of software engineering from theoretical aspects.
Topics of Interest
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
More information is available on the conference's web page.
CiE is a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world.
The CiE conferences serve as an interdisciplinary forum for research in all aspects of computability, foundations of computer science, logic, and theoretical computer science, as well as the interplay of these areas with practical issues in computer science and with other disciplines such as biology, mathematics, philosophy, or physics.
Important Dates:
More information is available on the conference's web page.
Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order and model theory. The programme of the conference TACL 2024 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical and topological methods.
Featured topics
We welcome contributed talks on any topic involving the use of algebraic, categorical or topological methods in either logic or computer science. This includes, but is not limited to, the following areas:
Important dates
More information is available on the conference's web page.
Artificial intelligence has seen a significant shift in focus towards designing and developing intelligent systems that are interpretable and explainable. This is due to the complexity of the models, built from data, and the legal requirements imposed by various national and international parliaments. This has echoed both in the research literature and the press, attracting scholars worldwide and a lay audience. An emerging field with AI is eXplainable Artificial Intelligence (xAI), devoted to producing intelligent systems that allow humans to understand their inferences, assessments, predictions, recommendations and decisions. Initially devoted to designing post-hoc methods for explainability, eXplainable Artificial Intelligence (xAI) is rapidly expanding its boundaries to neuro-symbolic methods for producing self-interpretable models. Research has also shifted the focus on the structure of explanations and human-centred Artificial Intelligence since the ultimate users of interactive technologies are humans.
The World Conference on Explainable Artificial Intelligence is an annual event that aims to bring together researchers, academics, and professionals, promoting the sharing and discussion of knowledge, new perspectives, experiences, and innovations in the field of Explainable Artificial Intelligence (xAI). This event is multidisciplinary and interdisciplinary, bringing together academics and scholars of different disciplines, including Computer Science, Psychology, Philosophy, Law and Social Science, to mention a few, and industry practitioners interested in the practical, social and ethical aspects of the explanation of the models emerging from the discipline of Artificial intelligence (AI).
This special track explores approaches to Explainable AI (XAI) based on logic and reasoning techniques. While the traditional role of logic in AI lies in knowledge representation and reasoning, it is increasingly used in other areas highly relevant to Explainable AI. This includes neuro-symbolic approaches to AI, learning from a combination of knowledge and data, explanation interfaces, and as a basis for meta-reasoning about machine learning systems. An example of meta-reasoning is explaining predictions made by classifiers. As opposed to popular heuristic-based approaches, the logic-based approach, based on prime implicants, leads to provably correct explanations and the ability to reason formally about the behaviour of a classifier, such as whether the classifier exhibits bias. Logic and reasoning can be used to study the foundations of explanations in diverse settings. This track aims to bring together researchers applying logic and reasoning within XAI. It covers various logic-based strategies for representing, validating, and implementing XAI systems, emphasising the harmonisation of logic with AI explainability.
Important Dates
More information is available on the conference's web page.
More and more mathematical information is digitally processed, generated, communicated, stored and curated.
CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration.
CICM covers
Workshops typically feature presentations of ongoing research that is not ready yet for formal publication, and tutorials present extended demos of a particular software.
However, the CICM organizers strongly encourage a broad interpretation of these concepts and welcome proposals for any kind of event that benefits the CICM community.
A proposal should include the following information:
CICM 2024 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to
Important Dates
workshop proposals:
All proposals should be submitted via email to Dennis Mueller.
Paper submissions
More information is available on the conference's web page.
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
We invite submissions on all aspects of modal and related logic, including (but not limited to):
Important Dates
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 15th 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:
More information is available on the conference's web page.
We invite all members of the international AI research community to submit their best work to ECAI 2024. Join us to mark the 50th birthday since the first AI conference was held in Europe back in 1974.
We welcome submissions on all aspects of AI. Submissions will be subject to double-blind peer review by the programme committee. They will be evaluated based on relevance, clarity, significance, originality, soundness, reproducibility, scholarship, and quality of presentation.
Topics
Submissions on all aspects of AI are welcome. This includes in particular:
Important Dates
More information is available on the conference's web page.
The Italian Conference on Computational Logic (CILC) is the annual meeting of the Italian Association for Logic Programming (GULP - Gruppo Ricercatori e Utenti Logic Programming).
The Conference will feature presentations of invited speakers and contributed papers concerning all aspects of computational logic.
List of Topics
Important Dates
More information is available on the conference's web page.
The CP conference is the premier international event for presenting research in all aspects of computing with constraints, including, but not restricted to: theory, algorithms, environments, languages, models, systems, and applications.
The conference welcomes submissions that advance the state of the art of fundamental constraint-based technologies, as well as those that seek connections with other domains: for example, operations research, satisfiability, computational biology, configuration and design, computer music, entertainment, sport, cybersecurity, and AI in its broader context.
Important Dates
More information is available 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.
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. Further details about the submission guidelines and the selection criteria can be found on the website.
Topics of Interest
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.
Important Dates
More information is available on the conference's web page.
The aim of the FMICS conference series is to provide a forum for researchers and 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.
Topics
Topics of interest include (but are not limited to):
Important Dates
More information is available on the conference's web page.
The PPDP 2024 symposium brings together researchers from the declarative programming communities, including those working in the functional, logic, answer-set, and constraint handling programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for analyzing, performing, specifying, and reasoning about computations, including mechanisms for concurrency, security, static analysis, and verification.
Submissions are invited on all topics related to declarative programming, from principles to practice, from foundations to applications. Topics of interest include, but are not limited to:
Important dates:
More information is available on the symposium's web page.
The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in logic-based program development in any programming language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress.
Topics of interest include all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large, including, but not limited to:
Important dates:
More information is available on the symposium's web page.
Topics
The conference seeks to address the applications of formal methods in all aspects of software components and services. FACS aims at developing a community-based understanding of relevant and emerging research problems through formal paper presentations and lively discussions. FACS 2024 welcomes contributions including but not limited to:
Important Dates
More information is available on the conference's web page.
The ICTAC conference series aims to bring 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 The conference concerns all aspects of theoretical computer science, including, but not limited to:
Important Dates
More information is available on the conference's web page.
Research in verification has seen an increase in heterogeneous techniques and a synergy between the traditionally distinct areas of dynamic and static analysis. There is growing awareness that dynamic techniques such as testing and static techniques such as proving are complementary rather than mutually exclusive. Notable examples that provide evidence for the potential of a combination of static and dynamic analysis are counterexample generation based on symbolic execution, the integration of SAT/SMT-solving in model checking, or the combination of predicate abstraction with exhaustive enumeration. The verification of systems based on machine learning spurs novel combinations of dynamic and static analyses, e.g., property verification of surrogate models that are generated through testing.
TAP’s scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Topics of interest center around the combination of static techniques such as proving and dynamic techniques such as testing.
Papers are solicited on, but not limited to, the following topics:
Important Dates
More information is available on the conference's web page.
Non-classical logics – such as modal logics, conditional logics, intuitionistic logic, description logics, temporal logics, linear logic, dynamic logic, deontic logics, fuzzy logic, paraconsistent logic, relevance logic – have many applications in AI, Computer Science, Philosophy, Linguistics and Mathematics. Hence, the automation of proof search in these logics is a crucial task.
The ARQNL workshop aims at fostering the development of proof calculi, automated theorem proving systems and model finders for all sorts of quantified non-classical logics. The workshop will provide a forum for researchers to present and discuss recent developments in this area. The contributions may range from theory to system descriptions and implementations. Contributions may also outline relevant applications, describe problem formalizations, example problems, and benchmarks. We welcome contributions from computer scientists, linguists, philosophers, and mathematicians.
Topics of the ARQNL workshop will cover all aspects related to the mechanization and automation of quantified non-classical logics, including but not limited to:
Important Dates
More information is available on the workshop's web page.
Quantifiers play an important role in language extensions of many logics. The use of quantifiers often allows for a more succinct encoding as it would be possible without quantifiers. However, the introduction of quantifiers affects the complexity of the extended formalism in general. In consequence, theoretical results established for the quantifier-free formalism may not directly be transferred to the quantified case. Further, techniques successfully implemented in reasoning tools for quantifier-free formulas cannot directly be lifted to a quantified version.
The goal of the Workshop on Quantification (QUANTIFY 2024) is to bring together researchers who investigate the impact of quantification from a theoretical as well as from a practical point of view. Quantification is a topic in different research areas, e.g., in SAT in terms of QBF, in CSP in terms of QCSP, in SMT, etc. This workshop has the aim to provide an interdisciplinary forum where researchers of various fields may exchange their experiences.
In particular, the following topics shall be considered at the workshop:
Important Dates
More information is available on the workshop's web page.
The TPTP Tea Party brings together developers and users of the TPTP World, including (but not limited to):
The meeting aims to elicit feedback, suggestions, criticisms, etc, of these resources, in order to ensure that their continued development meets the needs of successful automated reasoning. The meeting will be structured discussion following an agenda of topics that have been suggested and agreed upon in advance.
This year funding for participants is provided by Working Group 2 Automated Theorem Provers, COST Action 2011 EuroProofNet. If you would like to receive announcements about the meeting, funding, and more, please join the TPTP World Google Group.
More information is available on the tea party's web page.
The workshop addresses recent trends in implementing first-order theorem provers, and focus on new challenges and application areas. The workshop also discusses the development and use of the first-order theorem prover Vampire, and its potential use cases and interaction with other systems.
Workshop participants include both Vampire developers and users, with discussions between tool developers and users. Participants can learn more about the use of Vampire, its efficiency in various application areas and needs of the users.
The workshop sheds light on topics such as:
Important Dates
More information is available on the workshop's web page.
The automation of logical reasoning is a challenge that has been studied intensively in fields including mathematics, philosophy, and computer science. PAAR is the workshop on turning this theory into practice: how can automated reasoning tools be built that work and are useful in applications? PAAR covers all aspects of this challenge: which theories, logics, or fragments are well-behaved in practice, and connect well to application domains? which reasoning tasks are tractable and useful? which algorithms are able to solve real-world instances? how should automated reasoning tools be designed, implemented, tested, and evaluated?
The goal of PAAR is to bring together theoreticians, tool developers, and users, to concentrate on the practical aspects of automated reasoning. The workshop welcomes high-quality contributions of any kind, including new research results, presentation of work in progress, presentation of new tools, new implementation techniques, new application domains, or case studies.
Topics include, but are not limited to:
Important dates
More information is available on the workshop's web page.
Symbolic Computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions.
The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces for tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop is to provide an opportunity to discuss, share knowledge and experience across both communities.
The topics of interest include but are not limited to:
Important Dates
All deadlines are by the end of the day anywhere on earth.
More information is available on the workshop's web page.
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of a new software generation and to discuss existing systems.
Topics of interest include:
Important Dates
More information is available on the workshop's web page.
UNIF 2024 is the 38th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of making two given terms equal, either syntactically or modulo an equational theory. It is a fundamental process used in various areas of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, knowledge representation, types, etc.
The International Workshop on Unification (UNIF) is a forum for researchers in unification theory and related fields to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for students, young researchers and scientists working in related areas to get an overview of the current state of the art in unification theory.
Topics
A non-exhaustive list of topics of interest includes:
Important Dates
More information is available on the workshop's web page.
We are delighted to announce the Fifth International Workshop on Automated (Co)inductive Theorem Proving, an event dedicated to the latest developments in inductive and coinductive methods for verification. This workshop is a significant gathering for researchers and practitioners in the field, providing an invaluable opportunity to explore current challenges and innovations in computational verification.
Key Themes
Important Dates
More information is available on the workshop's web page.
The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, ATP systems – the world championship for such systems. One purpose of CASC is to provide a public evaluation of the relative capabilities of ATP systems. Additionally, CASC aims to stimulate ATP research, motivate development and implementation of robust ATP systems that can be easily and usefully deployed in applications, provide an inspiring environment for personal interaction between ATP researchers, and expose ATP systems within and beyond the ATP community. CASC evaluates the performance of ATP systems in terms of the number of problems solved, the number of acceptable proofs and models produced, and the average time taken for problems solved, in the context of a bounded number of eligible problems and specified time limits.
CASC is held at each CADE and IJCAR conference - the major forums for the presentation of new research in all aspects of automated deduction. CASC-J12 will be held during the 12th International Joint Conference on Automated Reasoning (IJCAR, which incorporates CADE). The competition organizer is Geoff Sutcliffe, assisted by Martin Desharnais (SLH division). The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. The panel members are Cláudia Nalon, TBA, and Christoph Weidenbach. If you have any questions about the competition, please email the organizer.
More information is available on CASC's web page.
Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis.
After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques.
The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas.
The competition will be affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2024). It will be run on the StarExec platform. The final run and a presentation of the final results will be live at IJCAR.
We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications.
A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed.
Important dates
For further information, we refer to the website of the termination and complexity competition.
As a PhD student, or Master student with research ambitions, you may wonder how internationally recognised researchers in computer science could become what they are now. What can one learn from their example? What do successful research paths look like? Are the important factors just as expected, or are there surprising aspects which make the difference? What is important to think about at your stage?
We welcome PhD students, and Master students with research ambitions, to join the Mentoring Workshop at ETAPS 2024 in Luxembourg! During this workshop, well known computer science researchers, of different seniority, will give inspirational talks about the path they took, what was important on the way, and insights they want to pass on to early career researchers. There will be plenty of opportunity for discussions and interaction, during the workshop and in the social programme around it.
We are proud that we could secure the following speakers:
Participating at the workshop requires a registration for the ETAPS workshops on Sunday.
The early registration deadline is March 6th, 2024.
More information is available on the workshop's web page.
Many Program Verification and Synthesis problems of interest can be modeled directly using Constrained Horn Clauses (CHCs) and many recent advances have centered around efficiently solving problems presented as Horn clauses.
This series of workshops aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis.
Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences.
Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:
Important dates:
More information is available on the workshop's web page.
RRRR provides a forum to present and discuss novel approaches to foster reproducibility of research results, and replication studies of existing work, in the broad area of formal methods research. Its goal is to spread the word on best practices, and reward the work invested in replicating results. RRRR invites abstracts and short papers for presentation at the workshop; we plan to invite authors to submit full papers to a special issue of STTT afterwards.
Submissions are encouraged in, but not limited to, the two main topics of reproducibility and replication:
Timeline
More information is available on the workshop's web page.
SynCoP 2024 aims at bringing together researchers working on verification and parameter synthesis for systems with discrete or continuous parameters, in which the parameters influence the behaviour of the system in ways that are complex and difficult to predict. Such problems may arise for real-time, hybrid or probabilistic systems in a large variety of application domains. The parameters can be continuous (e.g. timing, probabilities, costs) or discrete (e.g. number of processes). The goal can be to identify suitable parameters to achieve desired behaviour, or to verify the behaviour for a given range of parameter values.
Systems composed of a finite but possibly arbitrary number of identical components occur everywhere from hardware design (e.g. cache coherence protocols) to distributed applications (e.g. client-server applications). Parameterised verification is the task of verifying the correctness of this kind of systems regardless the number of their components.
The scientific subject of the workshop covers (but is not limited to) the following areas:
Important Dates (AoE)
More information is available on the workshop's web page.
There will be a session on Interactions Between Proof Assistants and Mathematical Software at the biannual International Conference on Mathematical Software.
As part of this Alex Best and Heather Macbeth are calling for abstracts for talks to be presented at the session. Abstracts should be around 200 words. The short abstract deadline is the 24th February 2024, but we will review and accept abstracts on a rolling basis before then. Please send abstracts via email.
The aim of this call is to inspire people to bring both their completed projects but also works in progress and demos to meet and discuss the intersections of formal and informal mathematical software with a wide range of interested participants. Abstracts will be published on the website as they are accepted.
We welcome expressions of interest before the official deadline, both of potential speakers and other participants in order to help us with the planning.
There will be the opportunity for accepted speakers to publish extended abstracts / papers in the proceedings of the ICMS, subject to participant interest. So if you have some work you'd like to present that would be of interest for this session please submit an abstract to us whenever it is ready! For funding and other particulars about the ICMS and location and travel please see the main ICMS website (which will be updated further in future).
The full description of the session is as follows: Interactive proof assistants (ITPs) are pieces of software that allow one to express mathematical constructs and arguments and check them interactively. Formalisation, the process of writing mathematical proofs in these systems, is becoming increasingly popular amongst mathematicians.
This session will showcase projects bridging the gap between ITPs and other kinds of mathematical software and computation. There are many aspects of this which could be explored further. For example; tactics for ITPs which make use (and verify) witnesses extracted from unverified computation; code extraction, allowing formalised algorithms to be used for computer algebra; proof discovery and visualisation tools within ITPs which make use of external mathematical software; using proof assistants to check key reductions in computer algebra; or interfaces between ITPs and SAT/SMT solvers to verify completely automated proofs.
We hope that this session will foster collaboration among people working in formalisation, computer algebra, and other areas of mathematical computation.
More information is available on the workshop's web page.
The aim of this workshop is to bring together experts from different research communities (such as proof theory, model theory, proof complexity, verification, database theory, knowledge representation, automated reasoning, automata theory, philosophy, linguistics) in order to discuss and disseminate recent and ongoing research pertaining to Craig interpolation and Beth definability.
If you are interested in attending, and would like to apply for funding and/or give a presentation at the workshop, please register by March 15 using the form specified at the workshop webpage
For more information, please contact Balder ten Cate or any of the other organizers.
Twenty years after the publication of Ehrhard and Regnier’s first seminal paper on the subject, we are delighted to announce a conference on Differential λ-calculus and Differential Linear Logic, nicknamed DiλLL 2024.
The programme will consist in a series of invited talks, a good proportion of which will be tutorials, targeted at young researchers as well as non-specialists. It will also include surveys of the main advances obtained in the course of twenty years, as well as research talks on current topics.
For young researchers, it will also be possible to display posters in the premises of the conference during the whole week, in order to foster discussion around your work.
Registration for in person attendance until 17 March 2024.
More information is available on the workshop's web page.
The Interaction and Concurrency Experience (ICE) series of international scientific meetings are a forum for computer science researchers with research interests in models, verification, tools, and programming primitives for complex interactions.
Scope The general scope of the workshop is interaction and concurrency, broadly construed. The workshop welcomes contributions spanning the spectrum from theoretical models to practical implementations and empirical studies. Topics of interest include (but are not limited to):
Important Dates
More information is available on the workshop's web page.
We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to:
Important Dates:
More information is available on the workshop's web page.
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
LFMTP 2024 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
Important Dates
More information is available on the workshop's web page.
The Tsinghua University - University of Amsterdam Joint Research Centre for Logic initiated a Logic Summer School Program in the year 2021. The program is primarily aimed at advanced undergraduate students, graduate students, and early career researchers in philosophy, computer science, mathematics, linguistics, cognitive sciences, and so on. Students and colleagues can learn here about the latest developments in logic interfacing with the aforementioned disciplines, including their theoretical results and technical backgrounds. The courses are particularly designed to supplement the logic courses that are taught in the usual curriculum.
For participants who attend and complete the courses, the Joint Research Centre will award a certificate of completion.
To ensure better teaching and learning experience, for each course we will accept only around 30 students.
Please contact Chenwei Shi if you have any questions.
More information is available on the school's web page.
The IMS Graduate Summer School in Logic is jointly organized and funded by the Institute for Mathematical Sciences (IMS) and the Department of Mathematics of the National University of Singapore. The Summer School bridges the gap between a general graduate education in mathematical logic and the specific preparation necessary to do research on problems of current interest in the subject. In general, students who attend the Summer School should have completed their first year, and in some cases, may already be working on a thesis. While a majority of the participants will be graduate students, some postdoctoral scholars and researchers may also be interested in attending.
Having completed at least one course in Mathematical Logic is required, and completion of an additional graduate course in model theory, recursion theory or set theory is strongly recommended. Students should be familiar with the Gödel Completeness and Incompleteness Theorems, basic results in model theory and recursion theory, as well as the Gödel and Cohen Consistency and Independence Theorems in Set Theory.
Preference will be given to students who have not attended the summer schools previously held at IMS, but all interested graduate students are welcome to apply.
Applications are invited from interested students. Up to 30 students will be offered financial support. Selected overseas participants will be provided stipend, accommodation and partial funding for travel.
Deadline for application is 15 March 2024.
Completed applications will be considered on a rolling basis from 15 March 2024 and applicants notified of the decisions by 15 April 2024.
More information is available on the school's web page.
ISR 2024 is aimed at master and PhD students, researchers and practitioners interested in the study of rewriting concepts and their applications. It offers three parallel tracks, taught by well-known experts:
Each track consists of 20 slots of 90 minutes. Further details (including registration information) can be found on the website of ISR 2024.
early registration deadline: May 1
More information is available on the school'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, both 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. The school follows the successful line of Summer Schools that ran from 2011 to 2022.
We are pleased to announce that the next edition of the SAT/SMT/AR Summer School will take place in Nancy, France from June 26 to June 29, 2024. The lectures planned this year are detailed on the website and include a mix of basic and advanced theory as well as practical sessions.
The school is intended for PhD students, Master students, and industrial practitioners who want to get a good understanding of capabilities and current research directions in the area of SAT, SMT, and Automated Reasoning. Prior knowledge in those areas is not required, but knowledge of logic, general problem solving skills, good programming and math skills are helpful.
Application will open in March.
Check out the school's web page for up-to-date information.
The Programming Languages and Systems (PLAS) group at the University of Kent’s School of Computing invites applications for 3.5-year PhD scholarships (fully funded for both UK and international students). The PLAS group is a diverse community of researchers exploring all aspects of programming languages, spanning from theory to applications.
Applications are due by the 3th March 2023.
These scholarships include a doctoral stipend (equivalent to the Research Councils UK National Minimum Doctoral Stipend, £18,622 2023/24 rate, 2024/25 to be announced) for 3.5 years, tuition fees at the home rate and access to further research support funding. If you are applying as an international candidate, Kent will waive the difference between Home and International fees.
If you are interested in applying, please contact a potential supervisor (see list below) as soon as possible, and at least two weeks prior to the closing date. If the supervisor wishes to support your application, they will direct you to make an official application through the KentVision system.
Submit your formal applications through the university admission system by the 3th March 2023. Your application should include a completed online admission form; the name and contact details of two referees; an original document providing confirmation of your degree (or a transcript if the degree is not yet awarded). For non-native English speakers, a certificate of competence in English is required at IELTS 6.5 or higher, with no element less than 6.0 (or equivalent).
Programming Languages and Systems Group Topics suggested by our group Application process, requirements and general enquires
PLAS is a large research group with potential supervisors who work across the breadth of programming languages and systems research.
In the recent QS World University Rankings, the University of Kent has secured its place within the top 25% of Higher Education Institutions globally.
Kent's campus is based atop a scenic hill with a stunning view of the historic city of Canterbury, a designated World Heritage Site and host of the cathedral of the Archbishop of Canterbury.
The campus offers diverse housing options within its colleges with a 30-minute walking distance from the city. Commuting options include biking or public transport via bus. Canterbury is in a most advantageous location offering quick access to London with just a 55-minute train ride, and European travel is within reach via the Eurostar train or by car.
A postdoctoral position in program semantics and verification is open at the Singapore Institute of Technology (SIT) under the supervision of Prof. David Sanan.
The project aims to minimize the gap between formal verification and efficient industrial applications. Specifically, we are focusing on constructing a verification framework for software using deductive reasoning, and on formalizing the semantics of smart contracts, with special attention to the Solidity language.
The candidate will work on formalizing programming language semantics, constructing a framework for scalable verification, and developing mechanisms for automatic reasoning in Isabelle/HOL.
Qualifications:
The expected salary range is 75k~100k SGD + bonus. SIT is located in Singapore, a multicultural English-speaking city known for its high-quality education and healthcare systems, as well as very low tax rates.
This full-time position is available for one year initially, with the possibility of renewal(s).
Starting date: As soon as possible.
To apply, please send an email with your CV to Prof. David Sanan.
Exciting opportunities for two PhD Research Fellows in Algorithms, Logic, and AI at the Department of Informatics at the University of Bergen. The positions are for a fixed-term period of 3 years with the possibility of a 4 th year extension for teaching. The positions are subject to financing by the TMS-grant Trustworthy AI and by the University of Bergen. The successful candidate must be able to start in the position no later than September 30th, 2024.
Algorithmic Foundations of Trustworthy AI project aims to build a new theoretical framework for understanding, developing, and designing socially responsible algorithms incorporating human values into AI systems.
The growing ubiquity of algorithms raises serious concerns about their fairness, bias, and accountability. How can algorithmic injustice and inequity occur, and how can it be detected? How can we ensure that algorithms are not discriminating? Can we design algorithms that will eliminate, or at least reduce, the bias of the human user? How democratic are algorithmic decisions, and how easily can they be manipulated? The project aims to address such questions by limiting the algorithm’s perceived unfairness through adding new constraints (or decision rules) to the mathematical model, developing a modelling framework that combines formal models of social phenomena with formal models of computation.
The project comprises seeks to address two research questions: (1) How to develop algorithms with guaranteed performance (such as scalability, running time, approximation, or space complexity) for the needs of constraining algorithmic optimization? (2) How to design models with the right balance between algorithmic bias and algorithmic effectiveness?
Applicants must hold a master's degree or equivalent education in Computer Science or Mathematics. Master students can apply provided they complete their final master exam before 25.06.2024. It is a condition of employment that the master's degree has been awarded.
To apply, click here.
If you have questions please get in touch with Fedor Fomin or Inge Jonassen.
École polytechnique, leading engineering school in France, member of IP Paris, welcomes applications for several academic positions, starting in September 2024:
Full-time position holders are expected to join the LIX, the computer science laboratory of École polytechnique. Part-time position holders combine their teaching activity at École polytechnique with a main job carried out in the academic or industrial sector.
Precise informations (and in particular contacts) regarding each of these job offers are available following this link. Applications are open until March 15, 2024.
Aalborg university is looking to appoint a number of assistant professors (with possibility of tenure-track) and associate professors in computer science. You can apply for both the Copenhagen campus and the Aalborg campus of Aalborg University.
The deadlines for applications are soon!
From the ITP community we have here also Jonathan Julian Huerta y Munive and Léon Gondelmans who you may also know.
You can apply here:
There are two PhD scholarships available at The Australian National University, for the following areas: Verification of Non-blocking Concurrent Algorithms and Verification of Safety-Critical Systems using Rely/Guarantee.
Both topics are quite flexible and interested applicants are welcome to discuss their own project ideas in similar areas.
Suitable applicants should have a background in Computer Science, Software Engineering, Mathematics or similar fields. Familiarity with formal methods, logic, verification, model checking, program reasoning, etc. is a benefit but is not essential.
Contact Nisansala Yatapanage to apply or for informal enquiries. Applications will be accepted until the positions are filled, but applicants are encouraged to apply as soon as possible.
The Security and Privacy Research Unit at TU Wien is offering a fully funded PhD position in Formal Methods for Security and Privacy under the supervision of Univ.-Prof. Dr. Matteo Maffei.
Your profile:
We offer:
Applications are to be performed online. The application material should include:
Applications are welcome until our positions are filled. The applications will be evaluated in a bi-weekly fashion, and applicants will be contacted only in case they are selected for an interview.
Are you interested to work, in an interdisciplinary research setting, on topics at the intersection of logic, machine learning and automated reasoning? The Institute for Logic, Language and Computation (ILLC) of the University of Amsterdam is looking for a talented PhD candidate. Your research will concern the use of machine learning for automated reasoning (such as mathematical theorem proving and/or declarative constraint-based reasoning).
See here for more information.
The deadline for applications is March 11, 2024.