The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, choosing the Herbrand Award selection committee, instituting new awards, etc.
The members of the board of trustees until the 2021 elections were:
The terms of Christoph Benzmüller and Stephan Schulz ended. The term of office of André Platzer as CADE-28 programme chair ended after the CADE conference, and Jasmin Blanchette joined the board of trustees as IJCAR 2022 program chair.
This means that two new trustees had to be elected.
The following candidates were nominated and their statements, in alphabetical order, are below:
In this year, the election was carried out using the Condorcet Internet Voting Service (CIVS), and the Condorcet completion Minimax-PM, following the change of the CADE bylaws in 2019. Participants of the last three CADE/IJCAR conferences (who paid registration fees at at least one of the conferences) were invited to vote, and a total of 225 ballots were sent out on September 24. By October 8, 60 CADE members had voted through CIVS, which translates to a participation rate of 26.7% (as compared to 34.5% in 2019, 21.1% in 2018, 9.1% in 2017, 11.2% in 2016).
The results of the election can be viewed on CIVS:.
The two candidates elected are Cláudia Nalon and Stephan Schulz.
The new board of trustees is:
On behalf of the AAR and CADE Inc., I would like to thank Christoph Benzmüller for his service on the board of trustees, and for being the CADE vice-president since 2015, and André Platzer for his service since 2020. I would like to congratulate Cláudia Nalon who will join the board as a new trustee, and Stephan Schulz for being reelected!
I am honoured to be nominated to serve in the CADE's Board of Trustees. I have followed both CADE and IJCAR for many years, in person whenever I could. I have contributed research papers to both conferences, served as a PC member in several opportunities, and helped organising the first edition of CADE in South America.
The very first IJCAR was the very first major conference in AR that I attended. It was exciting then, it is still exciting today to taking part of these meetings. I believe that many would also benefit from the interaction with senior researchers, as I did myself in the early stages of my studies and career. I strongly support the continuation of the Bledsoe Award (that made possible my travelling to Sienna back in 2001), which allows students to attend the conferences, and the newly created Bill McCune's award, which gives visibility to younger researchers and their work in the field.
My research is focused on both the theoretical foundations and practical aspects related to the implementation of proof methods for non-classical logics and their combinations. I have developed and implemented proof systems for non-monotonic logics, many-valued logics, and for several modal logics (normal multimodal logics and their extensions, and parameterised multi-modal confluent logics; interacting epistemic and temporal modal logics; dynamic logics; non-normal modal logics for cooperative agency; preferential logics; etc). Working on theorem-proving for non-classical logics is interesting and challenging. It is also related to many non-trivial industrial applications. It is my intention as a trustee to stimulate the development of theories and tools for such challenging applications, which goes beyond the traditional focus of CADE in classical logics.
I believe the co-location with other major conferences should be continued as it is helpful in fostering further collaboration within the field. As an enthusiastic developer, who believes in the benefits of the fruitful synergy between theory and practice, I advocate for encouraging more submissions of both system's descriptions and research papers related to the practical aspects of automated reasoning. Finally, although boldly going to places where no conferences had gone before is not the motto for CADE, I very strongly believe that a better geographical distribution would be extremely beneficial to our community, helping to stimulate research and disseminate knowledge about AR, and also attracting the talented minds from several underrepresented regions into the field.
I am a tenured professor of computer science at DHBW Stuttgart in Germany. In the CADE community I am probably best known for the development of the theorem prover E (and the many systems build on and around E), and the co-creation of the ES* and PAAR workshop series. I became ex-officio trustee in my role as one of the IJCAR 2018 program chairs, and I was elected to my first full term in 2018.
With the COVID pandemic, two both IJCAR 2020 and CADE 2021 had to move to online formats. I think we learned a lot about the advantages and the disadvantages of such virtual conferences - I eagerly look forward to physical conferences, but I also think we should try to keep some of the advantages of virtual conferences, such as much easier and cheaper access for many more participants.
CADE has decided to move its proceedings to open access, and this intend seems to be shared by our sister conferences. I have strongly supported this move. We now have different attractive open-access options, and I think we need to carefully balance impact and visibility (in particular for younger researchers) vs. cost.
For the same reasons open access is valuable, I also think code of systems described at CADE should be available - ideally in source code under a free license. Many important implementation details and techniques cannot be learned from a short paper, and replication of results is essentially impossible without access to the code. I think this should be at least strongly encouraged, and I will work towards this for future conferences.
I am quite happy with the current schedule of alternating CADE and IJCAR conferences, with a FLoC every 4 years. However, given the real, environmental, and time cost of travel, it might be a good idea to have more collocated events, as e.g. during the Vienna Summer of Logic in 2014.
My current research interests span from explainable AI using abduction in description logics, to the formalization of theoretical frameworks for saturation-based calculi using Isabelle/HOL and the extension of first-order theorem proving techniques to higher-order logic.
I was involved in the organisation of CADE-28 as pc member and publicity chair, and I am a workshop chair for IJCAR 2022, as well as part of the steering comity of PAAR. I am or was also involved as a pc member in the neighbour conferences TABLEAU, CPP, AAAI and IJCAI.
I really enjoy the balance between theory and practice at CADE, as well as the friendly and open atmosphere of our community. As a CADE trustee, I will strive to preserve these strengths of ours, and to nurture the communication and interactions between the different components of our community, as I am already doing as the editor of the AAR newsletter. I will also support the ongoing process of moving to open access proceedings, as well as any endeavour to improve our reproducible research practices.
The Steering Committee of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods ("TABLEAUX") currently has three elected members whose terms will expire:
The Steering Committee is therefore calling for nominations of candidates who wish to contest an election for three positions, which will be held in December 2021.
To nominate please send an email to Jens Otten containing: - the name of the candidate who has already agreed to be nominated; - the name of the second nominator; - a statement from the candidate to be put on the TABLEAUX website.
Only members of the TABLEAUX community may act as nominators and a person may nominate or second only one candidate. Closing date for nominations is November 30th, 2021.
The TABLEAUX community consists of all people who have been registered participants in at least one of the three most recent TABLEAUX Conferences including IJCAR (i.e. TABLEAUX 2019, IJCAR 2020 and TABLEAUX 2021) and all members of the current IJCAR Program Committee.
The current Steering Committee rules and more information can be found on the TABLEAUX website.
The TABLEAUX Steering Committee is now calling for bids to host the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods ("TABLEAUX") in 2023. TABLEAUX typically merges into IJCAR (the International Joint Conference on Automated Reasoning) in even years. Previous TABLEAUX/IJCAR conferences took place in Birmingham/UK (TABLEAUX 2021), Paris/France (IJCAR 2020), London/UK (TABLEAUX 2019), Oxford/UK (IJCAR 2018), Brasília/Brazil (TABLEAUX 2017), Coimbra/Portugal (IJCAR 2016), Wrocław/Poland (TABLEAUX 2015), Vienna/Austria (IJCAR 2014), Nancy/France (TABLEAUX 2013), Manchester/UK (IJCAR 2012), Bern/Switzerland (TABLEAUX 2011), Edinburgh/UK (IJCAR 2010), and Oslo/Norway (TABLEAUX 2009). See here for a complete list of previous conferences.
A bid should cover at least the following aspects: - contact person: name and email address - names of other people involved in the local organization - experience, if any, of organizing previous similar events - planned venue, accessibility and transportation - suggested dates of the conference - plans, if any, for co-location with other meetings, conferences and/or workshops - available accommodation, e.g., hotels and/or dormitory rooms - catering arrangements - any relevant plans for social events, e.g., excursions - a list of potential national and local sponsors - expected expenses and expected registration costs
Bids that consider co-locating TABLEAUX with other conferences, such as FroCoS or ITP, are strongly encouraged. In 2013, 2015, 2019, and 2021 TABLEAUX was co-located with FroCoS (the International Symposium on Frontiers of Combining Systems). In 2017 TABLEAUX was co-located with FroCoS and ITP (the International Conference on Interactive Theorem Proving).
In 2021, TABLEAUX was organized as a hybrid conference, allowing participants to attend the conference on-site as well as online. It is planned to organize TABLEAUX 2023 again as a hybrid conference in order to give everyone interested the chance to participate.
The leader or leaders of the winning bid will become the Conference Chair or Co-Chairs of TABLEAUX 2023. Traditionally they will also become the PC Chair or Co-Chairs; the final decision on this will be made by the TABLEAUX Steering Committee. The PC Chair or Co-Chairs will create a PC in consultation with the TABLEAUX Steering Committee and will also be expected to edit the conference proceedings.
The bid should be limited to 10 pages and should be submitted as a PDF file to Jens Otten.
The deadline for submissions is March 28th, 2022.
The TABLEAUX Steering Committee will decide which bid to accept and announce a decision after the deadline.
Perspective organizers are encouraged to register their intention informally and to get in touch with the TABLEAUX Steering Committee for informal discussion before they submit their bid.
More information about the TABLEAUX conference series and its history can be found here.
Non-classical logics constitute a huge collection of tools for representation of and reasoning within domains that require extension or restriction, in some way or another, of the formal principles usually employed in the mathematical fields. Intuitionistic, modal, and more broadly, non-monotonic logics are examples of such tools that are long known and studied within Philosophy, Mathematics, and also Computer Science. Their adequacy for reasoning in different topical areas has been advocated for many years, as they capture more precisely the nuances intrinsically related to the problems within those areas. Applications of interest range from theoretical foundations of Mathematics over engineering problems to applications in AI: Non-classical logics can be used to represent and reason about computations, conflicting information, provability, temporality, epistemology, defeasible information, norms, vagueness, ... the list goes on and on.
The development of non-classical logics is needed if we intend to deal with complex problems in a complex world. Although some logics are well understood, with well-established model and proof theories, it seems that there is still a lot to do with respect to the automation of the reasoning tasks for those logics. There are, of course, many different tools for many non-classical logics. Their existence, however, seems to rely on individual and continuous efforts of researchers and their groups whilst we can observe a more community-driven and systematic approach to the construction and maintenance of reasoners for classical logics: standards are in place (e.g., the TPTP languages), provers can talk to each other (with little effort), and those provers are under constant scrutiny of the community. This allows for both the easier adaptation and incorporation of implementation techniques and also fosters their correctness and reliability.
The implementation of non-classical provers may require sophisticated techniques, not always adaptable from the classical approaches, in order to rightly and efficiently deal with the kind of reasoning that reflects their often complex semantical counterparts. Every different logic may require very different techniques, and there are too many of such logics.
These and many other problems were discussed in the topical session about non-classical logics that we had the honour to be invited to host at CADE-28. About 20 participants joined the session, raising challenges and obstacles in the field, including the following:
"Stepping into the dark side" may translate well the perception that this list of difficulties is an impediment to the development of reasoner tools for non-classical logics. As we argued in the topical session, our vision is that their applicability should help us to surpass the existing problems and, actually, shed light into the challenges that we need to face to provide a good reasoning service for those intended applications.
Community efforts could, e.g., include a logic independent central, open and free collection of benchmarks (not necessarily in the same format, but standards should arise on the long run) and to encourage domain experts to co-create benchmarks as a service to the automated reasoning community. Currently, there seem to be more open questions than answers, but this also entails (at least in some non-classical formalisms) that there is a vast potential.
It is dark before dawn, and there seems to be interest enough for fostering collaboration between implementers, for proactively planning and working on minimising the existing problems, and stepping towards the light: those challenges (and fun) that are intrinsically related to particular domains and logics themselves. We would be more than happy to receive feedback or ideas (via E-Mail) from interested readers of the newsletter.
The new COST action CA20111 EuroProofNet is the European research network on digital proofs. It aims at boosting the interoperability and usability of proof systems. It gathers 190 researchers on proof systems and formal proofs, from 30 different countries. The action consists of six working groups (WG), which we briefly introduce next.
To join the action, apply to the working groups you are interested in. In addition, feel free to join the Action's Zulip Chat.
UNESCO proclaimed 14 January to be World Logic Day, a global day of supporting the development of logic through teaching and research, as well as to public dissemination of the discipline.
The coordination of World Logic Day 2021 is --for the second time-- in the hands of the Conseil International de Philosophie et des Sciences Humaines (CIPSH) and its member organization, the Division for Logic, Methodology and Philosophy of Science and Technology of the International Union of History and Philosophy of Science and Technology (DLMPST/IUHPST): see here and here.
We would like to encourage logicians all around the world to organize (possibly small) events in close proximity to 14 January 2022 to celebrate this day. It is impossible to predict what type of meeting will be possible in January 2022 and what the international travel situation will be. As a consequence, we should like to ask all organisers to weigh pros and cons of planning in person events, purely online events, or hybrid events before making an announcement. Note that online and hybrid events have the advantage of allowing easy access of people from around the world. Events will be listed on the CIPSH website.
To be added to that list, follow the instructions here or write a short email.
The International Colloquium on Automata, Languages and Programming (ICALP) is the main conference and annual meeting of the EATCS (European Association for Theoretical Computer Science). This year, after two virtual ICALP events, we are happy to be able to host this event in hybrid mode--and hope that many of us will be able to meet again in beautiful Paris! This is a call for workshops to be affiliated with ICALP 2022. We invite researchers to organise workshops on central topics on Automata, Languages and Programming, to help further mark off ICALP 2022.
Important Dates:
More information is available on the colloquium's web page.
The symposium is planned to be held in person at California Institute of Technology, but potentially transitioning to fully virtual if the COVID situation persists. Virtual presentations will be possible even if the conference is held in-person.
The symposium has NO registration fee for presenting and attending.
Theme of Symposium
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry requires advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems. The focus of the symposium will be on formal/rigorous techniques for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace during all stages of the software life-cycle.
Topics of Interest
Topics of interest include, but are not limited to, the following aspects of formal methods:
Important Dates
More information is available on the symposium's web page.
CiE 2022 is the 18th conference organized by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world.
The CiE conferences serve as an interdisciplinary forum for research in all aspects of computability, foundations of computer science, logic, and theoretical computer science, as well as the interplay of these areas with practical issues in computer science and with other disciplines such as biology, mathematics, philosophy, or physics.
Important Dates:
More information is available on the conference's web page.
Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to:
Tracks and Special Sessions
Besides the main track, ICLP 2022 will host additional tracks:
Important Dates
More information is available on the conference's web page.
The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric.
Suggested, but not exclusive, topics of interest include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, foundations of probabilistic, real-time and hybrid systems, games and logic, higher-order logic, knowledge representation and reasoning, lambda and combinatory calculi, linear logic, logic programming, logical aspects of AI, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, process calculi, programming language semantics, proof theory, reasoning about security and privacy, rewriting, type systems, type theory, and verification.
COVID-19 etc..
For people who cannot travel to Israel, the possibility of remote participation will be ensured.
Important Dates
Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is given by anywhere on earth (AoE).
More information is available on the conference's web page.
The ITP conference series is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.
The FLoC organizing committee will make all efforts possible to ensure everyone can attend in person. However, they are very much aware that there might be members of the community who cannot travel to Israel. In cases where travel is not possible, they will ensure people can participate remotely.
Topics
ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include, but are not limited to, the following:
Important Dates
More information is available on the conference's web page.
FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, models of computation, semantics and verification in new challenging areas.
The suggested, but not exclusive, list of topics for submission is:
Important Dates
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
More information is available on the conference's web page.
IJCAR 2022 is the merger conference of the following leading events in automated reasoning:
IJCAR 2022 topics include the following ones:
Important Dates
More information is available on the conference's web page.
Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences.
Topics
We invite submissions on all aspects of modal logic, including:
Important Dates
More information is available on the conference's web page.
Rewriting is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application domains. It also has good properties as a metalogical framework for representing logics. Several successful languages based on rewriting (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of WRLA is to bring together researchers with a common interest in rewriting and its applications, and to give them the opportunity to present their recent work, discuss future research directions, and exchange ideas.
The topics of the workshop include, but are 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 working in the fields of Program Verification and Program Transformation.
There is a great potential for beneficial interactions between these two fields because:
The workshop will provide a forum where researchers from these fields may interact and foster new developments.
The workshop solicits research, position, application, and system description papers with a special emphasis on case studies, demonstrating viability of the interactions between the research fields of program transformation and program verification in a broad sense. Also papers in related areas, such as program testing and program synthesis are welcomed.
The workshop offers twofold benefits for the verification community. On the one hand it will rise awareness of and stimulate the development of novel verification methods and techniques. On the other hand it will draw attention of the community to the novel and challenging verification problems and research opportunities.
Topics of Interest
include, but are not limited to:
Important Dates:
More information is available on the workshop's web page.
The scope of this special issue is open to contributions by researchers, from both academy and industry, working in the multidisciplinary field of XAI.
Topics of Interest
Topics relevant to this special issue include ? but are not limited to ? the following:
Deadline
VerifyThis is a series of program verification competitions, which has taken place annually since 2011 (with the exception of 2020). Previous competitions in the series have been held at FoVeOOS 2011, FM 2012, Dagstuhl (April 2014), and ETAPS 2015—2021.
To extend the problem pool and tend better to the needs of the participants, we are soliciting verification problems for the competition:
Problems from previous competitions can be seen at the archive.
Please send submissions via email by January 31, 2022.
The most suitable submission for competition will receive a prize.
More information is available on the competition's web page.
The Core Initiating Committee of the Proof Society and the organising committee are very happy to announce the third edition of The Proof Society Workshop on Proof Theory and its Applications together with the Winter School on Proof Theory. The events will be presencial and shall not be streamed online.
The intended audience for the Winter School is advanced master students, PhD students, postdocs and experienced researchers new to the field in mathematics, computer science and philosophy. The workshop will bring together researchers on proof theory and its applications through a series of invited and contributed talks as well as panel discussion.
Both events will be held in Madeira in 2021 in the week from Monday, November 29 through Friday, December the third.
Confirmed speakers include:
The important dates are:
More information is available on the school's web page.
Attendance Modes: In-person in Bergen, Norway (admitted students) or online (general public)
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 students.
Confirmed Lectures
Registration
More information is available on the school's web page.
Overview
Homotopy Type Theory and Univalent Mathematics are emerging fields of mathematics that study
a fruitful relationship between homotopy theory and (dependent) type
theory.
This relation plays a crucial role in Voevodsky's program of Univalent
Foundations, a new approach to foundations of mathematics, based on
ideas from homotopy theory, such as the Univalence Principle.
The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is freely available for everyone, as an open-source project, from the web. The School will give many young researchers an opportunity to familiarize themselves with the UniMath library and become contributors.
Participants will receive an introduction to Univalent Foundations and to Mathematics in those foundations, by leading experts in the field. In the accompanying problem sessions, participants will formalize pieces of Univalent Mathematics in the UniMath library.
Lecturers
Guest Speakers
Schedule
More information is available on the school's web page.
The Department of Mathematics and Computer Science of the Eindhoven University of Technology, The Netherlands, has a vacancy for a tenured/tenure track assistant professor in the Formal System Analysis (FSA) group.
The Formal System Analysis Group studies formal techniques to model and analyse software and hardware systems. The goal is to develop techniques that are both mathematically elegant and practically effective. Techniques typically used are term rewriting, fixed points, parity games, SAT and SMT solving and symbolic state space representations. The group maintains the mCRL2 toolset, which is in use at a number of major industries and public bodies, generally as a verification backend. The group has strong ties with industrial partners and actively strives to apply its methods in industrial contexts.
The group is particularly keen on strengthening its expertise in automated reasoning, SAT solving and SMT solving.
This vacancy is part of the Irène Curie Fellowship and is currently only open for female candidates. Male applicants will not be considered for the position. As an Irène Curie Fellow, you are entitled to a substantial start-up package to kick-off your career.
For more information, see here or contact dr.ir. T.A.C. (Tim) Willemse.
Applications will be screened as soon as they are received. Screening will continue until the position has been filled.
Revantha Ramanayake and Helle Hvid Hansen invite excellent PhD candidates to join us at the Fundamental Computing group, Bernoulli Institute for Maths, CS and AI, University of Groningen.
Founded in 1614, the University of Groningen is proud to number among the world’s top universities with a ‘Top 100’ ranking in the most recent ARWU Shanghai Ranking and the THE World University Rankings, among others. With the youngest population in the Netherlands (more than 20% international), Groningen is a lively, cosmopolitan city, as well as a very safe and eco-friendly city to live in, rated highly for quality of life, education, social care and healthcare.
Three fully-funded 4-year PhD positions are available:
Prospective candidates are encouraged to contact the respective supervisor to express their interest well in advance of the deadline.
David Pym is looking for a PhD student in logic, in the PPLV group at UCL in London. The project is to work on logic as basis for system modelling. Examples of questions to be addressed include:
The logical systems of interest as a basis for this work are likely to include dynamic, epistemic, deontic, and doxastic approaches, with case studies in security and policy modelling. I would expect the project to require both theoretical work in logic and more applied work in modelling, with a particular focus on systems security models and security policy models.
The PPLV group provides an outsanding environment in which to study logic and UCL’s information security group, the Science, Technology, Engineering and Public Policy Department, and the Security and Crime Science Department provide an excellemnt environment for studying security. We have excellent connections to logicians and security researchers across UCL, London, and the wider world.
The studentship will be part of UCL’s Centre for Doctoral Training (CDT) in Cybersecurity: see here and here to find advice on how to apply may be found.
The CDT requires that all students engage in an advanced interdisciplinary programme in security during their first year. This programme provides an excellent context for students’ specific research projects.
Although most of the CDT’s funding is for UK nationals, international candidates can also be considered.
The Institute of Information Security at University of Stuttgart offers a fully-funded Postdoc position in formal verification
The successful candidate is expected to work on tool-supported formal verification of security-critical systems and security protocols.
The position is available immediately with an internationally competitive salary (German public salary scale TV-L E13 or TV-L E14, depending on the candidate's qualification, ranging from about 4.600 Euro to 6.200 Euro monthly gross salary). The appointment period follows the German Wissenschaftszeitvertragsgesetz (WissZeitVg), ranging from one year to up to six years.
The Institute of Information Security offers a creative international environment for top-level international research in Germany's high-tech region.
The successful candidate should have a Ph.D. (or should be very close to completion thereof) in Computer Science, Mathematics, Information Security, or a related field. We value strong analytical skills and
The University of Stuttgart is an equal opportunity employer. Applications from women are strongly encouraged. Severely challenged persons will be given preference in case of equal qualifications.
To apply, please send email with subject "Application: Postdoc Position Formal Verification" and a single PDF file containing the following documents to Ralf Küsters:
The deadline for applications is October 31st, 2021. Late applications will be considered until the position is filled.
See here for more information about the institute.
See here for the official job announcement.
For further information please contact: Prof. Dr. Ralf Küsters.
One year postdoctoral research position is available at the Charles University in Prague. See here.
The call is broad and theoretically oriented. Nevertheless, one concrete option is a candidate who would want to participate on the formalization effort in the area of Combinatorics on Words within Isabelle. See here.
Feel free to contact David Stanovsky if you want to know more.
We are looking for a researcher to strengthen our Safety & Security team at fortiss, a research institute in Munich with close connections both to the Munich universities TUM and LMU and to industry.
The Safety & Security team develops new methods and engineering principles related to safety and security in software and system development. Example areas of interest include:
The position is available starting as soon as possible and will be for at least two years initially, with the possibility of extension. You would be a team member contributing to our research in one of the above areas. Applications from candidates with skills in related areas are also welcome.
More details about this position can be found here.
Applications are invited for a one-year postdoctoral position at the University of Minnesota. The position is available immediately; applications will be reviewed as they are received.
The project within which the appointment is to be made concerns the development of a framework that supports the encoding of rule-based relational specifications and the process of reasoning about such specifications through the encoding. An emphasis in the project is the use of the so-called higher-order abstract syntax approach to representing objects that embody a binding structure. In recent work, we have developed a new logic for articulating properties of LF specifications, which has provided the basis for a proof assistant called Adelfa for reasoning about such properties. In other work, we are developing the capability to reason about linear logic specifications within the Abella proof assistant and are also using this system to explore the benefits of higher-order representations of syntax in the verification of compilers and transformers for functional programming languages. The successful candidate will be expected to participate in and help lead the work in some of these directions.
To be suitable for the position, the candidate should be broadly conversant with the areas of computational logic and programming languages and should have the mathematical and programming skills necessary for conducting research in them. Some particular facets that would be helpful in engaging immediately with the research problems are a prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as fixed-point definitions, and familiarity with issues related to proof search in sequent calculi and similar logical systems.
Please feel free to contact Gopalan Nadathur for more details about the position. To view the official announcement, please visit this URL.
This site also provides details about how to apply and serves as the portal for applications. A prerequisite for employment in this capacity is a doctoral degree in Computer Science or closely related field.
IRIF (CNRS and Université de Paris), Paris, France, is seeking excellent candidates for postdoctoral positions in all areas of the Foundations of Computer Science. Every year, 5-10 new postdocs join IRIF.
IRIF (Institute for Research in Foundations of Computer Science) is a joint laboratory of the CNRS (French National Center for Scientific Research) and Université de Paris. Currently, it hosts about 90 permanent faculty members, 40 non-permanent full-time researchers, and 50 Ph.D. students. For further information about IRIF please see here.
The postdoc positions at IRIF are financed either by the laboratory resources, or by group or personal grants, or by joint applications of IRIF members and the candidate to outside funding agencies with which IRIF is affiliated.
The starting date of the positions is usually in September-October, but this may sometimes vary. Candidates must hold a Ph.D. degree in Computer Science or a related area before the starting date of the position. Knowledge of French is not required, and applications can be sent either in French or in English.
The application deadline for most application tracks is November 1st, 2021. For a list of specific openings as well as instructions how to apply please visit this webpage.
The Institute for Logic, Language and Computation (ILLC) at the University of Amsterdam currently has a vacancy for an Assistant Professor in Model-Based AI.
We are looking for a specialist in an area of model-based AI such as, for instance, SAT solving, constraint programming, planning and scheduling, answer set programming, description logics, ontology engineering, or computer-aided verification. We hope that you will be able to connect with the long and proud research tradition in logic at the ILLC, while also reaching out to the broader AI research community in Amsterdam.
Deadline: 22 November 2021
Full details: see here
Contact: Please do not hesitate to contact Ulle Endriss if you have any questions.
A postdoctoral position is available in the Computer Science department at Boston College under the supervision of Jean-Baptiste Tristan and Joseph Tassarotti. The candidate will join our project on the formally verified compilation of probabilistic programs.
The goal of the project is to use the Coq proof assistant to implement a compiler for the Stan programming language and prove that the generated inference algorithm converges to the distribution specified by the input program. Our project builds upon the CompCert compiler and compiles Stan programs with a succession of well-defined program transformations. Candidates are expected to participate in the generalization of existing transformations to more features of the Stan language, the design and implementation of new transformations, the definition of the operational semantics of the intermediate languages, and the proofs of semantics preservation.
Successful candidates must be proficient in scientific writing and have a track record of expertise in at least one of the following topics:
The position is available immediately, with a flexible starting date. It includes funds for travel to conferences and comes with no teaching load.
Interested candidates should apply at this link and contact Jean-Baptiste Tristan and Joseph Tassarotti with a copy of their CV.
Jeremy Avigad and colleagues are seeking to fill a joint postdoctoral position between the Department of Mathematical Sciences and the new Hoskinson Center at Carnegie Mellon, starting in Fall 2022. More information can be found here. The deadline is December 15, 2021.
The position is designed to allow promising young mathematicians to develop their careers while also exploring the use of formal methods (based on Lean) in their teaching and research.
The novel interdisciplinary Marie Skłodowska-Curie COFUND doctoral training programme LogiCS@TUWien - Logics for Computer Science co-funded by the European Commission, will offer 20 full-time PhD positions. The program is hosted by TU Wien, one of the most successful technical universities in Europe and the largest one in Austria. The Faculty of Informatics of TU Wien is a leading research and teaching institution which consistently ranks among the top 100 computer science faculties in the global Times Higher Education ranking. In the heart of Europe, Vienna has a distinguished history in mathematics, computer science, and logic research and offers one of the highest living standards in the world.
The doctoral positions are open to international high-potential early-stage researchers working on Logical Methods in Computer Science and their applications, including:
The programme provides a 4-year long doctoral training for international PhD candidates within an English-language curriculum. LogiCS@TUWien will run for 60 months and foresees the recruitment of 20 PhD candidates. The PhD candidates will be supervised by:
Two calls will accomplish the recruitment of the 20 positions. The first call is now open, with an application deadline of December 30, 2021.
For details on how to apply, see this webpage or watch the video here.