The 29th Conference on Automated Deduction will take place in Rome. The PC chairs are Brigitte Pientka and Cesare Tinelli and the conference chair is Daniele Gorla. The tentative dates for the conference are July 1-4, 2023. The conference will be co-located with FSCD.
More information is or will soon be available on the conference website and a call for papers will follow.
We invite proposals for sites around the world to host the 12th International Joint Conference on Automated Reasoning (IJCAR) to be held in summer 2024. 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 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; and IJCAR 2022 as part of FLoC in Haifa, Israel.
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. In 2020, ITP was part of IJCAR and it may join IJCAR again in 2024. Usually, a considerable number of workshops are also affiliated with the conference.
The deadline for proposals is January 30, 2023. Proposals should be sent to the IJCAR Steering Committee Chair (see contact information above). We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within one month after the proposal due date.
Proposals should address the following points that also represent criteria for evaluation:
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 Award selection committee, instituting new awards, etc.
The members of the board of trustees until the 2022 elections were:
The terms of Pascal Fontaine, Laura Kovács, Aart Middeldorp, and Christoph Weidenbach ended. The term of office of Jasmin Blanchette as IJCAR 2022 programme chair ended after the IJCAR conference, and Brigitte Pientka joined the board of trustees as CADE-29 program chair.
This means that four 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 251 ballots were sent out on September 22. By October 6, 67 CADE members had voted through CIVS, which translates to a participation rate of 26.7% (as compared to 26.7% in 2021, 34.5% in 2019, 21.1% in 2018, 9.1% in 2017, 11.2% in 2016).
The results of the election can be viewed on CIVS.
The four candidates elected are Pascal Fontaine, Sophie Tourret, André Platzer, and Jürgen Giesl.
In the first meeting of the new board of trustees on October 19, Jürgen Giesl was elected as the new president of CADE Inc.
The new board of trustees is therefore:
On behalf of CADE Inc., I would like to thank Jasmin Blanchette, Laura Kovács, Aart Middeldorp, and Christoph Weidenbach for serving on the board of trustees, and Christoph Weidenbach for his work as the CADE president 2016–2022. I would like to congratulate Sophie Tourret, André Platzer, and Jürgen Giesl, who will join the board as new elected trustees, and Pascal Fontaine for being reelected. Finally, I would also like to thank Cezary Kaliszyk for running in the election.
My research covers various theoretical and practical aspects of automated deduction, mostly focused around SMT. CADE is my home conference. I attend CADE and IJCAR whenever possible. I believe that our (CADE) community is welcoming fundamental and theoretical works (that can sometimes be overlooked elsewhere because of lack of immediate applications), as well as more experimental and practical works (that can sometimes be overlooked elsewhere because of a lack of appreciation of the enormous amount of energy to develop software and practical experiments). Besides being open to a large range of research, I also believe our community is a friendly one, it is open to new ideas and is welcoming of new people, notably young PhD students. All these nice aspects must be preserved and improved, and this requires constant attention from all, particularly from PC chairs, PC members, and the Board of Trustees. I am thus honored to be nominated for the Board of Trustees. Elected or not, I will continue to work at my place for these important aspects in our research.
The Board of Trustees is crucial in maintaining an open and friendly environment for all, especially for young researchers. In particular, it is ensuring the continuity of the Woody Bledsoe Awards, the SAT/SMT/AR summer school and best student papers. Recently, the Bill McCune PhD Award was established. Besides sustaining these tools, I believe an important future work which is essential for openness is to think about hybrid conferencing. There is nothing equivalent to in-person attendance, but in-person is not always possible. There are financial aspects, people might not be able to attend in-person for health or family reasons, some are impacted by travel restrictions or difficulties to get VISAs, master students would not come for a week without funding, and an increasing number of people also have ethical concerns with traveling. The possibility to attend a talk remotely is probably something we could offer systematically for CADE to the world, for a reasonable price, without impacting at all the experience of the people attending in person. So why not do it? I believe this would contribute to openness towards many who for some reason cannot attend in person. This would give to master students a window to state-of-the-art research in automated deduction, and it might contribute to attract excellent PhD candidates. Were CADE remote attendance free, I would definitely advertise the conference to all students in my Logic course, and if remote attendance cost was not free but reasonable, I would fund attendance for a few selected master students each year. As a concrete example of a contribution as an elected member of the Board of Trustee, I would like to bring this discussion to the Board, so that this point is thoroughly discussed.
I still believe that the current cycle of conferences, CADE alternating with IJCAR, and IJCAR as a part of FLoC every four years, is the right organization for the current situation, since it preserves the specificity of CADE and of the other compound conferences of IJCAR. This must be done with coordination between CADE and the friend conferences like FroCoS, ITP, and Tableaux, e.g. to adjust dates and locations, and maybe sometimes experiment colocation.
My goal as a trustee would be to ensure that CADE keeps on being the main conference for all research in the area of automated deduction. Therefore, the scope of CADE should remain as broad as possible. CADE should be open to any aspect of automated deduction and it should cover everything from theoretical results and practical contributions up to applications of automated reasoning.
I also think that it is very important to attract tool submissions, and to organize tool competitions co-located with CADE. (Since its foundation in 2004, I have been active in the termination competition, which took place during IJCAR/CADE several times.)
I am also in favor of continuing the publication of CADE as an "open access" publication within LNCS, similar to the proceedings of CADE 2021 and IJCAR 2022.
I think the current organization of CADE as a stand-alone event every second year, within IJCAR every other year, and within FLoC every four years is still a very good solution to guarantee the visibility of CADE on its own, while keeping in close contact with neighboring meetings and fields.
To attract as many participants as possible and to allow students to attend the conference, I think CADE should aim at affordable conference fees and continue the very good tradition of Woody Bledsoe travel grants for students. While I am in favor of having physical meetings again, online participation should be possible as well to allow attendance also for researchers who cannot travel, e.g., due to financial or health constraints.
My own research is concerned with different aspects of automated deduction. Therefore, I have been attending and publishing papers at CADE since 1994. In particular, I am working on techniques and tools to analyze properties like termination or complexity of programs automatically.
I was one of the PC chairs of IJCAR 2010, PC chair of RTA 2005, Steering Committee chair of RTA (2005-2007), Area Editor of ACM TOCL (since 2013), SC member of FSCD (since 2022), and I served many times on the PCs of CADE, IJCAR, RTA, LPAR, FSCD, and several other conferences in the field. I have been CADE trustee from 2010-2011 and from 2014-2020.
I am honored to be nominated for the CADE Board of Trustees. Having joined CADE for the first time in 2011, I am among the younger members of the CADE community. I have been a PC member of IJCAR and CADE and have been involved as a PC member in several conferences related to automated deduction including ITP, FroCoS, CPP, IJCAI, and NeurIPS.
My research is centered around automation for proof assistants, as well as automated reasoning systems based on higher-order logic and type theory. I work both with symbolic approaches and heuristics for sound and complete calculi, as well as with machine learning approaches that may be incomplete but are often able to prove more conjectures in practice.
As a CADE trustee I would support attractive cost-effective open-access options. CADE is already a very open community but I would further welcome automation in the emerging non-classical logics and interdisciplinary applications. I also support the travel awards and best paper awards that make the community more accessible to younger scientists.
Because CADE has exciting research to share, I believe that CADE should be open, welcoming, and first-rate. All CADE publications should be Open Access, because CADE findings are too important to be overlooked by researchers in other fields or with limited library access. The CADE community needs to continue its traditional strength of being particularly warm and welcoming to young researchers. And CADE (along with IJCAR) has to be more widely recognized as the flagship conference in automated reasoning that it is.
Along with my CADE-28 conference co-chair Marijn Heule and PC-co-chair Geoff Sutcliffe, I took a pioneering role in making the CADE-28 proceedings Open Access while I served as conference and PC co-chair. While CADE-28 showed that, with good contacts to publishers and funding sources, Open Access CADE can be cost-effective, CADE still needs a longer-term strategy to balance cost, increase Open Access, but retain or increase CADE publication quality.
CADE is very welcoming to young scientists. But I believe it can do better by investing in the future with an automated reasoning summer school right before CADE. This will enable PhD students to pick up interesting background for the conference and grow into an international young scientists community before the main CADE conference even gets off the ground, which is particularly important to broaden CADE's scope, e.g., in reasoning applications and interdisciplinary research.
I am a passionate believer that deduction is a central significant element of logic, which is why I championed and organized the ACM SIGLOG affiliation of CADE when I co-chaired CADE-28. That is why, alongside LICS and CAV, CADE now has a representation in ACM SIGLOG, which I believe should become CADE's long-term perspective to be heard.
If we play our cards right as a community, then CADE has a strong future ahead.
My background: I am the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology (KIT) and lead the Logical Systems Lab at Carnegie Mellon University. My research characterizes the logical foundations of cyber-physical systems and answers the question how we can trust a computer to control physical processes. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. I pursue this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees, such as in our KeYmaera theorem provers.
I have contributed as an author to CADE/IJCAR (where the largest percentage of my papers are published), shared my views on logic and proofs in an invited talk at IJCAR 2016, served on several CADE/IJCAR PCs, and have been co-chair of CADE-28 in 2021. I serve on the editorial board of the Journal of Automated Reasoning, Acta Informatica, and the ACM Formal Aspects of Computing.
I work in automated reasoning since my PhD. CADE and IJCAR are the venues where I feel at home. I have been on the program committee of these conferences in their last two occurrences. Additionally, in 2021 I spammed the world as CADE's publicity chair, and this year I served as IJCAR's workshop co-chair. I am also in the steering committee of PAAR since 2020 and editor of the AAR newsletter since 2017.
My research interests revolve around first- and higher-order classical logic. In particular, now that superposition works in higher-order logic, I want to make higher-order SMT work even better, for which I am looking into higher-order quantifier instantiation. I am also interested in using Isabelle to verify theoretical (AR) results. I would love to see more formally verified AR results at CADE.
I support CADE's recent move to open access and would like its application to be more straightforward. I also believe we should make more efforts concerning reproducible research, e.g. by taking inspiration from venues such as CAV, or by making general-purpose open repositories such as Zenodo mandatory for archival of scripts, binaries and experimental results. In general, I also want to encourage the adoption of implementation guidelines (or good practices) in the community.
Since Alan Robinson's milestone paper on “A Machine-Oriented Logic Based on the Resolution Principle” in 1963, saturation-based Automated Theorem Proving (ATP) has received a lot, arguably the most, attention from the ATP community. (We should not neglect to acknowledge the efforts in other paradigms, e.g., the connection method, tableaux, etc., which have also made great contributions to the field - see more about these below.) In this note I focus my attention on saturation-based ATP, and the many implemented systems such as Otter, Prover9, SPASS, Vampire, E, Zipperposition, etc. I claim that our fixation on proving theorems, as opposed to other types of ATP, has given saturation-based ATP more attention than it might deserve. In particular: (i) Explainable proofs are becoming increasingly important in applications of ATP, and saturation- based ATP proofs are very hard to explain; (ii) Model finding is emerging as an equally important type of ATP, and saturation-based ATP is poorly suited to model finding. Taking each of these claims in turn:
Explainable Proofs:
"Explainable AI" is a buzz phrase of the present, with
a plethora of papers and projects around the world. The ATP corner of AI is
part of the wave, and explainable proofs are becoming increasingly important.
Proofs from saturation-based ATP systems are hard to explain, for two main
reasons: Firstly, proofs are typically by contradiction, showing that the
axioms and negated conjecture lead to falsity. Such proofs are mostly
counterintuitive to humans - as soon as the negated conjecture gets involved,
formulae in the proof are "wrong". Forward proofs from the axioms to the
conjecture are much easier for users to understand. There have been attempts
to convert proofs by contradiction into forward proofs, but this is not
standard practice. Secondly, most saturation-based ATP systems convert
formulae (or subsets of their formulae) into a lower logic, e.g., from
higher-order formulae to first-order formulae, from first-order formulae to
clause normal form, and from higher forms to propositional logic. This allows
efficient reasoning to be done in the lower logic, helping to establish the
existence of a proof in the higher logic. While this technique is highly
effective, the resultant proofs are nigh impossible to understand, even
without the complication of proof by contradiction. Lifting proofs in lower
logics back to their original higher logic form is necessary for
explainability, but this is rarely if ever done in the proof output. Thus
overall saturation-based ATP systems largely fail to provide explainable
proofs. (Proofs from tableau-based ATP systems, particularly non-clausal
tableau, are often easier to understand, but sadly current tableaux-based
ATP systems are not nearly as powerful as the saturation-based systems.)
Model Finding:
The importance of model finding is most prominent in fault
finding applications of ATP, e.g., in software verification. Here the
(counter-)model for a proof obligation points to the location of the fault.
Other important applications of model finding include checking the consistency
of an axiomatization and disproving conjectures. The models that are sought
for these tasks may have finite or infinite domains, infinite domains may be
explicit (e.g., the integers) or implicitly the Herbrand Universe, and Kripke
interpretations may have a finite or infinite number of worlds. Regardless
of the cardinalities, applications that use ATP systems to find models
typically need an explicit model with a domain and symbol mapping. The models
output by saturation-based ATP systems are, as the name suggests, saturations
that embody a Herbrand interpretation, but are pretty much impossible to
interpret explicitly in a way that can be used constructively by users. This
weakness has been recognized, and finite domain model finders such as Mace and
Paradox have helped fill the gap. Some saturation-based ATP systems also
include a finite model finder in their disproving schedules. Models with
infinite domains are obviously necessary as soon as the formulae contain any
numbers, and infinite domains are necessary in other non-numeric applications,
e.g., those that involve modelling time. The only ATP system I know of that can
produce a explicit infinite domain model is cvc5 (I think!), and saturation-
based ATP systems just cannot help here.
Summary:
Saturation-based ATP is a success story of which the ATP community
can justifiably be proud. But maybe it's time to invest more effort into other
types of ATP that provide greater explainability and greater capability for
finding explicit models. The TPTP World is currently evolving in the area of
model finding, with forthcoming standards for model representation (finite,
infinite, and Kripke). The TPTP problem library provides many challenges for
theorem proving, theorem disproving, and model finding. Contributions of more
challenges are always welcome, to reflect the needs of ATP users as new and
exciting applications of ATP emerge.
EuroProofNet is the European research network on digital proofs. EuroProofNet aims at boosting the interoperability and usability of proof systems. The aim of EuroProofNet working group 2 on Automated Theorem Provers is to promote the output of detailed, checkable proofs from automated theorem provers. This working group is working towards an inventory of available automated reasoning systems producing or verifying proofs, and proof and exchange formats. It is organized as a Wiki hosted at GitHub.
We invite every designer or developer of
For details on how to contribute to the inventory, please see here.
If you are not yet member of the EuroProofNet research network, you can join for free on e-COST.
UNESCO proclaimed 14 January to be World Logic Day, a global day of supporting the development of logic through teaching and research, as well as to public dissemination of the discipline.
The coordination of World Logic Day 2023 is -- for the third time -- in the hands of the Conseil International de Philosophie et des Sciences Humaines (CIPSH) and its member organization, the Division for Logic, Methodology and Philosophy of Science and Technology of the International Union of History and Philosophy of Science and Technology (DLMPST/IUHPST).
We would like to encourage logicians all around the world to organize (possibly small) events in close proximity to 14 January 2023 to celebrate this day. The Covid pandemic still has an effect on international travel and the question whether in person meetings are appropriate; in addition, we have learned over the last years that online meetings are easier to finance, better for the environment, and considerably more inclusive.
As a consequence, we should like to ask all organisers to weigh pros and cons of planning in person events, purely online events, or hybrid events before making an announcement. Note that online and hybrid events have the advantage of allowing easy access of people from around the world. Events will be listed on the CIPSH website.
To be added to that list, follow the instructions here or write a short email there.
The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting.
The Herbrand Award has been given in the past to:
A nomination is required for consideration for the Herbrand Award. Nominations can be submitted at any time. The deadline for nominations to be considered for the Herbrand Award 2023, which will be given at CADE-29, is
March 31 2023Nominations 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.
The ``Dov Gabbay Prize for Logic and Foundations'' is an international research prize established to honour the extraordinary, multi-faceted, and ongoing scientific and editorial work of Prof. Dov Gabbay, known in particular for editing an extensive collection of specialized Logic Handbooks. It has been launched on the occasion of his 77th birthday (for a short bio, see here).
The prize rewards outstanding researchers in Logic and Foundations, including Mathematical, Philosophical, and Computational Logic. It promotes work able to inspire current and future generations of logicians, if not a broader audience, ideally combining deep foundational insight and conceptual innovation with sophisticated theoretical analysis.
The winner will receive 2001 EUR and be invited to give a talk (accessible for an online audience) at a major logic centre or a logic-related meeting in 2023, the choice depending on the recipient's research area. Additional efforts will be made to promote the rewarded scientific work.
Nomination
Each nomination has to specify the researcher, provide a justification accessible to non-expert logicians (0.5-2 pages), and list the publications considered relevant.
It also has to include the name, affiliation, and email address of the nominator. Self-nominations are not allowed, the nominator should not depend on the nominee.
Proposals in pdf-format have to be sent by email. The deadline for this call is January 31, 2023.
Decision
The decision is made by an independent selection committee consisting of six internationally renowned logicians representing Mathematical, Philosophical, and Computational logic (for details, see here). The jury can decide to attribute no prize in a given year. The winner of the 2022 call will be announced in May 2023.
Admin
Prize and process are managed by the "Logic and Foundations Initiative (ILOAF)", which aims at initiating and supporting scientific and educational activities in Logic and Foundations. It is currently sponsored by the Luxembourg Logic Community.
Contact
For any questions, please contact the organizing committee (only) via email.
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 what siglog, eatcs, and eacsl say about it.
The 2022 Alonzo Church Award was given to Dexter Kozen for his ground- breaking work on the theory and applications of Kleene Algebra with Tests. Lists containing this and all previous winners can be found through the links above.
Eligibility and Nominations
The contribution must have appeared in a paper or papers published within
the past 25 years. Thus, for the 2023 award, the cut-off date is January 1,
1998. 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 2023 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 2023 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 Mariangiola Dezani using this email address and that one by February 1, 2023.
Presentation of the Award
The 2023 award will be presented at the 50th EATCS International Colloquium
on Automata, Languages and Programming, which is scheduled to take place in
Paderborn - Germany on July 10-14, 2023. 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.
Award Committee
The 2023 Alonzo Church Award Committee consists of the following five members:
Thomas Colcombet, Mariangiola Dezani (chair), Marcelo Fiore, Radha Jagadeesan, and
Igor Walukiewicz.
Tommaso Flaminio and Hykel Hosni invite submissions for a Special Issue on Logics for the new AI Spring, to be published with the International Journal of Approximate Reasoning.
The development of logics capable of representing human-like reasoning has always been one of the central objectives of logic-based Artificial Intelligence. In addition to providing very successful tools for knowledge representation and reasoning, logic-based AI is now facing the new and pressing challenge related to the integration of symbolic and sub-symbolic AI. In pursuing it, logic can once again shape significantly the future developments of AI. The primary goal of this special issue is to gather cutting-edge contributions which will jointly provide a comprehensive state-of-the-art in the subject.
To achieve this, the scope of the special issue focuses on, but is not limited to, the following topics:
Important: Given the goal of the special issue, authors are strongly encouraged to put forward as clearly as possible why and how their contribution can be seen to provide an element of the state-of-the-art in “Logic for Artificial Intelligence”. Failure to do so may lead to desk-rejection.
Instructions: Authors should prepare their manuscripts according to the "Instructions for Authors" guidelines of the International Journal of Approximate Reasoning outlined at the journal website.
Submissions are expected to be written in LaTeX following the Journal’s template. All papers will be peer-reviewed according to the standard procedure.
All manuscripts should be submitted electronically through Editorial Manager ®. When submitting papers, please select Article Type as "VSI:Logics for the new AI spring".
Submission Deadline: 1st March 2023.
Keywords: Logic for AI; Machine Learning, Knowledge Representation; Symbolic AI; Hybrid systems.
Guest editors:
Further information is available from the IJAR website.
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry require advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is an annual forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems.
New developments and emerging applications like autonomous software for uncrewed deep space human habitats, caretaker robotics, Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), and the need for system-wide fault detection, diagnosis, and prognostics provide new challenges for system specification, development, and verification approaches. The focus of these symposiums are on formal techniques and other approaches for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle.
Topics of Interest:
We encourage submissions on cross-cutting approaches that bring together
formal methods and techniques from other domains such as probabilistic
reasoning, machine learning, control theory, robotics, and quantum
computing among others.
Important Dates:
More information is available on the symposium's web page.
The 29th edition of the SPIN symposium aims to bring together researchers and practitioners interested in automated tool-based techniques to analyze and model software for the purpose of verification and validation. We invite submissions presenting theoretical results, novel algorithms, tool development, and empirical evaluation. We accept both long (up to 16 pages) and short (up to 6 pages) papers.
Important dates
More information is available on the symposium's web page.
The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric. Suggested, but not exclusive, topics of interest include:
Important Dates for Papers
Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is given by anywhere on earth (AoE).
LICS 2023 Call for Workshop Proposals
Researchers and practitioners are invited to submit proposals for workshops on topics relating logic -- broadly construed -- to computer science or related fields. Typically, LICS workshops feature a number of invited speakers and a number of contributed presentations. LICS workshops do not usually produce formal proceedings. However, in the past there have been special issues of journals based in part on certain LICS workshops.
Proposals should include:
Important Dates for Workshop Proposals
The workshops selection committee consists of the LICS Workshops Chair, the LICS General Chair, the LICS PC Chair and the LICS Conference Chair.
More information is available on the symposium's web page.
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 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. TASE 2023 aims to provide a forum for people from academia and industry to communicate their latest results on innovative advances in software engineering.
Topics
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 symposium's web page.
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.
ICALP is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). As usual, ICALP will be preceded by a series of workshops, which will take place on July 10.
The 2023 edition has the following features:
Papers presenting original research on all aspects of theoretical computer science are sought. Typical but not exclusive topics of interest are:
Track A: Algorithms, Complexity and Games
Important dates and information
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.
ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include, but are not limited to, the following:
Important Dates (AoE)
More information is available on the conference's web page.
Started in 2002, the CLA workshops provide an open, free access forum for interdisciplinary research concentrated around combinatorial and quantitative aspects of mathematical logic and their applications in computer science.
Topics within the scope of CLA include:
Important dates
More information is available on the workshop's web page.
This symposium aims to provide a supportive environment in which selected PhD students can present and discuss their ongoing work, meet other students working in the field of formal methods, and receive feedback and advice from experienced researchers. In addition to talks followed by discussions, the event will also provide opportunities for PhD students to meet senior academics in smaller groupings, to informally discuss research strategies, career aspects, or any other topic of interest.
If you are a PhD student researching any topic that falls within the area of formal methods, you are warmly invited to submit a Research Abstract for consideration to be selected as a participant of the Doctoral Symposium.
There will be a best presentation award.
Important Dates
More information is available on the symposium's web page.
The goal of the workshop is to bring together people from different fields such as algebra/coalgebra, verification, logic, around the thematic of fixed points. This workshop will be without proceedings. In particular you can present work that is already published elsewhere, or in progress. Depending on the nature of the contributions, a special issue of Fundamenta Informaticae might be published with selected contributions (we have the approval by the journal for this).
Fixed points play a fundamental role in several areas of computer science. They are used to justify (co)recursive definitions and associated reasoning techniques. The construction and properties of fixed points have been investigated in many different settings such as: design and implementation of programming languages, logic, verification, databases. Topics include, but are not restricted to:
Important dates
Assia Mahboubi and Enrico Tassi are organizing a winter school titled
The Mathematical Components library
in Sophia-Antipolis (Nice) from Monday 5th December 2022 to Friday
9th. On Wednesday of the same week we are organizing the workshop
Mathematical Components - 10 years after the Odd Order Theorem
The school will be in English and will target master or PhD students with basic knowledge of Coq. The course will introduce the SSReflect proof language and the Mathematical Components library, in particular its key principles and tools.
Although the workshop is part of the program of the school, it will be a standalone event not restricted to the participants to the school.
Both events will be held in person (pandemic permitting of course). Both events are free, no subscription fees, but registration is mandatory. Please email Enrico Tassi to register (subject “MC2022”).
More information is available on the school's web page.
The Logic Summer School @ ANU is open for registration as an in-person event
Check out the program and register on the school's web page.
VerifyThis is an annual program verification competition held as part of ETAPS. It is an opportunity for community members and tool authors to showcase their work and learn from each other with hands-on exercises.
The competition proceeds in three rounds. In each round, participants are given 90 minutes to implement and prove specified properties of a given algorithm and/or data structures. They are free to use any verification tools they choose.
We are looking for problem submissions. If you have recently encountered an interesting challenge in your work, don’t hesitate to submit it. Typical challenges have clear input-output specifications and often incorporate one or more of the following: heap allocation, concurrency, arithmetic reasoning. A challenge usually describes a problem using natural language together with some pseudocode, and then provides a list of properties or “verification tasks” of varied levels of difficulty. Contributors are encouraged to look at the Archive of previous problems on the VerifyThis web site, at the URL above.
An award will be given for any submission used in the competition.
To avoid spoiling the competition for others, we ask that you keep the subject of your submission private.
Submissions should be sent by email to Xavier Denis and Stephen Siegel.
Submission Criteria:
More information can be found on the competition website.
The Max Planck Institutes (MPIs) in Computer Science have several research opportunities for strong students. Please help spread the word about them:
About the MPIs: The participating institutes are part of a network of over 80 Max Planck Institutes, Germany’s premier basic-research organisations. MPIs have an established record of world-class, foundational research in the sciences, technology, and the humanities. They offer a unique environment that combines the best aspects of a university department and a research laboratory. All the programs listed above are highly selective, and the participating institutes use English as their working language.
We are looking for two bright and motivated PhD student for two 3-year PhD positions. The main research topics of the two PhD positions are, respectively: (1) verifying that distributed applications respect correctness, safety and reliability specifications; and (2) verifying the privacy and security goals of distributed programs and their interaction.
Project Description The two positions are part of the upcoming Horizon Europe project TaRDIS (Trustworthy and Resilient Decentralised Intelligence for edge Systems). The project goal is to design and develop a novel, event-driven programming model and toolkit (with solid foundations based on formal methods) to help programmers in creating safe and reliable distributed applications. The focus lies on distributed applications with smart and autonomous components deployed across the cloud-edge continuum.
Project TaRDIS is a collaboration between DTU, NOVA University Lisbon (Portugal, project coordinator), the University of Oxford (UK), the University of Novi Sad (Serbia), the National and Kapodistrian University of Athens (Greece), and 6 industry partners.
Responsibilities and Qualifications If you join this project, you will become a member of the DTU Compute research section on Software Systems Engineering, which involves researchers in various areas of software specification, verification, engineering, and security --- with a strong emphasis on formal methods. You will also join the DTU Compute PhD school and take part in its courses and activities. As part of your PhD training and research activities, you will have research stays at the academic collaborators' universities. Links:
Your main tasks within this project will be:
To be considered for the position, you need some experience with formal methods for programming languages, or distributed systems, or security. You will need to document these skills by listing the relevant university courses you took, or the relevant experience you have.
It will be an advantage if you can also document good programming skills – preferably including functional programming, and some experience in developing distributed applications.
To begin the PhD position, you must have a two-year master's degree (120 ECTS points) or a similar degree with an academic level equivalent to a two-year master's degree. You can apply prior to obtaining the degree, providing the expected graduation date.
Assessment and Further Details
The assessment of the applicants will take place in early December 2022.
For the application details, see here.
For further information and inquiries, please contact:
You can read more about DTU Compute here. You can read more about the DTU Compute Research Section on Software Systems Engineering here. If you are applying from abroad, you may find useful information on working in Denmark here.
The Department of Computer Science and Technology is seeking to recruit a new faculty member at the Assistant or Associate Professor level who can contribute to research and teaching in the area of Logical Foundations and Formal Methods.
The Computer Science department in Cambridge has a long history of research in logical foundations and formal methods, from groundbreaking work on higher-order logic and the proof assistant Isabelle, through to a wide range of important semantic frameworks, such as bigraphs, event structures, and nominal sets. Today logical foundations and formal methods is a thriving area of activity, which is explored with a wide variety of mathematical and logical tools, including category theory, domain theory, finite model theory, linear logic, operational semantics, proof assistants, and type theory.
We seek to appoint a new member of faculty to complement and enhance our research in this area. The position is open to researchers working in the area of formal methods and logical foundations of computer science, broadly conceived. While no list of topics could be exhaustive, potential candidates might work in the areas of automata theory, automated deduction, categorical syntax and semantics, descriptive complexity, homotopy type theory, modal or temporal logic, rewriting, or type theory, as could researchers applying formal or logical tools in concurrency theory, databases, networks, programming languages, quantum computing and other emerging models of computation, or verification.
The ideal candidate for this position will have a strong international track record of publication and impact commensurate with their research area and experience. They will have the ability, or potential, to secure research funding to support their research vision and build a world-class team of researchers. We welcome applications from researchers with interdisciplinary interests who will collaborate with people across different subdisciplines in Computer Science and Technology and with other academic disciplines. Collaborations outside academia are also highly-valued, including with industry and third-sector organizations.
The University actively supports equality, diversity and inclusion and encourages applications from all sections of society.
The deadline for applications is December 5, and the link to our advertisement is here.
Yao Li is looking for Ph.D students (starting Fall 2023) who are interested in programming languages, formal verification, and/or interactive theorem proving to join his new group at Portland State University.
He is a new assistant professor at Portland State University. His research aims to
Please feel free to drop him an email if you are interested or if you have any questions about his research, his group, or Portland State University.
Postdoctoral research positions at Virginia Tech, USA or The Open University, The Netherlands are available on a DARPA project at the intersection of formal verification and binary analysis. Project goals include developing trustworthy tools for reasoning about security exploits in binary code. Opportunities exist to investigate a broad set of topics including logic frameworks for automatic reasoning of security vulnerabilities, verified decompilation, auto-generation of trustworthy security analysis tools, and automatic patching with provable security properties. Opportunities also exist to investigate project-relevant topics of mutual interest.
Recent computer science PhD graduates with expertise in any of the following areas are sought: formal verification, proof assistants and verification tools, binary/program analysis, or compilers. The positions are available either at Virginia Tech or The Open University (or a combination with time at both universities) and have no teaching obligations. For experienced candidates, Research Assistant Professor appointments at Virginia Tech (inclusive of funding for graduate students) are possible.
Interested candidates are requested to contact Prof. Binoy Ravindran with a CV or for any questions.
The Computer Science Department at the University of Oxford is hiring four new faculty. The positions are open to all areas of computer science. The closing date is 12 noon on 14 December 2022. For more information, see here.
Juan Aguilera is offering a postdoctoral fellowship in Mathematical Logic at the research group in Computational Logic of the Institute of Discrete Mathematics and Geometry at the Technical University of Vienna (TU Wien) in Vienna, Austria.
The position is for 20 months, with the possibility of extension up to 36 months. It is funded by a grant from the Austrian Science Foundation (FWF) led by Juan P. Aguilera. The fellow will conduct research independently, as well as together with Dr Aguilera and with the other members of the research group in Computational Logic and of the Institute of Discrete Mathematics and Geometry. Moreover, the research group has ties to other Logic groups in and outside of Austria, most notably the Logic and Analysis group at Ghent University, and international collaborations will be possible and encouraged.
Topic
The main goal of the post-doctoral fellowship is the use of methods from infinitary proof theory to attack some specific problems in Descriptive Set Theory. The fellow is to carry out research independently, as well as together with other group members. Applicants should hold a PhD (or be close to obtaining one) in Logic and have an excellent research record, as well as experience in at least one of the following areas:
Application
Applicants should email Juan Aguilera at this address or this one and include all relevant documents as attachments.
Practical Information
The salaries for the doctoral and post-doctoral positions are those set forth by the Austrian Science Foundation according to the Collective Bargaining Agreement.
The beginning of the fellowship could be as late as November 2023, and as early as December 2022; the precise starting date is flexible. We will carry out monthly reviews of applications until the position is filled.
The Computing Foundations cluster at the School of Computing, The Australian National University, have multiple PhD scholarships available in areas relevant to the types community, including logic, programming languages, systems, formal methods, theory and software engineering.
If you want to do cutting edge research in any of these fields, or a mix thereof, visit our page and get in touch with any of the staff listed. Please also contact Michael Norrish (cluster lead) for further details.
The LIRMM (UMR 5506, University of Montpellier, CNRS) is recruiting a full-time research engineer for a period of 12 months in the field of automated proof. The desired start date is January 1, 2023, and the position will be located in Montpellier (France).
Assignments:
The purpose of this position is to strengthen the software development capabilities of the MaREL team (specialized in the field of software engineering) of the Computer Science department of LIRMM. The person hired will be involved in the development of Goéland, an automated reasoning tool developed in the team by Julie Cailler (PhD student) for over a year. This tool is based upon a new proof search procedure for first-order logic, which leverages concurrency to produce proofs in the context of the tableaux method. This tool currently gives excellent results (as measured by the number of solved problems) in comparison with similar tools. Notably, it achieves better results in some problem categories than similar (tableaux-based) tools, some of which have been established for years. A conference article on Goéland has been accepted for publication at IJCAR 2022, a rank A conference, demonstrating the interest of the community for the approach used by that tool. Furthermore, Goéland has taken part in the CASC-J11 competition, organized in parallel with IJCAR 2022, and in which the current best automated deduction tools compete on different sets of problems. The tool has been awarded the “best newcomer” distinction during this competition.
The hired person will participate in the development and maintenance of the Goéland software, which is developed using Go, a language suited to concurrent programming. The aim of this position is twofold. The first mission is to get the tool in working for competitions, particularly CASC, a yearly occurrence that serves as a display of our work. The second is to apply the tool in a more industrial setting. A benchmark of problems originating from the modeling of industrial applications with the B method is already available (as a result of the ANR project Bware) but a number of extensions to Goéland are needed before it can be used on this benchmark.
In more detail, the assignments of the hired person will include:
Activities:
The hired person will work under the direction of David Delahaye (PR/full professor in the team MaREL), Simon Robillard (MCF/associate professor in the team MaREL), and Julie Cailler (PhD student in the team MaREL, with a thesis on the topic, and the main developer of Goéland).
The technical program follows the assignments described in the previous section. The order of assignments is not critical, with the exception of tests on the BWare benchmarks, for which the integration of polymorphism and linear arithmetic reasoning are prerequisites.
Skills:
The candidate must demonstrate the following:
Context:
LIRMM (Laboratoire d'Informatique, de Robotique et de Microélectronique de Montpellier) is a research department (unité mixte de recherche) headed by CNRS and the University of Montpellier. It hosts 410 employees, including 192 permanent positions. It is organized in three divisions: Computer Science, Robotics and Micro-Electronics, as well as centralized services, among which the Research Support Service (SAR, comprising 16 engineers) that provides technical support for research projects and manages the technology platforms of the department. The hired engineer will join this service and provide support for researchers in the department.
The research topics of the Computer Science division cover a large spectrum ranging from the foundations of computer science (algorithms, computation, data science, software engineering, AI) to inter-disciplinary research (environment, health, biology). This division hosts 106 permanent positions (researchers, teacher-researchers and engineers) and 71 PhD students in 15 teams.
The hired person will more specifically join the MaREL team.
Contact : To send your application or simply to have more information about this position, contact the following people:
This is a call for interest for PhD and postdoctoral research at Yoni Zohar’s group in Bar-Ilan University.
The positions will focus on Satisfiability Modulo Theories (SMT) methods for verification of smart contracts, as well as for bit-precise reasoning.
The work will be done in collaboration with the University of Iowa and Stanford University.
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.
Starting date is planned for 2022-2023.
The group of André Platzer, the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems, in the Department of Informatics at KIT is recruiting a PhD student or postdoc (TVL E13, full-time). Our research develops the logical foundations for cyber-physical systems and practical theorem proving tools for analyzing and correctly building such systems, including the theorem prover KeYmaera X, verified runtime monitoring ModelPlex, verified compilation, and verified safe machine learning techniques. Our techniques are used to analyze the safety of autonomous cars, airplanes and collision avoidance protocols in aerospace applications, robotics, and train control.
Key requirements for successful applications:
The successful candidate is able to quickly get into new research areas and will be responsible for actively engaging in novel research questions, publishing and communicating research results, advising junior students, assisting in research grants, implementation of research results in formal methods tools, and demonstrating their applicability in cyber-physical systems applications.
Faculty / Division: Alexander von Humboldt Professor on Logic of Autonomous Dynamical Systems
Institute: Institute of Information Security and Dependability (KASTEL)
Starting Date: Immediately
Contact Person: André Platzer (web site).
Vincent Rahli would like to invite applications for an up to 3 years fully-funded postdoctoral position within the School of Computer Science at the University of Birmingham (see below for details on how to apply).
The successful candidate will contribute to an EPSRC-funded project aiming at designing and formally verifying distributed systems, in particular Byzantine fault-tolerant distributed systems as used for example in blockchain technology.
The start date is flexible, ideally early 2023.
The environment:
The School of Computer Science has large and thriving Theory and Security research groups. Among our research interests related to this project are for example:
How to apply:
Interested people are encouraged to contact Vincent Rahli by email to discuss their research interests and details of the positions. Further information on how to apply is available here
Within the TCS Group of the Department of Computer Science at the University of Innsbruck, Austria there is an opening for a 4 year PhD student position; kindly see here for further details.
Applications (including CV, short letter of motivation, three references) should submitted via the following link no later than December 22, 2022. Informal inquiries may be sent to Georg Moser.
The city of Innsbruck is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of urban life in this historic town and the Alpine environment provides a high quality of living.
Further information is available from the following links: