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 and Bill McCune Award selection committee, instituting new awards, etc.
Nominations for four CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2022.
The current members of the board of trustees are (in alphabetical order):
The terms of Pascal Fontaine, Laura Kovács, Aart Middeldorp, and Christoph Weidenbach end. Pascal Fontaine and Aart Middeldorp may be nominated for a second term, whereas Laura Kovács and Christoph Weidenbach have already served two consecutive terms and cannot be nominated this year.
The term of office of Jasmin Blanchette as IJCAR 2022 programme chair ends after the IJCAR conference. As outgoing ex-officio trustee, Jasmin Blanchette is eligible to be nominated as elected trustee.
In summary, we are seeking to elect four trustees.
Nominations can be made by any CADE member, either by e-mail or at the CADE business meeting at IJCAR 2022; since nominators must be CADE members, they must have participated at at least one of the CADE or IJCAR conferences in the years 2019-2022. 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
Christoph Weidenbach, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of CADE Inc.
We invite proposals for sites around the world to host the international Conference on Automated Deduction (CADE) to be held in summer 2023. CADE typically merges into IJCAR (the International Joint Conference in Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome.
The deadline for proposals is 30 June 2022.
CADE's/IJCAR's recent location history is as follows:
The upcoming CADE/IJCAR event will be:
We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal deadline.
Proposals should address the following points that also represent criteria for evaluation:
Prospective organizers are encouraged to get in touch with the CADE Secretary and the CADE President for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers are encouraged.
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 May 15, 2022. 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:
When asked to write a column for the AAR newsletter, my first idea was to write about proofs in automated reasoning, and at the same time, advertise the new COST action EuroProofNet. (In case you are not aware of this COST action yet, let me insist that anyone in the automated reasoning community with an interest in proofs is very much welcome in the initiative). Then, after reading again the recent excellent column on proof certifications by Chantal Keller, I felt that writing again a full column focused on proofs would be redundant. So, let me take a step back and broaden the subject. Producing proofs is just one aspect of a greater goal that is dearest to my heart in research: enabling cooperation between automated reasoning tools.
Proofs are crucial for the cooperation of tools: an increasing number of applications interact with automated reasoning tools through proofs, or would like to. Proofs are important to improve the confidence in reasoning software, and help debugging them. For all those reasons, the energy we are currently putting in improving proof generation is justified. I believe there is another aspect of proofs in automated reasoning that is gaining importance: education. I just started this year to teach logic to computer scientist and engineering students. In a previous life more than fifteen years ago, I was teaching assistant for the same course in the same university. This experience gives me a before/after picture of the students, and I think it is relevant for us. Students change: they now speak better English, they are able to program in many different programming languages, and jump from one project to another in no time. But most of them do not know, coming from high school, what a rigorous proof is, and barely what a sound argumentation is. Maybe automated reasoning (including automated provers, SAT, SMT and proof assistants) is becoming a valuable and even necessary tool to teach rigour? Do you successfully use automated reasoning tools as a mean to teach logic and mathematical proofs? What, in your experience, works best for this?
After this digression about education, let me go back to my main subject. Proofs are instrumental for tools to cooperate. And standards are essential too. Our community is doing great, I believe, on the aspects of standards, with important initiatives and decades-long efforts, just to cite a few: TPTP and SMT-LIB.
We could probably do better for software. On the one hand, a great proportion of automated reasoning software is now open source. On the other hand though, the most successful projects tend to develop as monolithic, large tools, that require quite fairly big teams to maintain and evolve, and that are a bit hard to get into. Besides this path of success, the other software, after hesitating towards large successful projects, often join the pool of prototypes, that survive while one person takes care of it, and that disappear when the maintainer's other duties take precedence. These last software are absolutely essential for research, because they explore new directions, and among those directions the successful ones will eventually make it to the few main large projects.
Maybe we could however do a better job though, to build on all these experiments, to reuse the many hours of careful design and engineering put in the code. We might get some inspiration from Unix and Linux in their infancy (before service configuration tools and GUIs progressively engulfed an increasing number of orthogonal operating system aspects). Maybe our software should be organized as a myriad of small libraries, focused on one small task, cooperating in various ways, in various tools? Those libraries would be easier to maintain, to reuse, to experiment. They might outlive their creators, and be more useful for our community. Obviously this is not easy, but I firmly believe it is possible, at least for some. For instance, I have the impression we are nearly there for SAT solvers. We could soon be able to use off-the-shelf SAT solvers to build SMT solvers, without any need to adapt them. Maybe arithmetic theories (à la SMT) could be also designed as separate libraries? Do you also believe there are chunks of our software that we could factor out into smaller libraries? How could we encourage this?
If you would like to react or discuss one or the other question of this letter, you can subscribe to this zulip chat room.
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 OTTER, Prover9 and Mace 4, automated tools for first-order reasoning which are known to this day by its accuracy and robustness. He was also known for his generosity towards research colleagues and 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 sent to both Claudia Nalon and Pascal Fontaine, by April 15, 2021.
The nomination must consist of a compressed file (.zip) containing:
The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of Automated Reasoning.
Procedure
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 2021 consists of the following people (to be soon completed):
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 2022, which will be given at IJCAR 2022, is
April 30 2022Nominations 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
Christoph Weidenbach, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of AAR and 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 the siglog page, the eatcs page, and the eacsl page.
The 2021 Alonzo Church Award was given jointly to Georg Gottlob, Christoph Koch, Reinhard Pichler, Luc Segoufin and Klaus U. Schulz for their ground-breaking work on logic-based web-data extraction, and querying tree-structured data. 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 2022 award, the cut-off date is January 1,
1997. 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 2022 award are now being solicited. The nominating letter must summarize 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 should be submitted to Radha Jagadeesan by April 2, 2022.
Presentation of the Award
The 2022 award will be presented at the Federated Logic Conference 2022, which is
scheduled to take place in Haifa, Israel in July/August 2022. 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.
Principles of Knowledge Representation and Reasoning, Incorporated (KR Inc.) has established a KR Early Career Award to recognize and promote outstanding early career researchers in knowledge representation and reasoning. The award winner for 2022 will be announced at the 2022 KR conference in Haifa, Israel, in August 2022.
Eligibility
Eligible for the award is any researcher who completed their doctoral degree in 2020 or 2021.
Nominations Award candidates should be nominated by an academic familiar with their work (for instance, their PhD supervisor or a PhD panel member). Self-nominations or nominations by the Award Committee are not allowed. Unsuccessful candidates who completed their doctoral degree in 2021 can be nominated again next year.
How to Submit Nominations
Nominations should be submitted via Easychair.
The name of the candidate should be put in the Title field, and the email address, affiliation, and PhD defense date of the candidate should be listed in the Abstract box.
A single PDF file (extension .pdf) should be uploaded consisting of:
The deadline for nominations is March 31, 2022.
Nominations are now invited for the 2022 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2020 and 31 December 2021 are eligible for nomination for the award.
The deadline for submission is 1 July 2022. Submission details follow below.
Nominations can be submitted from 1 March 2022 and should be sent to the chair of the Jury, Thomas Schwentick, by e-mail.
The Award
The 2022 Ackermann award will be presented to the recipient(s) at CSL
2023, the annual conference of the EACSL.
The award consists of
The Jury
The jury consists of:
How to submit
The candidate or his/her supervisor should submit
The submission should be sent by e-mail as attachments to the chairman of the jury, Thomas Schwentick with the following subject line and text:
Since 1998, the Association for Logic, Language, and Information (FoLLI) has been awarding the annual E.W. Beth Dissertation Prize to outstanding Ph.D. dissertations in Logic, Language, and Information, with financial support of the E.W. Beth Foundation.
Nominations are now invited for outstanding dissertations in these areas resulting in a Ph.D. degree awarded in 2021.
The deadline for nominations is the 15th of April 2022.
Qualifications:
The prize consists of:
The prize will be awarded by the chair of the FoLLI board at a ceremony during the 33rd ESSLLI summer school, in Galway, August 8-19, 2021.
A two day logic conference to mark the 85th birthday of John N. Crossley will take place on the dates of 14-15 June 2022 (the sessions will be scheduled in AEST but they will be friendly to North-American and European time zones as well). This will be a fully online Zoom event (please contact the organizer, Guillermo Badia for the links).
Everyone is very welcome to attend!
The speakers will be:
More information is available on the conference's web page.
In 2020, Annals of Mathematics and Artificial Intelligence (AMAI) celebrated its 30th anniversary. Over the years, the journal has promoted better understanding of the application of quantitative, combinatorial, logical, algebraic and algorithmic methods to artificial intelligence areas as diverse as decision support, automated deduction, reasoning, knowledge-based systems, machine learning, computer vision, robotics and planning. AMAI special issues are intended to be collections of original research papers reflecting the intersection of mathematics and a focussed discipline demonstrating how each has contributed greatly to the other. A further goal of the journal is to close the gaps between the fields even further. Papers should report on current research in the appropriate areas, as well as more retrospective papers in which progress has been ongoing over a period of time.
The purpose of this special issue of AMAI is to promote research on theoretical and practical aspects of symbolic computation in software science, combined with recent artificial intelligence techniques. Symbolic Computation is the science of computing with symbolic objects (terms, formulae, programs, representations of algebraic objects etc.). Powerful algorithms have been developed during the past decades for the major subareas of symbolic computation: computer algebra and computational logic. These algorithms and methods are successfully applied in various fields, including software science, which covers a broad range of topics about software construction and analysis. Meanwhile, artificial intelligence methods and machine learning algorithms are widely used nowadays in various domains and, in particular, combined with symbolic computation. Several approaches mix artificial intelligence and symbolic methods and tools deployed over large corpora to create what is known as cognitive systems. Cognitive computing focuses on building systems which interact with humans naturally by reasoning, aiming at learning at scale.
The special issue is related to the topics of the The 9th International Symposium on Symbolic Computation in Software Science - SCSS 2021. Participants of the symposium, as well as other authors are invited to submit contributions.
Topics
This special issue focuses on advanced results on the topics that
include, but are not limited to, the following:
Deadline: May 23, 2022.
More information is available on special issue's web page.
The Logic Journal of the IGPL will publish a special issue in honour of Prof John N. Crossley on the occasion of his 85th birthday. The volume will contain invited contributions by students and collaborators of Prof Crossley in addition to any contributed submission that is found suitable after the appropriate review process. The list of invited authors includes Anil Nerode, Wilfrid Hodges, John Bell, Rod Downey, Rohit Parikh, Martin Wirsing, Lloyd Humberstone, Geoff Sutcliffe and Pimpen Vejjajiva. The issue will welcome submissions in the areas of history of logic, model theory, recursion theory, set theory, modal logic, constraint logic programming, and program extraction, particularly if they are related to Crossley?s work.
John Crossley started his career at the University of Oxford as the first university lecturer in mathematical logic in that institution, a position created with the help of Prof Sir Michael Dummett. Some years later, Crossley moved to Monash University (Australia) to become a Professor of Pure Mathematics (and later, Logic). He is the main author of Constructive Order Types (North-Holland, 1969) and has co-authored various books, including Combinatorial Functors (Springer, 1974), Adapting proofs-as-programs: The Curry-Howard Protocol (Springer, 2005) and What is mathematical logic? (OUP, 1972). The latter is a very celebrated text and the first introduction to mathematical logic produced in Australia. He was editor of the Journal of the Australian Mathematical Societyand he has also edited or co-edited half a dozen logic conference proceedings. He was the chair of the Committee for Logic in Australasia of the Association for Symbolic Logic for 16 years, a former president of the Australasian Association for Logic, and one of the creators of the Asian Logic Conference. John Crossley has had several doctoral students who have gone to become very prominent logicians, most famously, Peter Aczel, Wilfrid Hodges, John Bell and Rod Downey. According to the Math Genealogy Project, Crossley has 216 academic descendants, more than any other logician in Australia or New Zealand.
The submission deadline will be 1 June 2022. Please send your manuscript to Jane Spurr, the executive editor of the journal, with a copy to Guillermo Badia, the guest editor. The subject line of the e-mail should be "Submission for special issue on JNC of the Logic Journal of the IGPL". The journal submission requirements can be found here.
The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability.
Research in verification has seen a steady convergence of heterogeneous techniques and a synergy between the traditionally distinct areas of testing (and dynamic analysis) and of proving (and static analysis). Formal techniques for counter-example generation based on, for example, symbolic execution, SAT/SMT-solving or model checking, furnish evidence for the potential of a combination of tests and proofs. The combination of predicate abstraction with testing-like techniques based on exhaustive enumeration opens the perspective for novel techniques of proving correctness. On the practical side, testing offers cost-effective debugging techniques of specifications or crucial parts of program proofs (such as invariants). Last but not least, testing is indispensable when it comes to the validation of the underlying assumptions of complex system models involving hardware and/or system environments. Over the years, there is growing acceptance in research communities that testing and proving are complementary rather than mutually exclusive techniques.
The TAP conference aims to promote research in the intersection of testing and proving by bringing together researchers and practitioners from both areas of verification.
List of Topics
TAP's scope encompasses many aspects of verification technology, including
foundational work, tool development, and empirical research. Its topics of
interest center around the connection between proofs (and other static
techniques) and testing (and other dynamic techniques). Papers are solicited
on, but not limited to, the following topics:
Important Dates
More information is available on the conference's web page.
HIGHLIGHTS 2022 aims at integrating the community working in these fields. Papers from these areas are dispersed across many conferences, which makes them difficult to follow. A visit to the Highlights conference should offer a wide picture of the latest research in the field and a chance to meet everybody in the community, not just those who happen to publish in one particular proceedings volume.
We encourage you to attend and present your best work, be it already published or not, at the Highlights conference.
Modalities of Attendance Highlights is an informal event which will take place on-site (barring unforeseen circumstances), and the preferred form of participation is to give your talk in-person. Highlights is mostly intended for a local community of participants who can attend with a limited carbon footprint (e.g., no plane travel). Before coming from further away, please review how your trip and international flights are contributing to climate change. If you do come, we encourage you to make the most of your stay in Paris, e.g., by also attending the ICALP'22 conference and/or using this opportunity for a research visit (see the Highlights website for details). If you cannot attend, you can watch the talks remotely via a video stream, interact via text-based questions and answers, and you can also submit a proposal for a pre-recorded talk. If it is accepted, you will provide a video of your talk, which will be hosted online with other conference videos and be advertised on-site. The selection process will not discriminate between pre-recorded talks and in-person talks.
Scope
Representative areas include, but are not restricted to:
Important Dates
More information is available on the conference's web page.
The purpose of CONCUR 2022 is to bring together researchers, developers, and students in order to advance the theory of concurrency, and promote its applications.
Important note concerning the COVID-19 pandemic
concur 2022 is planned as a physical, in-person event, with certain support for remote presence, both for speakers and for other participants who are unable or unwilling to come. Depending on the pandemic situation, we may have to make a decision whether to cancel the physical component of the event or not. This should be definitely decided by the end of June 2022.
Topics
Submissions are solicited in semantics, logics, verification and analysis of concurrent systems. The principal topics include (but are not limited to):
Important Dates (all dates are AoE)
More information is available on the conference's web page.
Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.
Topics
Dates
More information is available on the conference's web page.
The ICTAC conference series aims at bringing together researchers and practitioners from academia, industry and government to present research and exchange ideas and experience addressing challenges in both theoretical aspects of computing and the exploitation of theory through methods and tools for system development. ICTAC also aims to promote research cooperation between developing and industrial countries.
The conference concerns all aspects of theoretical computer science, including, but not limited to:
Important Dates
More information is available on the colloquium's web page.
Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information.
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 2022 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to
Important Dates
More information is available on the conference's web page.
Inductive reasoning is one of the most important reasoning techniques for humans and formalises the intuitive notion of “reasoning from experience”. It has thus influenced both theoretical work on the formalisation of rational models of thought in Philosophy as well as practical applications in the areas of Artificial Intelligence and, in particular, Machine Learning.
The First International Conference on Foundations, Applications, and Theory of Inductive Logic (FATIL2022) aims at bringing together experts from all fields concerned with inductive reasoning.
Dates and Deadines
More information is available on the conference's web page.
RuleML+RR 2022 aims to bring together rigorous researchers and inventive practitioners, interested in the foundations and applications of rules and reasoning. It provides a forum for stimulating cooperation and cross-fertilization between different communities focused on the research, development, and applications of rule-based systems. We are looking for high-quality papers related to theoretical advances, novel technologies, and artificial intelligence applications that involve rule-based representation and reasoning.
Topics
ruleml+RR welcomes research from all areas of Rules and Reasoning.
The topics of the conference include, but are not limited to:
Important dates
More information is available on the conference's web page.
The aim of GandALF 2022 is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The idea is to cover an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization. Papers focused on formal methods are especially welcome. Authors are invited to submit original research or tool papers on all relevant topics in these areas. Papers discussing new ideas that are at an early stage of development are also welcome. The topics covered by the conference include, but are not limited to, the following:
Important Dates
More information is available on the conference's web page.
The past two decades have witnessed important progress in static analysis and verification of code with low-level pointer and heap manipulations, mainly due to the development of Separation Logic (SL). SL is a resource logic, a dialect of the logic of Bunched Implications (BI) designed to describe models of the heap memory and the mutations that occur in the heap as the result of low-level pointer updates. The success of SL in program analysis is due to the support for local reasoning, namely the ability of describing only the resource(s) being modified, instead of the entire state of the system. This enables the design of compositional analyses that synthesize specifications of the behavior of small parts of the program before combining such local specifications into global verification conditions. Another interesting line of work consists in finding alternatives to the underlying semantic domain of SL, namely heaps with aggregative composition, in order to address other fields in computing, such as self-adapting distributed networks, blockchain and population protocols, social networks or biological systems.
We consider submissions on topics including:
Important Dates
More information is available on the workshop'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.
Aims and Scope
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.
The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to:
Papers on pragmatic aspects of implementing and using SMT tools, as well as novel applications of SMT, are especially encouraged. In addition, to celebrate the 20th edition of the workshop, we challenge the community to submit high-impact work!
Important Dates
More information is available on the workshop's web page.
Starting from Craig's interpolation theorem for first-order logic, the existence and computation of interpolants became an active research area, with applications in different fields, notably in verification, databases, and knowledge representation. There are challenging theoretical and practical questions, for model-theoretic as well as proof-theoretic approaches. The workshop aims at bringing together researchers working on interpolation and its various applications, based on different approaches, increasing the awareness of the automated reasoning community for challenging open problems related to interpolation.
Relevant 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:
Key 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.
PAAR 2022 will host the meeting of the working group on Automated Theorem Provers of the EuroProofNet COST action. Every workshop participant is welcome to attend.
Topics include, but are not limited to:
Important dates
More information is available on the workshop's web page.
The purpose of UNIF 2022 is to bring together researchers interested in unification theory and its applications, as well as closely related topics, such as matching (i.e., one-sided unification), anti-unification (i.e., the dual problem to unification), disunification (i.e., solving equations and inequations) and the admissibility problem (which generalizes unification in modal logics). It is a forum for presenting recent (even unfinished) work, and discuss new ideas and trends in this and related fields.
Unification is concerned with the problem of identifying given (first- or higher-order) terms, either syntactically or modulo a theory. It is a fundamental technique that is employed in various areas of Computer Science and Mathematics. In particular, unification algorithms are key components in completion of term rewriting systems, resolution-based theorem proving, and logic programming. But unification is, for example, also investigated in the context of natural language processing, program analysis, types, modal logics, and in knowledge representation.
Topics of interest of the workshop include, but are not limited to:
Important dates
More information is available on the workshop's web page.
The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilization of ideas from the different communities interested in termination (e.g., working on computational mechanisms, programming languages, software engineering, constraint solving, etc.). The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications.
The 18th International Workshop on Termination welcomes contributions on all aspects of termination. In particular, papers investigating applications of termination (for example in complexity analysis, program analysis and transformation, theorem proving, program correctness, modeling computational systems, etc.) are very welcome.
Topics of interest include (but are not limited to):
Important Dates:
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 the new software generation and to discuss existing systems.
Topics of interest include:
Important Dates
More information is available on the workshop's web page.
The workshop brings together users, contributors, and developers of the Coq proof assistant.
The Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, rather than serving as a venue for traditional research papers, the workshop is organized around informal presentations and discussions, supplemented with invited talks.
Relevant subject matter includes but is not limited to:
Important dates:
More information is available on the workshop's web page.
NMR is the premier forum for results in the area of nonmonotonic reasoning. Its aim is to bring together active researchers in this broad field within knowledge representation and reasoning (KRR), including belief revision, uncertain reasoning, reasoning about actions, planning, logic programming, preferences, deontic reasoning, argumentation, causality, and many other related topics including systems and applications (see NMR page).
As in previous editions, NMR 2022 aims to foster connections between the different subareas of nonmonotonic reasoning and provide a forum for emerging topics. We especially invite papers on systems and applications, as well as position papers and papers addressing benchmark issues. The workshop will be structured by topical sessions fitting to the scopes of accepted papers.
Important Dates
More information is available on the workshop's web page.
Embedded or cyber-physical systems that interact autonomously with the real world, or with users they are supposed to support, must continuously make decisions based on sensor data, user input, knowledge they have acquired during runtime as well as knowledge provided during design-time. To make the behavior of such systems comprehensible, they need to be able to explain their decisions to the user or, after something has gone wrong, to an accident investigator.
While systems that use Machine Learning (ML) to interpret sensor data are very fast and usually quite accurate, their decisions are notoriously hard to explain, though huge efforts are currently being made to overcome this problem. In contrast, decisions made by reasoning about symbolically represented knowledge are in principle easy to explain. For example, if the knowledge is represented in (some fragment of) first-order logic, and a decision is made based on the result of a first-order reasoning process, then one can in principle use a formal proof in an appropriate calculus to explain a positive reasoning result, and a counter-model to explain a negative one. In practice, however, things are not so easy also in the symbolic KR setting. For example, proofs and counter-models may be very large, and thus it may be hard to comprehend why they demonstrate a positive or negative reasoning result, in particular for users that are not experts in logic. Thus, to leverage explainability as an advantage of symbolic KR over ML-based approaches, one needs to ensure that explanations can really be given in a way that is comprehensible to different classes of users (from knowledge engineers to laypersons).
The problem of explaining why a consequence does or does not follow from a given set of axioms has been considered for full first-order theorem proving since at least 40 years, but there usually with mathematicians as users in mind. In knowledge representation and reasoning, efforts in this direction are more recent, and were usually restricted to sub-areas of KR such as AI planning and description logics. The purpose of this workshop is to bring together researchers from different sub-areas of KR and automated deduction that are working on explainability in their respective fields, with the goal of exchanging experiences and approaches.
Topics of Interest
A non-exhaustive list of areas to be covered by the workshop are the following:
Important Dates
More information is available on the workshop's web page.
Sophisticated causal reasoning has long been prevalent in human society and continues to have an undeniable impact on the advancement of science, technology, medicine, and other significant fields. From the development of ancient tools to modern roots of causal analysis in business and industry, reasoning about causality and having the ability to explain causal mechanisms enables us to identify how an outcome of interest came to be and gives insight into how to bring about, or even prevent, similar outcomes in future scenarios.
This workshop aims to bring together researchers and practitioners of logic programming with a dedicated focus on methods and trends emerging from the study of causality and explanation. We welcome the submission of papers on systems, tools, and applications of logic programming methods for causal reasoning and explanation. In particular, we encourage submissions presenting recent developments, including works in progress. The workshop will present the latest research and application developments in these areas and provide opportunities to discuss current and future research directions and relationships to other fields (e.g. Machine Learning, Diagnosis, Natural Language Processing and Understanding, Philosophy of Science). An important expected outcome of this workshop is to collect first-hand feedback from the ICLP community about the role and placement of causal reasoning and explanation in the landscape of modern computer theory as well as in the software industry.
Topics
Topics of interests include (but are not limited to):
Important Dates
More information is available on the workshop's web page.
Probabilistic logic programming (PLP) approaches have received much attention in this century. They address the need to reason about relational domains under uncertainty arising in a variety of application domains, such as bioinformatics, the semantic web, robotics, and many more. Developments in PLP include new languages that combine logic programming with probability theory as well as algorithms that operate over programs in these formalisms.
PLP is part of a wider current interest in probabilistic programming. By promoting probabilities as explicit programming constructs, inference, parameter estimation and learning algorithms can be run over programs that represent highly structured probability spaces. Partly due to logic programming's strong theoretical underpinnings, PLP is fast becoming a very well founded area of probabilistic programming. It builds upon and benefits from the large body of existing work in logic programming, both in semantics and implementation, but also presents new challenges to the field. PLP reasoning often requires the evaluation of a large number of possible states before any answers can be produced thus breaking the sequential search model of traditional logic programs.
While PLP has already contributed a number of formalisms, systems and well understood and established results in: parameter estimation, tabling, marginal probabilities and Bayesian learning, many questions remain open in this exciting, expanding field in the intersection of AI, machine learning and statistics. The workshop encompasses all aspects of combining logic, algorithms, programming and probability. It aims to bring together researchers in all aspects of probabilistic logic programming, including theoretical work, system implementations and applications. Interactions between theoretical and applied minded researchers are encouraged.
Topics of Interest
This workshop provides a forum for the exchange of ideas, presentation of results and preliminary work in all areas related to probabilistic logic programming; including, but not limited to:
Important Dates
More information is available on the workshop's web page.
Dynamic logic (DL), a generalisation of the logic of Floyd-Hoare introduced in the 70s by Pratt, is a well-known and particularly powerful way of combining propositions, for capturing static properties of program states, and structured actions, responsible for transitions from a state to another (and typically combined through a Kleene algebra to express sequential, non-deterministic, iterative behaviour of systems), into a formal framework to reason about, and verify, classic imperative programs.
Over time Dynamic logic grew to encompass a family of logics increasingly popular in the verification of computational systems, and able to evolve and adapt to new, and complex validation challenges. In particular, the dynamic logic community is interested in the study of operators that can modify the structure in which they are being evaluated. Examples include dynamic logics tailored to specific programming problems or paradigms (e.g., separation logics to model the evolution of a program heap); languages to reason and represent evolving information (e.g., dynamic epistemic logics); and formalism that aim to model new computing domains, including probabilistic, continuous and quantum computation.
Dynamic logic is not only theoretically relevant, but it also shows enormous practical potential and it is indeed a topic of interest in several scientific venues, from wide-scope software engineering conferences to modal logic specific events. That being said, DaLí is the only event exclusively dedicated to this topic. It is our aim to once again bring together in a single place the heterogeneous community of colleagues which share an interest in Dynamic logic - from Academia to Industry, from Mathematics to Computer Science, - to promote their works, to foster great discussions and new collaborations.
List of Topics
Submissions are invited on the general field of dynamic logic, its variants
and applications, including, but not restricted to:
Important Dates
More information is available on the workshop's web page.
Linearity has been a key feature in several lines of research in both theoretical and practical approaches to computer science. On the theoretical side there is much work stemming from linear logic dealing with proof technology, complexity classes, and more recently quantum computation. On the practical side, there is work on program analysis, expressive operational semantics for programming languages, linear programming languages, program transformation, update analysis and efficient implementation techniques.
Linear logic is not only a theoretical tool to analyse the use of resources in logic and computation. It is also a corpus of tools, approaches, and methodologies (proof nets, exponential decomposition, geometry of interaction, coherent spaces, relational models, etc.) that were originally developed for the study of linear logic's syntax and semantics and are nowadays applied in several other fields.
The aim of this Joint Linearity and TLLA workshop is to bring together researchers who are currently working on linear logic and related fields, to foster their interaction and provide a forum for presenting new ideas and work in progress. We also hope to enable newcomers to learn about current activities in this area. New results that make central use of linearity, ranging from foundational work to applications in any field, 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:
Important Dates
More information is available on the workshop's web page.
Several successful logic programming languages, evidenced by the availability of a multitude of solvers, industrial applications, and an active research community, have been proposed in the literature. Researchers have long recognized the need for epistemic operators in these languages. This led to a flurry of research on this topic, and renewed interest in recent years. A central question is that of the definition of a rigorous and intuitive semantics for such epistemic operators, which is still subject of ongoing research. Notions of equivalence, structural properties, and the inter-relationships between logic programming languages and established logics are all subjects being actively investigated. Another important topic is that of practical solvers to compute answers to logic programs that contain epistemic operators. Several solvers are actively developed, building on established solvers, or using rewriting-based approaches. For practical applications, additional language features are actively explored in order to be able to apply epistemic extensions of logic programming langauges to practical problems. The goal of this workshop is to facilitate discussions regarding these topics and a productive exchange of ideas.
Topics of interests include (but are not limited to):
Important Dates
More information is available on the workshop's web page.
Since its introduction in the late 1980s, Answer Set Programming (ASP) has been widely applied to various knowledge-intensive tasks and combinatorial search problems. ASP was found to be closely related to SAT, which led to a new method of computing answer sets using SAT solvers and techniques adapted from SAT. This has been a much studied relationship, and is currently extended towards satisfiability modulo theories (SMT). The relationship of ASP to other computing paradigms, such as constraint satisfaction, quantified Boolean formulas (QBF), Constraint Logic Programming (CLP), first-order logic (FOL), and FO(ID) is also the subject of active research. Consequently, new methods of computing answer sets are being developed based on relationships to these formalisms.
Furthermore, the practical applications of ASP also foster work on multi-paradigm problem-solving, and in particular language and solver integration. The most prominent examples in this area currently are the integration of ASP with description logics (in the realm of the Semantic Web) and constraint satisfaction (which recently led to the Constraint Answer Set Programming (CASP) research direction).
A large body of general results regarding ASP is available and several efficient ASP solvers have been implemented. However, there are still significant challenges in applying ASP to real life applications, and more interest in relating ASP to other computing paradigms is emerging. This workshop will provide opportunities for researchers to identify these challenges and to exchange ideas for overcoming them.
Topics of interests include (but are not limited to):
Important Dates
More information is available on the workshop's web page.
LFMTP 2022 will hold a special session in honour of Frank Pfenning's 60th birthday: one more reason to contribute & participate!
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 2022 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
The workshop's program will include contributed and invited talks. We hope that LFMTP takes place physically in Haifa, but online participation will be possible and may even be necessary.
LMFTP 2022 will host a special session celebrating Frank Pfenning's contributions in the occasion of his 60th Birthday (belated). We therefore encourage and invite contributions that build or reflect on Frank's broad range of contributions.
Important Dates
More information is available on the workshop's web page.
The DL workshop is the major annual event of the description logic research community. It is the forum in which those interested in description logics, both from academia and industry, meet to discuss ideas, share information and compare experiences.
Workshop Scope
We invite contributions on all aspects of description logics,
including, but not limited to:
Important Dates
More information is available on the workshop's web page.
The 18th Doctoral Consortium (DC) on Logic Programming provides students with the opportunity to present and discuss their research directions, and to obtain feedback from both peers and experts in the field.
Audience
The DC is designed for students currently enrolled in a Ph.D. program, though we are also open to exceptions (e.g., students currently in a Master's program and interested in doctoral studies). Students at any stage in their doctoral studies are encouraged to apply for participation in the DC. Applicants are expected to conduct research in areas related to logic and constraint programming; topics of interest include (but are not limited to):
Submissions by students who have presented their work at previous ICLP DC editions are allowed, but should occur only if there are substantial changes or improvements to the student's work. The DC offers participants a convenient, more informal way to interact with established researchers and fellow students, through presentations, question-answer sessions, panel discussions, and invited presentations. The Doctoral Consortium will also provide the possibility to reflect - through short activities, information sessions, and discussions - on the process and lessons of research and life in academia. Each participant will give a short, critiqued, research presentation.
Discussants
Renowned experts and researchers in the fields of logic and constraint programming will join in evaluating submissions and will participate in the DC, providing valuable feedback to DC participants.
Goals
Important Dates
DC students are highly recommended to attend the School on Logic Programming and Constraint Programming.
More information is available on the doctoral consortium's web page.
Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory.
The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. As part of the workshop there will be an introductory tutorial intended to make the invited and contributed talks accessible to non-experts.
Important Dates
More information is available on the workshop's web page.
Graphs and graph transformation systems are used in many areas within Computer Science: to represent data structures and algorithms, to define computation models, as a general modeling tool to study complex systems, etc.
Topics of interest for TERMGRAPH encompass all aspects of term-/graph rewriting (term-graph and graph rewriting), and applications of graph transformations in programming, automated reasoning and symbolic computation, including:
The aim of this workshop is to bring together researchers working in these different domains, to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area.
Important Dates:
More information is available on the workshop's web page.
Machine Ethics, Explainability are two recent topics that have been attracting a lot of attention and concern in the last years. This global concern has manifested in many initiatives at different levels. There is an intrinsic relation between these two topics. It is not enough for an autonomous agent to behave ethically, it should also be able to explain its behavior, i.e. there is a need for both ethical component and explanation component. Furthermore, an explainable behavior is obviously not acceptable if it is not ethical (i.e., does not follow the ethical norms of the society).
In many application domains especially when human lives are involved (and ethical decisions must be made), users need to understand well the system recommendations, so as to be able to explain the reasons for their decisions to other people.One of the most important ultimate goals of explainable AI systems is the efficient mapping between explainability and causality. Explainability is the system ability to explain itself in natural language to average user by being able to say, "I generated this output because x,y,z". In other words, the ability of the system to state the causes behind its decision is central for explainability.
However, when critical systems (ethical decisions) are concerned, is it enough to explain system's decisions to the human user? Do we need to go beyond the boundaries of the predictive model to be able to observe a cause and effect within the system?
There exists a big corpus of research work on explainability, trying to explain the output of some blackbox model following different approaches. Some of them try to generate logical rules as explanations. However, It is worth noting that most methods for generating post-hoc explanations are themselves based on statistical tools, that are subject to uncertainty or errors. Many of the post-hoc explainability techniques try to approximate deep-learning black-box models with simpler interpretable models that can be inspected to explain the black-box models. However, these approximate models are not provably loyal with respect to the original model, as there are always trade-offs between explainability and fidelity.
On the other side, a good corpus of researchers have used inherently interpretable approaches to design and implement their ethical autonomous agents. Most of them are based on logic programming, from deontic logics to non-monotonic logics and other formalisms.
Logic Programming has a great potential in these two emerging areas of research, as logic rules are easily comprehensible by humans, and favors causality which is crucial for ethical decision making .
Anyway, in spite of the significant amount of interest that machine ethics has received over the last decade mainly from ethicists and artificial intelligence experts, the question "are artificial moral agents possible?" is still roaming around.There have been several attempts for implementing ethical decision making into intelligent autonomous agents using different approaches. But, so far, no fully descriptive and widely acceptable model of moral judgment and decision making exists. None of the developed solutions seem to be fully convincing to provide a trusted moral behavior. The same goes for explainability, in spite of the global concern about the explainability of the autonomous agents' behaviour, existing approaches do not seem to be satisfactory enough. There are many questions that remain open in these two exciting, expanding fields.
This workshop aims to bring together researchers working in all aspects of machine ethics and explainability, including theoretical work, system implementations, and applications. The co-location of this workshop with ICLP is intended also to encourage more collaboration with researchers from different fields of logic programming.This workshop provides a forum to facilitate discussions regarding these topics and a productive exchange of ideas.
Topics of interest include (but not limited to):
Important Dates
More information is available on the workshop's web page.
Answer set programming is a successful extension of logic programming for solving combinatorial problems as well as knowledge representation and reasoning problems. Most current implementations of ASP work by grounding a program and using a SAT solver-like technology to find the answer sets. While this approach is extremely efficient, relying on grounding of the program leads to significant blow-up of the program size, and computing the whole model makes finding justification of an atom in the model hard. This limits the applicability of ASP to problems dealing with large knowledge bases. Goal-directed or query-driven execution strategies have been proposed that do not require grounding. The goal of this workshop is to foster discussion around challenges and opportunities that such approaches present.
Tentative list of topics include:
Important Dates:
More information is available on the workshop's web page.
The aim of LANMR is to bring together researchers interested in methods of reasoning and applications involving logic broadly understood from philosophy to programming languages and artificial intelligence. We invite authors to submit papers to this forum, presenting original and unpublished research on all pertinent subjects, including but not limited to the following
Important Dates
More information is available on the workshop's web page.
The aim of the FMICS conference series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.
FMICS is the ERCIM Working Group conference on Formal Methods for Industrial Critical Systems. FMICS is the key conference in the intersection of industrial applications and Formal Methods. This year's conference is the 27th in the series. FMICS will be held as part of CONFEST 2022.
Topics of interest include (but are not limited to):
Important Dates
More information is available on the workshop's web page.
The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as a formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends. In 2020 WADT features additionally two special thematic tracks: one in *Algebra for timed and hybrid systems* and another in *Algebraic approaches to quantum computation*.
Main track Typical, but not exclusive topics of interest for the main track are:
Algebra for timed and hybrid systems
The track 'Algebra for timed and hybrid systems' seeks algebraic contributions towards a better understanding of timed and hybrid systems, including their design and verification. A non-exhaustive list of topics includes:
Algebraic approaches to quantum computation
This track seeks contributions on algebraic methods in the context of quantum computing, broadly understood, ranging from foundations to applications and tools. A non-exhaustive list of topics includes:
Important dates
More information is available on the workshop's web page.
Learning models defining recursive computations, like automata and formal grammars, are the core of the field called Grammatical Inference (GI). The expressive power of these models and the complexity of the associated computational problems are major research topics within mathematical logic and computer science. Historically, there has been little interaction between the GI and ICALP communities, though recently some important results started to bridge the gap between both worlds, including applications of learning to formal verification and model checking, and (co-)algebraic formulations of automata and grammar learning algorithms.
The goal of this workshop is to bring together experts on logic who could benefit from grammatical inference tools, and researchers in grammatical inference who could find in logic and verification new fruitful applications for their methods.
Topics of interest include (but are not limited to):
More information is available on the workshop's web page.
Interaction and Concurrency Experience (ICE) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools, and programming primitives for complex interactions.
Scope
The general scope of the venue includes theoretical and applied
aspects of interactions and the synchronization mechanisms used among
components of concurrent/distributed systems, related to several areas
of computer science in the broad spectrum ranging from formal
specification and analysis to studies inspired by emerging
computational models.
We solicit contributions relevant to Interaction and Concurrency, including but not limited to:
Important Dates
More information is available on the workshop's web page.
Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and computational languages, supporting tool development and reasoning. The LSFA series' objective is to put together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side.
LSFA topics of interest include, but are not limited to:
Important dates
More information is available on the workshop's web page.
WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers.
Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are:
Important Dates
More information is available on the workshop's web page.
The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models.
Topics of interest for EXPRESS/SOS 2022 include, but are not limited to:
We especially welcome contributions bridging the gap between the above topics and neighbouring areas, such as, for instance:
Important Dates
More information is available on the workshop's web page.
QBFEVAL'22 is the 2022 competitive evaluation of QBF solvers, and the fifteenth event aimed to assess the performance of QBF solvers. QBFEVAL'22 awards solvers that stand out as being particularly effective on specific categories of QBF instances.
We warmly encourage developers of QBF solvers to submit their work, even at early stages of development, as long as it fulfills some very simple requirements. We also welcome the submission of QBF formulas to be used for the evaluation. Researchers thinking about using QBF-based techniques in their area (e.g., formal verification, planning, knowledge representation & reasoning) are invited to contribute to the evaluation by submitting QBF instances of their research problems (see the requirements for instances). The results of the evaluation will be a good indicator of the current feasibility of QBF-based approaches and a stimulus for people working on QBF solvers to further enhance their tools.
For questions, comments and any other issue regarding QBFEVAL'22, please get in touch with the organizers.
Important Dates
Details about solvers and benchmarks submission, tracks, and related rules, are available on the competition's web page.
The competition will offer a number of challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness, and elegance.
Participation Participation is open for anybody interested. Teams of up to two people are allowed. Registration for ETAPS workshops (deadline: March 26) and physical presence on site is required.
We particularly encourage participation of:
More information is available on the conference's web page.
Term Rewriting is a simple but powerful model of computation with numerous applications in computer science and mathematics. It is heavily used in symbolic computation, formal reasoning, and program verification. Rewriting-based techniques are useful in many other fields as well, for instance, in quantum computing, biology, music...
The 13th International School on Rewriting (ISR 2022) will take place at Ivane Javakhishvili Tbilisi State University, Tbilisi, Georgia. The school is aimed at students, researchers and practitioners interested in the use or the study of rewriting and its applications and offers two parallel tracks:
Registration
Registration will open in May.
The registration fee is 200/250 Euro (early till July 15/late till August 31), which will include access to school materials, coffee breaks, and social events (excursion and banquet). The registration fee for an accompanying person is 50/100 Euro (early/late) and included only social events.
Participants affiliated with Ukrainian universities will have the registration fee waived. Further support will be announced if funds get available.
More information is available on the school's web page.
MGS is an annual spring school that offers an intensive programme of lectures on the mathematical foundations of computing. While the school addresses especially PhD students in their first or second year, it is also open to UG and MSc students, postdocs, participants from the industry, and generally everyone interested in its topics. MGS'22 is the school's 22nd incarnation.
Programme
MGS'22 offers eight courses:
The registration period closes as soon as all places are filled or on March 21, whichever is sooner.
More information is available on the school's web page.
The school will cover a diverse range of topics around foundational database theory and the use of knowledge (constraints, ontologies) in data management, with a special focus on inconsistent, incomplete and more generally "imperfect" data.
We invite students, postdocs, and other researchers interested in learning about the foundational aspects of databases and handling imperfect data to participate in the summer school.
Program
The summer school will feature 11 tutorials from internationally renowned researchers:
Important Dates
Application and registration details can be found on the school's web page.
The International Artificial Intelligence in Bergen Research School aims at disseminating recent advances on AI. In this edition (AIB 22), the broad theme of the school is Knowledge Graphs and Machine Learning. The research school is aimed at master and PhD students, postdocs, and researchers who wish to learn more about the theme. The event will be co-located with a workshop where participants will have the opportunity to present their work in oral and poster sessions. A social program is also included to foster interaction between the admitted participants.
Confirmed Lectures
Registration
The registration is already open, and it is free of charge.
More information is available on the school's web page.
MOVEP is a five-day summer school on modelling and verification of infinite state systems. It aims to bring together researchers and students working in the fields of control and verification of concurrent and reactive systems.
MOVEP 2022 will consist of ten invited tutorials. In addition, there will be special sessions that allow PhD students to present their on-going research (each talk will last around 20 minutes). Extended abstracts (1-2 pages) of these presentations will be published in informal proceedings.
The organisation committee is closely monitoring the COVID situation. Currently, we are planning for an in-person school in Aalborg with the possibility for remote participation for those that cannot attend in person. Should it become necessary, the school will be held virtually.
Speakers
Student Session
We encourage participants to present their (ongoing or published) work. Talks will last around 20 minutes.
Important Dates
More information is available on the school's web page.
There are currently several open positions, at the Master's, PhD, and postdoc level, at the LaBRI computer science lab, located in Bordeaux, France.
These positions are funded by the INTENDED project, whose aim is to develop principled methods for handling imperfect data. The project brings together experts on knowledge representation and reasoning, database theory, and medical informatics to explore how to exploit formally represented knowledge (constraints, ontologies) and logical reasoning to holistically tackle a range of data quality issues.
Detailed job postings and information on how to apply can be found on our website.
Excellent candidates with experience and interest in knowledge representation and reasoning, databases, and/or logic in CS are encouraged to get in touch.
Project opportunity This Earmarked Scholarship project is aligned with a recently awarded Category 1 research grant. It offers you the opportunity to work with leading researchers and contribute to large projects of national significance.
Data available for collection in the real world is very often not a matter of yes or no, not a matter of all or nothing, but actually a matter of degrees. There is a growing need to represent this information in graded databases. Moreover, real-world data usually involves only finitely-many objects. Mathematical logic offers precise syntactic tools via logical languages that allow for expressing and querying information, which has already proved its power in the case of finite databases with binary yes-or-no properties with the deep development of classical finite model theory. On another research stream, mathematical fuzzy logic has developed a wealth of results about logical tools for general (possibly infinite) graded structures. However, graded finite structures pose specific difficulties that do not allow a straightforward application of general results. In this project, we want to fill this obvious theoretical gap by putting forward a mathematically ambitious study of graded finite structures, which may turn out to be crucial for a wider applicability of mathematical logic.
Scholarship value
As a scholarship recipient, you'll receive:
Supervisor
Dr Guillermo Badia, School of Historical and Philosophical Inquiry
Preferred educational background
Your application will be assessed on a competitive basis.
We take into account your
Latest commencement date
If you are the successful candidate, you must commence by Research Quarter 3, 2023. You should apply at least 3 months prior to the research quarter commencement date.
If you are an international applicant, you may need to apply much earlier for visa requirements.
How to apply
You apply for this project as part of your PhD program application.
Freek Wiedijk and colleagues are looking for a PhD student with a master in mathematics or equivalent, who wants to write his/her/their PhD thesis on formalization of mathematics. In particular this is about a formalization project related to Fermat's Last Theorem. See this webpage for more details about the position.
If you are interested, or know someone who might be interested, they would very much like to hear from you.
Postdoctoral Research Position
College overview
The Australian National University (ANU) College of Engineering and Computer Science (CECS) is a vibrant and diverse community of more than three thousand students, staff, and visitors. Our College is comprised of three schools: the School of Computing, School of Cybernetics, and School of Engineering, supported by the Professional Services Group. We aim to bring together expertise in social, technical, ecological and scientific systems to build a new approach. In the College, we draw on our disciplinary foundations to find and solve problems of global importance. Our people build on our traditional world-class expertise and take it in creative, unconventional directions. Through the Reimagine investment, we have the privilege and the responsibility to build a new legacy for the University, the country, and even the world. We will deliver on our mission by building a strong community, providing transformative educational experiences, conducting high-impact research, seeking meaningful engagement, and becoming a resilient organisation post COVID-19. Join us in shaping a new intellectual agenda to reimagine engineering, computing, and the use of technology in the world.
The School of Computing in collaboration with the Defence Science and Technology Group (DST) and the Australian Signal Directorate (ASD) is a leading centre in formal modelling, analysis and verification of safety-critical systems, aiming at trustworthy and resilient systems. The school brings together the best and brightest researchers, scholars and fostering a vibrant culture of enabling technologies for the 21st century.
Position overview
The Research Fellow will develop foundations and tools for specifying and verifying software, with a particular emphasis on applications in the areas of concurrency, programming languages, and security. Foundations should be based on sound mathematical frameworks, e.g., process algebra or operational semantics. Tool support can range from frameworks within interactive proof assistants via the use of off-the-shelf model checkers to code generation. The Postdoctoral Fellow should apply the developed theory to real-world case studies, such as compiler verification, or the analysis of protocols in terms of correctness or security. The successful candidate is encouraged to develop new and innovative research directions in their specified scientific impact domain, including relevant collaborations.
The opening is a research-focused position. However, the Research Fellow may undertake work in all three areas of academic activity—research, education, and service (including outreach). The allocation of time to each area will be discussed with the position supervisor. The Research Fellow may also be required to supervise or assist in the supervision of students and contribute cooperatively to the overall intellectual life of the School, College and University.
The Research Fellow will be a member of the School of Computing, accountable to their direct supervisor and the Director of the School. The Research Fellow will be expected to work collegially, leading by example to develop and maintain effective, productive, and beneficial workplace relationships with all academic and professional School and College staff, students and honorary appointees, as well as with industry stakeholders. This position will also have a mentoring role for students and will engage in collegial and productive collaborations with local, national, and where possible, international colleagues.
ANU values diversity and inclusion and believes employment opportunities must not be limited by socio-economic background, race, religion or gender. The University actively encourages applications from women, Aboriginal and Torres Strait Islander people and candidates from culturally and linguistically diverse backgrounds. Furthermore, it is policy in the ANU College of Engineering and Computer Science to require selection panels to seek a gender balance when compiling shortlists of candidates for interview. For more information about staff equity at ANU, visit services.anu.edu.au/human-resources/respect-inclusion.
The ANU provides attractive benefits and excellent support to maintain a healthy work/life balance and offers generous remuneration benefits, including four weeks paid vacation per year, assistance with relocation expenses and 17% employer contribution to superannuation. This also includes generous parental leave, the possibility of flexible and part time working arrangements, a parental and aged care support program, dual career hire programs, ANU school holiday programs, and childcare facilities on campus. For more information, please visit this web page.
Application information
Applicants must apply online via the ANU recruitment portal and should upload the following separate documents:
Closing date Review of your application is guaranteed if your application is received by 31 January 2022. The search will continue until the positions are filled, or until 30 June 2022, whichever comes first.
The project aims at the construction of formally verified secure IoT systems that follow the concept of “zero trust architecture”, dubbed ZT-IoT systems. It consists of four research teams and two teams, led by Atsushi Igarashi, Kyoto University, Japan and Taro Sekiyama, National Institute of Informatics, Japan (NII) are investigating applications of formal verification or programming language techniques to the construction of secure IoT systems.
The main research topic of Igarashi’s team is centered around the design and theory of security policy engines for ZT-IoT systems, inclucing the design of a language to describe security policies and policy enforcement algorithms and the techniques for verifying policy enforcement algorithms against given security policies. Other team members are Kohei Suenaga and Masaki Waga at Kyoto University.
The main research topic of Sekiyama’s team is centered around techniques for monitoring and intervention for ZT-IoT systems. Other team members include Ichiro Hasuo and Shin-ya Katsumata at NII.
Although the two teams are based in different places, we collaborate closely with each other.
The appointment can start as early as April 2022 (the starting date is negotiable). The contract will initially run until the end of March 2023, with the possibility of annual renewal until the end of the project, which is March 2027 at maximum. Salary will be about 360,000–550,000 JPY/month.
Applicants should have a Ph.D in computer science or related fields, and have a strong background in formal verification and/or programming language theory. Due to the project’s nature, they are required to have strong interests in applying theory to practice; they should also be (self-)motivated, dedicated, and able to work both independently and collaboratively. Strong communication skills in oral and written English are required.
Workplace
Members of Igarashi’s team will work at Kyoto University, Kyoto, Japan and members of Sekiyama’s team will work at NII, Tokyo, Japan.
(Living costs in Japan are not very high nowadays. An estimate is found here and we find rent can be cheaper than the cited amount.)
Applications and inquiries
Inquiries can be sent by email, with the subject CREST Job Inquiry. Feel free to ask us any questions on relevance, topics, compensation, etc. We will reply when we see enough relevance.
Applications should be made electronically via the following JREC-IN Portal web sites.
Please upload a pdf including
You will be contacted for further material and interview, provided that your application is found sufficiently relevant. Starting dates are negotiable. The positions will remain open until filled.
Liam O'Connor has a funded PhD studentship available (at LFCS, Uni of Edinburgh) to anyone with a good proposal related to PL/FM. In particular I'm hoping to work with someone on my Quickstrom project (a property-based testing tool based on Linear Temporal Logic). More details here.
The Software Safety and Security Lab at CEA LIST, Université Paris-Saclay, France has 2 open postdoc positions in the area of runtime verification for code safety and security: - Designing Compilation Techniques for Improving Efficiency of E-ACSL, a Runtime Assertion Checker for C Programs (see here), - Control Flow Integrity for Remote Attestation (see here).
The postdoc researchers will:
Strong knowledge in at least one of the following areas is welcome:
Interested applicants should send a CV and a motivation letter to Julien Signoles.
Researcher positions (postdoc/phd) within the ERC Consolidator grant “Certified Quantum Security”
[Below is the description of postdoc positions. Phd positions are similar and can be found here.]
[This call can also be found here.]
As part of the ERC Consolidator Grant "Certified Quantum Security" and the US Airforce project "Verification of Quantum Cryptography", we are looking for postdocs to work on verification of quantum cryptography (or more generally on quantum cryptography).
We will develop methods for the verification of proofs in quantum cryptography. Similar to what the EasyCrypt tool does in classical cryptography. The scope of the project covers everything from the logical foundations, through the development of tools, to the verification of real quantum protocols.
The ideal candidate would have experience in:
Of course, expertise in all those areas is very rare, so candidates who are strong in some of those areas and are interested in the others are encouraged to apply!
Please contact Dominique Unruh if you have more questions about the project, the required background, Estonia, the position itself, or the application process. I can also provide a detailed description of the overall research project.
The salary range is 30000-36000 Euro per year (depending on experience), which is highly competitive in Estonia due to low costs of living and low income tax rate (20%). Pension contributions and health insurance are covered by the employer.
Applications are accepted at any time (until all positions are filled), and positions can start as soon as possible. Positions are typically for 2-3 years (up to negotiation).
To apply, please send the following documents to Dominique Unruh:
Ana Ozaki and colleagues invite highly motivated applicants interested in carrying out foundational and/or applied research in knowledge representation, ontologies, and machine learning. The starting date is flexible (from March to September 2022).
The Ph.D. positions are fully funded for 3 years and can be extended by one more year through 25% of teaching activities during the Ph.D. studies. Additional funding is available for travel.
Bergen (The capital of the fjords!): see here.
The annual meeting of Ph.D. students: see here.
Department of Informatics: see here.
For more information, contact Ana Ozaki.
Institution: Cryptography and Blockchain Lab, University of Warsaw, Poland
We are looking for a post-doc/senior researcher in an Advanced Grant “PROCONTRA” funded by the European Research Council (ERC) and led by Stefan Dziembowski. The task of the successful candidate will be to substantially contribute to our efforts of formally verifying cryptographic protocols that interact with smart contracts deployed on blockchains. Examples of such protocols include “state channels,” “Plasma,” or “rollups” (see, e.g., the publications of Stefan Dziembowski for more on such protocols).
We are currently focusing on applying proof assistants and automated provers (such as Coq, Easycrypt, Why3) to achieve this goal. We aim to formalize cryptography using the Universal Composability framework. Still, a successful candidate will be given substantial academic freedom and can work on various research problems related to the project’s central theme. We require good background on formal verification, documented by publications. Knowledge of cryptography is a plus but is not required.
We offer an internationally competitive salary, a substantial budget for travel and equipment, and membership in a young and vibrant team with several international contacts. The funding is available until the end of 2025, and the position can last until then (this is subject to negotiations).
For more information, please get in touch by email with the project leader, Stefan Dziembowski.
The project aims at advancing theoretical foundations at the borderline between automata theory, concurrency and verification. We promise, except for very competitive salary, a vibrant working atmosphere in the automata group at the University of Warsaw, and exciting and challenging research problems.
The ideal candidate is expected to have:
We offer a fully-funded PhD position within the NCN grant "Frontiers of automatic analysis of concurrent systems". The project aims at advancing theoretical foundations at the borderline between automata theory, concurrency and verification, but anticipates also development of prototype analysis tools. A successful candidate is expected to enroll into the PhD program in the University of Warsaw.
We offer:
The successful candidate is expected to have: Master’s degree or equivalent in computer science or math solid background in formal methods and automata theory strong motivation for research work in foundations of computer science advanced skills in written and spoken English.
A postdoc/junior researcher position is available to join the Logic Group at the ICS, for the project "Metamathematics of substructural modal logics".
We are looking for a researcher ready to conduct unsupervised research in close collaboration with members of the project team and the Logic group, within the area of the project.
Applications will be reviewed on a rolling basis with a first cut-off point on 20. 3. 2022.
Starting date: July 1, 2022 or upon agreement.
Duration: 18–30 months (with the possibility of follow-up tenure-track application).
More details can be found here.
Amazon has a growing number of automated reasoning scientists working on various exciting projects. The most prominent being in the direction of provable security. A lot of information can be found on the associated web page, which also links to academic papers.
Each year, Amazon open their doors to current MSc and PhD students to undertake an Applied Science Internship, working within an Amazon team to help develop automated reasoning solutions to business problems. Internships are compensated (very well by academic standards, in my opinion) and typically last 14 weeks. They can be taken at any point during the year (in agreement with the hosting team).
This is an excellent opportunity to get a taste of what automated reasoning science looks like in industry. There is a broad and growing range of automated reasoning specialisms being deployed within AWS and an even faster growing set of business problems be tackled by automated reasoning techniques. Byron Cook recently opined that automated reasoning is entering a golden era as a research area – come and see if he’s right!
Interested applicants are encouraged to reach out to an existing member of Amazon’s Automated Reasoning Group (e.g. Giles Reger) before applying. There is one link for PhD students and one link for MSc students wishing to apply.
Please do forward this opportunity to MSc or PhD students working in automated reasoning – there are many internship positions available.
Two PhD projects are proposed by the LILaC research group at IRIT, at the University of Toulouse, France:
The selection of applicants will be in two steps: first at department level (April), then an interview at the doctoral school level (May). For more information and for applications please write to the contact persons of the relevant project.
The Knowledge Representation and Reasoning (KRR) group at the Institute of Software Technology, Graz University of Technology, offers two funded PhD student positions in the field of Computational Argumentation within Artificial Intelligence.
Central aims of Computational Argumentation are to investigate representations of arguments, study their relationships, and perform automated argumentative reasoning, with application domains, e.g., in medical or legal reasoning, and eXplainable Artificial Intelligence (XAI).
With the PhD projects, we will advance the state of the art of foundational research on the complex reasoning process underlying argumentation. You will work on tasks ranging from deep theoretical understanding, such as complexity analysis, to algorithmic solutions for challenging reasoning problems.
We are looking for motivated and talented applicants with very good university degrees (MSc or equivalent) in Computer Science or Mathematics (or comparable fields), and with solid background in one or more of:
The positions are funded by the Austrian Science Fund (FWF), full-time, and fixed-term for three years. The contracts will be under the collective agreement for university employees at TU Graz. Candidates should be independent in organising their work, keen on working with teams of experts of project partners, and fluent in English, oral and written. Starting time can be as soon as possible, but some degree of flexibility is possible.
An inclusive environment and balancing family and career are important aspects to the group and university. We encourage women to apply.
Applications with
Additional information
Announcement for two 11-15-month postdoctoral positions funded by the ANR LambdaComb.
Project summary : LambdaComb is an interdisciplinary project financed by the French Agence Nationale de la Recherche. Broadly, the project aims to deepen connections between lambda calculus and logic on the one hand and combinatorics on the other. One important motivation for the project is the discovery over recent years of a host of surprising links between subsystems of lambda calculus and enumeration of graphs on surfaces, or "maps", the latter being an active subfield of combinatorics with roots in W. T. Tutte's work in the 1960s. More informations can be found on the project webpage.
We seek candidates holding or soon to receive a PhD in Computer Science or Mathematics and with expertise in one or several of the following areas:
The ideal candidate will have a strong background in one of the areas and at least an interest in the others.
We aim to recruit two postdocs who will be employed respectively at:
Both postdocs will have opportunities for visiting other partner institutions and for collaborating with other members of the project (see full list at the project page linked above).
Application process:
Context: The ANR project ICSPA aims at improving confidence in the proofs built in the context of B/Event-B and TLA+ by adding formal proofs to these systems and independently verifying these proofs with the Logical Framework Dedukti.
Job assignments: The post-doctoral researcher will
Applications must include a CV, a complete list of publications and a reference letter.
Nicolai Kraus would like to invite applications for one postdoctoral position and one PhD position in homotopy type theory or related areas at the University of Nottingham, UK. His group in Nottingham has three academics (Ulrik Buchholtz, Thorsten Altenkirch, Nicolai Kraus) and multiple PhD students working in the field. They have regular seminars and discussions, which offer a great environment to learn and collaborate.
(1) Postdoc position
The starting date for the postdoc position is flexible and it will initially be for 15 months (i.e. 15 months are guaranteed, extensions are likely but will depend on the funder). The position comes without teaching obligations.
The current call primarily addresses applicants who have experience in homotopy type theory, but if you are working in a related area and would be interested to switch to the field, please feel free to contact Nicolai Kraus.
As postdoc (officially: "research fellow"), you will be employed by the University of Nottingham with all employment benefits (pension etc). Details on the position are available here.
The application deadline is the 3rd of April. For any questions or expressions of interest, feel free to contact Nicolai Kraus.
(2) PhD position
The PhD position is for four years, includes all tuition fees, and comes with a stipend at the UKRI standard (currently approx. £15600 annually, increases with inflation). The stipend is free from tax or other deductions. You will not be obliged to teach but there will be opportunities to teach, paid on top of the stipend. I will consider applications until the position is filled. If you are interested, please contact Nicolai Kraus.
The Department of Mathematics of Vrije Universiteit Amsterdam welcomes applications for a fully-funded, 4-year PhD position in Number Theory and Formalization.
The preferred starting date is in the period 1 May - 1 September 2022.
The candidate will conduct research on Sander Dahmen's NWO-funded project "Formalizing Diophantine algorithms". This amounts to both developing and formalizing (with a proof assistant such as Lean or Coq) number theory necessary for solving Diophantine problems. The focus will be on effective/algorithmic number theory, but more "pure" results will (necessarily) also play an important role. We note that in this project most of the time will likely be spent on actual formalization work and that the proof assistant to be used will probably be Lean (but that is open for discussion). The position also contains a small teaching component.
The research will be embedded in the Algebra and Number Theory group of the Mathematics Department and in particular connects to the CAN-endowed chair "Automated verification of mathematical proof" held by Assia Mahboubi. Within the Faculty of Science there will also be close collaboration with (Theoretical) Computer Science, especially the group of Jasmin Blanchette.
Applications from all groups currently under-represented in academic posts are particularly encouraged. We are working to improve the present gender balance within the department, and particularly welcome applications from women.
More details here.
Telecom Paris, one of the top French Graduate Schools of Engineering, offers a full-time tenured academic position as Associate Professor in the area of Artificial Intelligence, with a focus on knowledge, AI, and NLP.
The candidate will join the DIG team (Data, Intelligence, Graphs), starting September 2022.
The candidate is expected to have strong skills in at least one of the following fields:
Online application: here.
Deadline for application: March 28, 2022.
At the Institute for Logic, Language and Computation (part of the University of Amsterdam) there is a vacancy for a PhD student within our Mathematical and Computational Logic group. The advert can be found here.
Deadline is March 31.
Interested candidates should feel free to contact Benno van den Berg.
Stephan Merz and Sophie Tourret are seeking applicants for a PhD position on automated reasoning for the B method, a formal development method based on set theory.
The B method is a formalism based on set theory that targets the development of software systems used in critical applications, subject to stringent certification requirements. It defines proof obligations that ensure the preservation of invariants or the correctness of refinements between models described at different levels of abstraction, and these proof obligations must be discharged for a model to be accepted as valid.
The application of the B method is supported by Atelier B, maintained by the Clearsy company, a platform that contains several engines for automatic proof. In a recent experiment, among the roughly 77,000 proof obligations of a representative industrial development project, 64% were proved automatically, leaving 28,000 obligations to be proved by human interaction. Also, no significant feedback is provided for why an obligation could not be proved.
Automated deduction has made significant progress in recent years, including the development of efficient SAT and SMT solvers, and the extension of first-order deduction techniques to fragments of higher-order logic.
The thesis will be carried out at the Inria research center in Nancy, France, and is supported by the ANR project BLaSST, that also involves the industrial partner Clearsy, a leading research group in SAT solving at the CRIL laboratory in Lens, and the University of Liège (Belgium).
The start of the thesis is scheduled for this autumn. Applications will be considered until a candidate is chosen. Applicants should ideally have prior experience in
If you are interested or simply curious about this position, don't hesitate to get in touch with Stephan Merz and Sophie Tourret.
The laboratory for foundations of computer science recruiting a postdoctoral researcher to join the Innovate UK project "Digital Security by Design: Technology Platform Prototype". This is a research collaboration between Arm and the Universities of Cambridge and Edinburgh to develop the Morello platform, applying a novel capability-based architecture to a mainstream high-performance processor and software stack.
Further information below: for full details and how to apply please visit this web site
If you would like to discuss informally then please contact Ian Stark, the project lead for Edinburgh.
The University of Edinburgh only takes formal references after appointment: if you have individual letters of support then please submit these as part of your initial application. This position is not restricted to UK or EU citizens and the university will assist with any visas and work permits necessary.
Follow these links for more about the wider project.
The only essential requirement for these positions is a PhD or equivalent research experience in computer science, informatics, mathematics, or a related discipline. This includes being close to PhD completion and submission.
We are particularly interested to hear from candidates with any of the following. There is no requirement to demonstrate all of these together: this project crosses domains and the precise tasks followed will depend on each researcher's individual skills, experience, and interests.
Christian Suttner, cofounder of the TPTP problem library, died recently in a glider accident while on vacation in South Africa. In addition to his foundational contributions to the TPTP (and hence to ATP in general), Christian was the person who suggested running CASC, and the author of the most succinctly clear definition of ATP ... "systems that automate the derivation of conclusions that follow inevitably from known facts". Christian was a scientist, a businessman, a husband, a father, and a friend. He died doing what he loved - living ... living a wonderfully full and adventurous life.
I found the following interesting piece of news that doesn't quite fit in the usual categories of the newsletter, but that I would like to share anyway. It is nice to see that proof assistants have a big enough community that such an endeavour is launched. As an Isabelle user, I look forward to using this Stack exchange platform, and, in the spirit of Pascal's column above, I am glad it is about proof assistants in general, with the potential of strengthening the cooperation between these tools' communities. I hope it gains momentum.
Proof assistant communities have grown quite a bit lately. They have active Zulip chats: Lean, Coq, Agda, Isabelle. These are good for discussions, but less so for knowledge accumulation and organization, and are not indexed by the search engines.
Andrej Bauer has therefore created a proposal for a new “Proof assistants” StackExchange site (see original post by Andrej Bauer here). Such a site would complement very well various Zulips dedicated to specific proof assistants. If you favor the idea, please support it by visiting the proposal and