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.
Nominations for two CADE trustee positions are being sought, in preparation for the elections to be held after CADE-28.
The current members of the board of trustees are (in alphabetical order):
The terms of Christoph Benzmüller and Stephan Schulz end. Stephan Schulz may be nominated for a second term, whereas Christoph Benzmüller has already served two consecutive terms and cannot be nominated this year.
The term of office of André Platzer as CADE-28 programme chair ends after the CADE conference. As outgoing ex-officio trustee, André Platzer is eligible to be nominated as elected trustee.
In summary, we are seeking to elect two trustees.
Nominees must be AAR members. Nominations can be made by any CADE member, either by e-mail or at the CADE business meeting at CADE-28; since nominators must be CADE members, they must have participated at at least one of the CADE or IJCAR conferences in the years 2018-2021. 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.
The International Conference on Automated Deduction (CADE) Herbrand Award for Distinguished Contributions to Automated Reasoning is presented to
Tobias Nipkow
in recognition of his leadership in developing Isabelle and related tools, resulting in key contributions to the foundations, automation, and use of proof assistants in a wide range of applications, as well as his successful efforts in increasing the visibility of automated reasoning.
More and more automatic theorem provers output evidence of their answers. When they derive the unsatisfiability of a given conjunction of formulas, these witnesses are called proof certificates. They are used to increase the confidence in these provers by checking a posteriori their claims, as well as for proof reconstruction to enjoy automation in interactive provers without increasing their trusted base. A major example is the check in the Coq proof assistant of the proof of the Boolean Pythagorean Triples problem, which was encoded into a Boolean unsatisfiability problem generating a raw proof certificate of 200 terabytes in size.
Certificates can be understood in a very large sense as an evidence that the result of a program satisfies the expected specification. Now widely spread in the automated reasoning community, another example is their use to validate some compilation phases. Verifiable computing, which allows one to check the result of any program with high probability by a cryptographic approach (also satisfying zero-knowledge properties), can be seen as a universal certificate of the execution of a program - but saying nothing on the functional correctness of the program.
Let us come back to automated reasoning.
Certificates for Boolean unsatisfiability are largely studied and optimized, with formats such as D/LRAT or DRUP which have a good balance between the difficulty to generate certificates, to check certificates, and the size of certificates. However, for more expressive solvers, a curse of Babel starts to appear: for instance, while formats have been proposed for Satisfiability Modulo Theory (SMT) solvers, no standard has emerged yet. TPTP provers could be seen as enjoying a common certificate format, but if the syntax is indeed standardized - which is already a good point for parsing - the semantics is not since any prover may use its own set of inference rules.
Then, what should the requirements on these inference rules be? At first sight, it seems that they should be simple enough so that it is "easy" to check them. In this statement, "easy" could be understood in different (possibly compatible) ways: in terms of computational complexity, or of logical atomicity. Unfortunately, this is contradictory with other requirements: they should be easy to output for provers, and they should also be small enough to be stored in memory.
My claim is that these two problems - different formats, and the contradiction in the requirements of the formats - are actually not so important, thanks to the power of certificates.
The power is that, for all the applications of certificates listed above, we actually do not care about the correctness of certificates. What we do care about is the correctness of the answer of the prover. Certificates are only a way to help establishing this latter, but they can be manipulated, completed, etc as much as needed to actually get convinced of the answer.
With this in mind, the first problem - the difference between formats - can be solved by means of encodings between formats, those encodings having no need to be trusted. Regarding the second problem, a certificate only containing one step is of course useless, but even few steps - and even non-atomic ones - are already of good help if they can be given (maybe on demand) to some tools dedicated to these particular steps that can progressively refine the certificate. An example is that an SMT solver may not detail Boolean and theory reasoning, as long as it separates them so that they can be detailed by as many (simpler) tools as kinds of reasoning.
So what is a good certificate format? It is actually a *documented* format, such that, for each step, one can identify the fragment that it handles, and thus how to encode it in another format or to refine it with another tool. Certificates are spreading across domains, for instance proof of programs, thanks to this flexibility and interoperability.
The Software Foundations team is pleased to announce another new volume in the series and significant updates to other volumes.
New Volume
Software Foundations volume 6, Separation Logic Foundations, by Arthur Charguéraud, is an in-depth introduction to separation logic—a practical approach to modular verification of imperative programs—and how to build program verification tools on top of it.
Updated Volume
Volume 2, Programming Language Foundations, surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems. The concrete notations in this volume have been extensively revamped for better readability, using the advanced Notation features of recent versions of Coq.
The other volumes in the series have been updated to track the current Coq release and incorporate many large and small improvements made since the last release. Watch for a major update to Volume 5, Verifiable C, later this summer!
All Software Foundations titles are available electronically, free of charge.
This book is an introduction to data structures and algorithms for functional languages, with a focus on proofs. It covers both functional correctness and running time analysis. It does so in a unified manner with inductive proofs about functional programs and their running time functions. All proofs have been machine-checked by the proof assistant Isabelle.
The book can be freely downloaded here.
The conference on Automated Deduction (CADE) is the major international forum at which research on all aspects of automated deduction is presented. The first conference was held in 1974, with this year's conference being the 28th CADE. Early CADEs were mostly biennial, and annual conferences started in 1996. The CADE conference series is managed by CADE Inc.
The 28th International Conference on Automated Deduction (CADE-28) will be virtual due to the COVID-19 pandemic.
Important Dates:
For information about registration, see the conference website's participation section.
A preliminary program is available on easychair.
More information is available on the conference's web page.
Workshops (June 27-28, 2021):
More information is available on the symposium's web page.
CiE 2021 is the seventeenth conference organized by the Association Computability in Europe. The /Computability in Europe/ conference (CiE) series has built up a strong tradition for developing a scientific program which is interdisciplinary at its core bringing together all aspects of computability and foundations of computer science, as well as the interplay of these theoretical areas with practical issues in CS and other disciplines such as biology, mathematics, history, philosophy, and physics. For more information about the CiE conferences and the Association CiE, please have a look here.
CiE 2021 will be the second CiE conference that is organized as a virtual event and aims at a high-quality meeting that allows and invites active participation from all participants. It will be hosted virtually by Ghent University.
Registration:
CiE 2021 will be hosted virtually. In order to enhance the social dimension of the conference we will be using gather.town with Zoom integrated. In order to register for CiE 2021, please go here.
Registration is free but required.
More information is available on the conference's web page.
CALP is the main conference and annual meeting of the European Association for Theoretical Computer Science (EATCS).
Workshops - 11-12 July 2021
More information is available on the colloquium's web page.
The 2021 edition of FSCD and of its satellite workshops will be held online. Participation will, a priori, be free of charge, unless we receive way too many requests, in which case we will invite those who can to pay the modest amount of 7 USD.
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 (e.g., quantum computing, probabilistic computing, homotopy type theory), semantics and verification in new challenging areas (e.g., blockchain protocols or deep learning algorithms).
Registration
The registration page is already open and linked from here.
This link should be used also to register for affiliated workshops.
Registration is open until July 11.
FSCD 2021 will run over the Clowdr platform. After the registration is closed, you will receive an invitation link and instructions on how to participate.
More information is available on the conference's web page.
Submission of Workshop Proposals
Researchers and practitioners are invited to submit proposals for workshops on topics in the field of computer science, related to logic in the broad sense.
Each workshop proposal must indicate one affiliated conference of FLoC 2022.
It is strongly suggested that prospective workshop organizers contact the relevant conference workshop chair before submitting a proposal.
Each proposal should consist of the following two parts.
The FLoC Organizing Committee will determine the final list of accepted workshops based on the recommendations from the Workshop Chairs of the hosting conferences and availability of space and facilities.
Proposals should be submitted through EasyChair.
Please see the Workshop Guidelines page for further details and FAQ.
Important Dates
Contact Information
Questions regarding proposals should be sent to the workshop chairs of the proposed affiliated conference. General questions should be sent to:
More information is available on the conference's web page.
GANDALF 2021 is planned to be a hybrid conference. We aim at organizing an in-presence event, but there will be possibilities for virtual participation for delegates affected by travel restrictions.
The aim of GandALF 2021 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 (all dates are AoE)
More information is available on the symposium's web page.
The 4th International Conference on Logic and Argumentation (CLAR 2021) invites contributions from logic, artificial intelligence, philosophy, computer science, linguistics, law, and other areas studying logic and formal argumentation.
CLAR 2021 will be held at Zhejiang University City College. Due to the uncertainties of the epidemiological situation, the conference will be held in a HYBRID format (virtual and physical attendance both accepted), and we encourage physical participation if possible.
Papers accepted to CLAR 2021 will be published as Springer LNAI proceedings, and will be available online during the conference. Authors of selected papers will be invited to submit an extended version to a journal special issue after the conference.
The CLAR 2021 conference will highlight recent advances in logic and argumentation and foster interaction between these areas within and outside China.
List of Topics
Suggested topics include, but are not limited to the following:
Important Dates
More information is available on the conference's web page.
Due to the covid-19 pandemic, synasc 2021 will be organized as a hybrid event. Note that if the general health situation due to the covid-19 pandemic does not allow for an in-presence event, the symposium will still be held in a remote mode.
Aim
SYNASC aims to stimulate the interaction among multiple communities focusing on defining, optimizing and executing complex algorithms in several application areas.
The focus of the conference then ranges from symbolic and numeric computation to formal methods applied to programming, artificial intelligence, distributed computing and computing theory. The interplay between these areas, in fact, is essential in the current scenario where economy and society demand for the development of complex, data intensive, trustable and high performant computational systems.
Tracks
Important Dates
More information is available on the symposium's web page.
Contributions are sought in all areas of logic programming, including but not restricted to:
Important Dates
More information is available on the conference's web page.
Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL).
It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.
Currently, we expect that the conference will be organized in a hybrid way: both with an in-presence component and an online component.
List of topics:
Important dates:
More information is available on the conference's web page.
Formal methods emerged as an important area in computer science and software engineering about half a century ago. An international community is formed researching, developing and teaching formal theories, techniques and tools for software modeling, specification, design and verification. However, the impact of formal methods on the quality improvement of software systems in practice is lagging behind. This is for instance reflected by the challenges in applying formal techniques and tools to engineering large-scale systems such as Cyber-Physical Systems (CPS), Internet-of-Things (IoT), Enterprise Systems, Cloud-Based Systems, and so forth.
The purpose of the SETTA symposium is to bring international researchers together to exchange research results and ideas on bridging the gap between formal methods and software engineering. The interaction with the Chinese computer science and software engineering community is a central focus point. The aim is to show research interests and results from different groups so as to initiate interest-driven research collaboration. The SETTA symposium is aiming at academic excellence and its objective is to become a flagship conference on formal software engineering in China.
To achieve these goals and contribute to the sustainability of the formal methods research, it is important for the symposium to attract young researchers into the community. Thus, this symposium encourages in particular the participation of young researchers and students.
List of Topics
Topics of interest include, but are not limited to:
Important Dates
More information is available on the symposium's web page.
As we are observing some growing interests in topics related to connexive logics, after six annual workshops, the Trends in Logic XXI aims at discussing directions for future research in connexive logics.
Any papers related to connexive logics are welcome. Topics of interest include (but are not limited to) the following:
Important Dates:
More information is available on the conference's web page.
LFCS topics of interest include, but are not limited to: constructive mathematics and type theory; homotopy type theory; logic, automata, and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; parameterized complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logics; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple agent system logics; logics of proof and justification; nonmonotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; other logics in computer science.
Important Dates.
More information is available on the symposium's web page.
Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics, logic, and education.
CPP 2022 will welcome contributions from all members of the community. The CPP 2022 organizers will strive to enable both in-person and remote participation, in cooperation with the POPL 2022 organizers.
Topics of Interest
We welcome submissions in research areas related to formal certification of programs and proofs. The following is a non-exhaustive list of topics of interest to CPP:
Important Dates
More information is available on the conference's web page.
NeSy is the annual workshop of the Neural-Symbolic Learning and Reasoning Association. The goal of Neural-Symbolic Integration is to combine neural networks' robust learning mechanisms with symbolic knowledge representation, reasoning, and explanation capability in ways that retain the strengths of each paradigm.
NeSy invites theoretical and applied submissions that span both connectionist and symbolic learning paradigms. We further invite papers detailing experimental and in-the-wild neural-symbolic systems and papers on topics where neural-symbolic learning has a strong use case. Topics of interest include, but are not limited to:
Important Dates:
More information is available on the workshop's web page.
Remote Participation due to COVID-19 Pandemic We understand that the global public health situation may make it difficult or impossible for some, if not all, participants to travel to Hanoi. For this reason, we commit to allowing authors of accepted papers to present virtually and will work hard to enable the best possible experience for all conference participants.
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. 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.
Second-order quantifier elimination (SOQE) is the problem of equivalently reducing a formula with quantifiers upon second-order objects such as predicates to a formula in which these quantified second-order objects no longer occur. In slight variations, SOQE is known as forgetting, projection, predicate elimination, and uniform interpolation. It can be combined with various underlying logics, including propositional, model, description and first-order logics. SOQE and its variations bear strong relationships to Craig interpolation, definability and computation of definientia, the notion of conservative theory extension, abduction and notions of weakest sufficient and strongest necessary condition, and generalizations of Boolean unification to predicate logic. It is attractive as a logic-based approach to various computational tasks, for example, the computation of circumscription, the computation of modal correspondence properties, forgetting in knowledge bases, knowledge-base modularization, abductive reasoning and generating explanations, the specification of non-monotonic logic programming semantics, view-based query processing, and the characterization of formula simplifications in reasoner preprocessing.
Topics of interest include, but are not limited to:
The workshop aims to bring together researchers working on SOQE and all these related topics to present, discuss and compare issues shared by problems emerging from different special contexts, interesting open research problems (perhaps with partial solutions), new applications and implementation techniques.
Important Dates
More information is available on the workshop's web page.
FMTea21 is a one-day combined workshop and tutorial that brings together researchers and educators working on formal methods to share their experiences in teaching formal methods, discuss key challenges, and stimulate collaboration that can lead to ways to reboot the presence of formal methods in curricula.
Objectives and Scope
Formal Methods provide software engineering with tools and techniques for
rigorously reasoning about the correctness of systems. While in recent years
formal methods are increasingly being used in industry, university curricula are
not adapting at the same pace. Some existing formal methods classes interest and
challenge students, whereas others fail to ignite student motivation. It is thus
important to develop, share, and discuss approaches to effectively teach formal
methods to the next generations. This discussion is now more important than ever
due to the challenges and opportunities that arose from the pandemic, which
forced many educators to adapt and deliver their teaching online. Exchange of
ideas is critical to making these new online approaches a success and having a
greater reach.
Topics
In the workshop part of the event, we welcome papers detailing experiences with
FM Teaching, including papers discussing successes and failures of various
methods, case studies, tools, etc. Given the increasing importance of online
teaching and self-learning, we also welcome reports of experiences with online
teaching, including experiences with teaching formal methods via MOOCs. We
invite novel papers that cover, but are not limited to, the following aspects:
Important Dates
More information is available on the workshop's web page.
COVID-19 Information
Taking into account the emergency situation, the organizers of OVERLAY 2021 will
closely monitor the evolution of the pandemic and will take all the necessary
actions to guarantee a successful event.
In the case that an in-person event will not be possible, OVERLAY 2021 will be a
hybrid or fully virtual conference. Updates on the organization mode will be
published and advertised in due time.
In any case, OVERLAY 2021 will be a no-fee event.
The increasing adoption of Artificial Intelligence techniques in safety-critical systems, employed in real world scenarios, requires the design of reliable, robust, and verifiable methodologies. Artificial Intelligence systems employed in such applications need to provide formal guarantees about their safety, increasing the need for a close interaction between the Artificial Intelligence and Formal Methods scientific communities. To witness this increasing need, tools and methodologies integrating Formal Methods and Artificial Intelligence solutions are getting more and more attention.
The workshop is the main official initiative supported by the OVERLAY group. The event aims at establishing a stable, long-term scientific forum on relevant topics connected to the relationships between Artificial Intelligence and Formal Methods, by providing a stimulating environment where researchers can discuss about opportunities and challenges at the border of the two areas.
Important goals of the workshop are
Topics of interest include (but are not limited to): automata theory automated reasoning automated planning and scheduling controller synthesis formal specification languages formal verification game theory hybrid and discrete systems logics in computer science reactive synthesis runtime verification and monitoring specification and verification of machine learning systems tools and applications
Important dates
More information is available on the workshop's web page.
The FMM workshop series enables mathematicians interested in computer assistance and researchers in formal and computer-understandable mathematics to meet and exchange ideas. The meeting provides a platform for discussion of suitable forms of computer assistance between the formal community and interested mathematicians and other researchers.
The main points of interest include
Important Dates
More information is available on the workshop's web page.
The 17th 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):
Important Dates
DC students are highly recommended to attend the Autumn School on Logic Programming and Constraint Programming.
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 of interests include (but are not limited to):
Important Dates
More information is available on the workshop's web page.
Modalities and predicates have since ancient time been central notions of logic. In the 20th century, various systems of non-classical logics have emerged, with applications in many disciplines like Computer Science, Linguistics, Mathematics, and Philosophy. This gave rise to the questions of a non-classical treatment of quantifiers and modalities and the accommodation of quantifiers and modalities in non-classical logics. In response, various modal and predicate variants of non-classical logics have been introduced and studied in the past decades.
NCMPL is a conference series solely dedicated to modal and predicate non-classical logics. The aim of the conference is to bring together researchers from various branches of non-classical logics, not only to present recent advances in their particular fields, but also to identify common problems and methods and foster the exchange of ideas between researchers from separate fields.
Topics of interest
The scope includes theoretical works on the above topics coming from all branches of formal logic (proof-theory, model theory, game theory, computational complexity, philosophical and historical aspects), as well as their applications in computer science, linguistics, philosophy, etc.
Strong papers on propositional logics can also be accepted, provided they relate to the themes in the main scope of the conference (e.g., the study of completions in algebraic semantics, infinitary logics, etc.).
Full versions of selected papers will be published in a special issue of an international peer-reviewed journal (to be specified).
Important dates
More information is available on the conference's web page.
Rewriting is a powerful model of computation that underlies much of declarative programming and is ubiquitous in mathematics, logic, theorem proving, verification, model-checking, compilation, biology, chemistry, physics, etc.
The school is aimed at Master and PhD students, researchers and practitioners interested in the use or the study of rewriting and its applications.
Courses
Registration Registration is already open (see here) and closes on July 2, 2021. Registration is free but required.
More information is available on the school's web page.
We are happy to announce that ESSLLI 2021 will be held as an online event in the period 26 July -14 August. The school offers an excellent program of courses and workshops and the well established Student Session. In view of the online format, the program is spread over three weeks so as to facilitate attendance. Details on the schedule will be posted on the website shortly.
The registration will be open until the beginning of the school or until all slots are filled
Courses and Workshops cover three main themes:
More information is available on the school's web page.
The purpose of the Reasoning Web Summer School is to disseminate recent advances on reasoning techniques and related issues that are of particular interest to Semantic Web and Linked Data applications. It is primarily intended for postgraduate (PhD or MSc) students, postdocs, young researchers, and senior researchers wishing to deepen their knowledge.
As in the previous years, lectures in the summer school will be given by a distinguished group of expert lecturers carefully selected to cover a wide range of topics relevant to the school (see below).
The students attending the RW school are particularly encouraged to also apply to the Doctoral Consortium of RuleML+RR.
Important dates
More information is available on the school's web page.
We are delighted to announce Logic and Interactions 2022: a five week session at the CIRM in Luminy (Marseille, France), on logic and its interactions in mathematics and computer science, but also in the broader perspective of its transdisciplinary nature, with connexions to philosophy and linguistics. Two weeks will be organized as thematic schools targeted primarily at PhD students and non-specialist researchers. The other three will be workshops presenting the state of the art in specific areas.
As for previous sessions, we expect this event to offer a friendly venue not only for established specialists but also for students and young researchers as well as non-specialists. In addition to the thematic schools, each week will include introductory material. We encourage colleagues, and especially students and young researchers, to attend several weeks or even the full month, in order to make the most of this special occasion.
Practical information
We hope that the sanitary conditions will allow us to hold the event
mainly in the pre-CoVid fashion: with participants attending physically
at the CIRM. In any case, attending remotely will certainly be possible:
the CIRM has invested a lot of efforts to make hybrid events the
standard practice.
Accommodation at the CIRM will be available for participants attending physically. A limited number of fundings will be available to cover the accommodation and travel expenses, especially for students.
Pre-registrations will open soon. In the meantime, you can already save those weeks in your agenda.
More information is available on the school's web page.
Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis.
After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques.
The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas.
The competition will be affiliated to CADE 2021. The competition will be run on the StarExec platform shortly before CADE.
We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications.
A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed.
Important dates
For further information, we refer to the website of the termination and complexity competition.
HENSOLDT Cyber develops embedded IT products that meet the highest security requirements. It integrates an invulnerable operating system with security-hardened hardware to build the most secure product on the global IT market. The company combines more than 50 years of domain experience with world-class expertise in hardware and software design to achieve global leadership.
We are buidling up a new research team, which is working on cutting-edge projects targeting the aspects formal verification, operating system design and cryptography with the focus on secure embedded systems. If you have a strong interest and/or background in secure operating system development, we would like to get in touch with you.
Tasks
Requirements
We are not only offering flexible and mobile working, but the opportunity to be involved in the development of cutting-edge security products in an international and innovative environment.
Did we spark your interest? Then we are looking forward to your application. If you have any questions on the vacancy please don't hesitate to contact us via mail.
We are offering one 4-years PhD grant on themes of ontology-based knowledge transformation and reasoning. The position is offered by the faculty of Computer Science of the Free University of Bozen-Bolzano (Italy) jointly with the Data and Knowledge Management unit at Fondazione Bruno Kessler, Trento (Italy) where most of the research activities will be conducted.
The deadline for applications will be on the 30th of June, 2021.
For application and more information on the call, see here (see "Call for specific part" document for grants funded by external parties).
We are looking for students interested in topics related to:
The Data and Knowledge Management unit is a research group internationally known for its activity in fields of logic-based representation of knowledge, logical-statistical inference, Semantic Web systems and knowledge acquisition methods. The PhD will be conducted under the joint supervision of Dr. Loris Bozzato (DKM) and a member of the CS faculty of UniBZ.
To know more about the activities of the Data and Knowledge and the possibilities of this call, contact Dr. Loris Bozzato or Dr. Luciano Serafini.
We are looking for a motivated postdoctoral scholar to work on formal methods for the development of high-assurance software and cyber-physical systems. In particular, the project involves the development and enhancement of systems through the composition and verification of programs written in high-level domain-specific languages (DSLs). Potential research problems include:
Location
You will be a member of the Institute for Software Research, School of Computer Science at Carnegie Mellon University in the USA. Pending the evolving situation with COVID-19, you will be expected to work from Pittsburgh, PA.
Qualifications
Candidates are expected to have a PhD in Computer Science or related fields, with a strong background and research record in formal methods, software engineering, and/or programming languages. Familiarity with automated verification technologies (e.g., model checkers, SMT solvers) is desirable.
Timeline
The position is expected to begin in September 2021 for 1 year, with a possibility of extension.
Instructions
To apply, please send a copy of your latest CV and research statement to Eunsuk Kang.
The Programming Methodology group at ETH Zurich is recruiting PhD students and post-docs in the area of program verification. We are especially interested in strengthening our teams working on Rust verification and Go verification. Our goal is to develop verification techniques and tools that can be used to prove correctness and security of advanced systems.
Key requirements for successful applications:
Applications and questions should be sent to Peter Müller. The application should include a CV and a description of research interests. We will consider applications until the positions are filled. The start date is negotiable.
More details about the positions:
General information on doctoral studies at ETH is available here
There is an opening for a 3-year PhD position at University of Lille, France. The successful applicant will be funded -- including salary and (international) conference travel -- through a new French-German ANR-funded project. There will also be an opportunity to collaborate with a research team in Japan.
Lille is at the heart of Europe: 45 minutes from Bruxelles, 1 hour from Paris, 1 hour and half from London. This is an important university hub that hosts the annual International Cybersecurity Forum (FIC).
The start date is September 1st, but might possibly be postponed to October 1st.
The PhD position is about the formal proof in Coq for shallow-embedded imperative programs and their compilation into C (more details below).
Interested students should meet the following requirements:
If you are interested in applying for this opportunity please begin by contacting Gilles Grimaud, Samuel Hym and David Nowak. as soon as possible with the following information:
Summary:
The topic of this PhD offer is the formal proof in Coq for
shallow-embedded imperative programs and their compilation into C.
More precisely, the objective is to conceive and develop formal tools
to simplify code writing and proof of system software for low-end
devices.
Context:
The Coq proof assistant allows to prove properties of programs.
Its language, called Gallina, is purely functional. In the Pip project,
we have considered a monadic subset of C-like Gallina enough to
formally write an OS kernel.
Objectives:
A first objective of this PhD is to extend the monadic subset in order
to include further imperative features (such as loops, references or
exceptions) that will simplify code writing and proof of system
software for low-end devices. For security properties the monadic
Hoare logic used for Pip will have to be extended to deal with the new
imperative features. For functional properties, there are two possible
directions: either use the monadic Hoare logic or monadic equational
reasoning as developed in Monae. The relation with FreeSpec
should also be investigated.
A second objective is to automatically translate programs written in this monadic subset into an AST of the CompCert C verified compiler and to prove formally that this translation is correct, in the sense that properties proved on the monadic subset are also true of the generated C code.
The Vrije Universiteit Brussel is offering two PhD scholarships to join Prof Bart Bogaerts' research group on knowledge representation and reasoning
Particular topics of interest are:
Please find full details here.
A PhD position is available on automated reasoning in separation logic at the laboratories LIG and Verimag in Grenoble (France). More details on the subject and on how to apply are given here.
There is currently a PhD position available at Radboud University Nijmegen (the Netherlands) in the topic Higher-order Term Rewriting for Program Equivalence. The position is for four years, and comes with a competitive salary and very attractive employment conditions.
Interested students who either already hold a Masters' degree in computer science, mathematics, or a related area, or who will complete such a degree before September, are encouraged to apply. The initial application deadline is 20 June, but will be extended if no suitable candidate is found by that time.
The project
As a PhD candidate, you will conduct research into higher-order term rewriting systems with logical constraints. This project brings together two different areas of theoretical computer science: higher-order term rewriting and program equivalence analysis.
Term rewriting is a formal system that can be used to specify algorithms. Its simple, rigorous definition makes it very suitable for formal analysis, and as a result, its properties are well studied. Higher-order term rewriting extends standard term rewriting with anonymous functions and binders as in the lambda-calculus, thus providing a highly liberal class of systems.
Term rewriting can be combined with a logical theory and logical constraints; for example, integer numbers and conditions such as x >= 1 /\ y != x. With this approach, it Is possible to model programs in common programming languages; higher-order term rewriting systems in particular offer a natural model to analyse functional and object-oriented programming languages.
Program equivalence analysis is the study of whether two systems of program code have the same result, given the same input. This is a challenging field with many applications both in business practice and in other areas of computing science.
In this project, your task will be to develop techniques for program equivalence analysis, by analysing in particular higher-order term rewriting systems with logical constraints, which encode realistic programs. The majority of the project is the development of theory, but since it is a goal to develop automatable techniques, you will also implement some of your techniques in a prototype analysis tool.
You will be supervised by Dr Cynthia Kop. If you wish to learn more, feel free to send an e-mail.
Work environment
Strategically located in Europe, Radboud University is one of the leading academic communities in the Netherlands. It is a place with a personal touch, where top-notch education and research take place on a beautiful green campus, in modern buildings with state-of-the-art facilities.
The position is available in the Software Science group of the Institute for Computing and Information Sciences (iCIS) at Radboud University. Research at iCIS focuses on software science, digital security and data science. During recent evaluations, iCIS has been consistently ranked as the No. 1 Computing Science department in the Netherlands. Evaluation committees praised our flat and open organisational structure, our ability to attract external funding, our strong ties to other disciplines, and our solid contacts with government and industrial partners. The Software Science group is well known for its contributions to the mathematical foundations of software, formal methods, and functional programming.
What we expect from you
What we have to offer
How to apply
Submit a motivation letter, your CV, and a list of courses taken and grades obtained by e-mail (you will receive a notification confirming when it has arrived).
The Institute of Information Security at University of Stuttgart offers a fully-funded Postdoc position.
The successful candidate is expected to work on tool-supported formal analysis of cryptographic protocols and web applications building, among others, on our work published at EuroS&P 2021, S&P 2019, CSF 2017, CCS 2016, CCS 2015, ESORICS 2015, and S&P 2014. One goal is to provide tool-supported security analysis based on DY* for our web infrastructure model (WIM).
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). 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. Knowledge in one or more of the following fields is an asset:
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" and a single PDF file containing the following documents to Prof. Dr. Ralf Küster:
The deadline for applications is July 4th, 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.
We are looking for a PhD candidate for a 4-year project on Formal Methods for Embedded Systems, as part of SAVES (ScAlable Verification of industrial Embedded control Systems), a collaboration with the University of Münster (WWU Münster). You will be working on the SAVES project, carried out in collaboration with prof. dr. Paula Herber (University of Twente / WWU Münster).
The overall goal of SAVES is to investigate methods and tools to establish correctness of embedded systems. With trends such as Industry 4.0, the internet of things, and autonomous driving, the complexity of embedded systems is steadily increasing. A prerequisite to ensure the correct functioning of industrial embedded systems under all circumstances is a clear understanding of the models and languages that are used in the development process. Formal methods provide a basis to make the development process systematic, well-defined, and automated. However, for many industrially relevant languages and models, the semantics are only informally defined. Together with the limited scalability of formal design and verification techniques, this makes the formal verification of industrial embedded control systems a difficult challenge, which can not be solved satisfactory with currently available methods and tools. At the same time, we see that in the area of deductive program verification, powerful techniques and tools have been developed to reason about software with unbounded parameters, for example the VerCors tool suite. In this project, we will extend these techniques with concepts to cope with heterogeneity, concurrency, and real-time to make them suitable for industrial embedded systems.
The PhD candidate hired at the University of Twente will be supervised by Marieke Huisman and Paula Herber and will work on extensions of the methods and tools developed in the FMT group for embedded systems, in close collaboration with the Embedded Systems group in Münster.
For further information about the group, see here. For further information about the project, see here.
Your Profile
Our Offer The terms of employment are in accordance with the Dutch Collective Labour Agreement for Universities (CAO) and include:
Information and Application
Are you interested in this position? Please send your application via this link before 5th of July and include:
The deadline of application is July 5, 2021 or until the position is filled. Starting date of the position is as soon as possible, or to be discussed.
For further information, you can contact Prof.dr.ir. Paula Herber or Prof.dr. Marieke Huisman
Department
In the Formal Methods and Tools (FMT) research group, formal techniques and tools are developed and used as a means to support the development of software. Our central goal is to increase the reliability of the software that we rely on, as individuals and as society. We primarily target complex concurrent ICT systems, embedded in a technological context or in a distributed environment.
The FMT group is part of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente. The FMT group also participates in the Digital Systems Institute (DSI).
Our institute was ranked first at the most recent research national assessment.
Organization
The faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) uses mathematics, electronics and computer technology to contribute to the development of Information and Communication Technology (ICT). With ICT present in almost every device and product we use nowadays, we embrace our role as contributors to a broad range of societal activities and as pioneers of tomorrow's digital society. As part of a people-first tech university that aims to shape society, individuals and connections, our faculty works together intensively with industrial partners and researchers in the Netherlands and abroad, and conducts extensive research for external commissioning parties and funders. Our research has a high profile both in the Netherlands and internationally. It has been accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre and Digital Society Institute.
As an employer, the EEMCS Faculty offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With our Faculty, you will be part of a leading tech university that is changing our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customizable conditions.
University of Twente (UT)
University of Twente (UT) has entered the new decade with an ambitious, new vision, mission and strategy. As ‘the ultimate people-first university of technology' we are rapidly expanding on our High Tech Human Touch philosophy and the unique role it affords us in society. Everything we do is aimed at maximum impact on people, society and connections through the sustainable utilisation of science and technology. We want to contribute to the development of a fair, digital and sustainable society through our open, inclusive and entrepreneurial attitude. This attitude permeates everything we do and is present in every one of UT's departments and faculties. Building on our rich legacy in merging technical and social sciences, we focus on five distinguishing research domains: Improving healthcare by personalised technologies; Creating intelligent manufacturing systems; Shaping our world with smart materials; Engineering our digital society; and Engineering for a resilient world.
As an employer, University of Twente offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With us, you will be part of a leading tech university that is changing our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customisable conditions.
The Logic Group at the University of Milan is thrilled to advertise a postdoc position (two years, renewable) within the project "Logical Foundations of AI".
The project will be developed within a research line contributing to bridging the gap between statistical methodologies at the basis of (supervised, unsupervised) Machine Learning and Logic in the development of AI.
We aim to develop Logics for Reasoning under Uncertainty and with limited resources to analyse and check transparency and trustworthiness of AI systems. Properties of interest include but are not limited to: Causality, Safety and Fairness.
The selected candidate will join a thriving research group based at the Department of Philosophy at the University of Milan, and will be working under the joint supervision of Marcello D'Agostino and Giuseppe Primiero (check out our members page for more information about our group and research interests). They will be expected to contribute to the activities of the Logic Group, and to present and publish their results at high-standard conferences and journals.
The ideal applicant will hold a Ph.D. in Logic, obtained either within a philosophy, mathematics or computer science programme. The candidate is also required to have good basic knowledge of one or more of the following areas: Foundations of Resource-Bounded Logics; Epistemic and Non-Monotonic Logics; Logics of Uncertainty and Probabilistic Logics; Temporal Logics; Proof Theory; Verification (both model-checking and automated theorem proving).
For more information and link to the online application form, see here and here.
Feel free to get in touch with Giuseppe Primiero should you have any questions.
The Department of Information and Computing Sciences of Utrecht University is looking for a PhD student who will work on temporal logic for intention revision. The PhD student will be part of the Intelligent Systems group, led by Professor Mehdi Dastani, who will also be your supervisor along with Dr. Natasha Alechina and Dr. Dragan Doder.
The application deadline is 1 July 2021.
Application submissions and the details about the offer are here.
If you have any questions about this position, please contact Dr. Dragan Doder.
A postdoc position is now available at the Technische Universität Wien (Vienna, Austria) within the project "Identities in polymorphism algebras" of the Austrian Science Fund, held by Michael Pinsker.
The starting date is flexible, but should be somewhen this year. The duration of the position is one year, with possible prolongation should further funding become available. The yearly gross salary will be approximately 55.242,50 EUR, and there is generous additional travel support.
Requirements for the applicant are a clear commitment to science and interest in (some of) the topics of the project: universal algebra, model theory (homogeneous structures), Ramsey theory, constraint satisfaction.
Applications should be sent in electronic form directly to Michael Pinsker, and include
For full consideration, please apply before July 15th. Informal inquires by email are encouraged.
Follow the links for more information about the institute and the principal investigator:
Ph.D. position at the Informatics Department of the University of Bergen
We invite highly motivated applicants interested in carrying out foundational and/or applied research in knowledge representation, ontologies, and machine learning. The starting date can be in July or in December 2021.
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!)
The annual meeting of Ph.D. students: see here.
For more information, contact Ana Ozaki.
The VCLA invites applications for the Helmut Veith Stipend from motivated and outstanding female master's students who plan to pursue one of the programs in Computer Science at TU Wien taught in English in one of the following semesters:
Helmut Veith Stipend
The Helmut Veith Stipend is awarded annually to exceptionally talented and motivated female students in the field of computer science who pursue (or plan to pursue) one of the master's programs in Computer Science at TU Wien taught in English and have (or have the interest to develop) a solid mathematical and technical background in at least one of the areas in which Austrian scientist Helmut Veith worked.
The Helmut Veith Stipend is dedicated to the memory of Helmut Veith (1971-2016), an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. The Helmut Veith Stipend's fund is set up by the TU Wien (Vienna University of Technology), the Wolfgang Pauli Institute, and the colleagues and friends of the late Prof. Veith.
Award Students who are awarded the Helmut Veith Stipend receive:
Eligibility
Conditions
Application Process
Students are required to submit the following documents:
A certified translation needs to be provided for documents that are not in German or English. Your application must be submitted electronically to this email address with the subject "Application" as a single PDF document. The name of the PDF file needs to be "document.pdf"
Application Deadline
The annual deadline for applications is November 30.
Questions?
Further Information on the Stipend can be found here.
Please do not hesitate to contact the master's email address for more information.
A Gentle Invitation into Theorem Proving towards Formal Hardware Verification
What is the nature of human reasoning and problem solving? How can machines exploit the known skills of problems solving to solve new problems automatically? Is it possible to work out general patterns of discovery and reasoning, such that machines can develop new methods and systems? We try to answer these problems and shrink the gap between machine learning and human wisdom.
Mathematical discovery and reasoning is considered the most creative activity of human wisdom. Mathematicians have been investigating the nature of human reasoning and problem solving since classical Greece. Even if the development of interactive theorem provers provides rigorous tools for people to formalise mathematics and to verify hardware and software designs, there is still a big gap between human reasoning and mechanical theorem proving: precious human intelligence is wasted on proving tedious and trivial lemmas, which are indispensable for machines to check the correctness and the integrity of a proof, but are quite obvious for well-educated mathematicians or computer scientists. Even worse, it is hard to recover the original intentions by reading these mechanical proofs.
During the first year of this project, we will focus on developing an automated theorem prover towards human reasoning. Except the automation of proof strategies and skills, the main planned innovation is: deriving theories automatically. We want to investigate and implement such a mechanism: to generate conjectures from cases, concepts, proofs, and known theorems, then produce automatically human readable and machine checkable proofs. We also plan to design and implement the mechanism to discover and exploit morphisms between algebraic structures, so as to simplify proofs by making use of abstract domains. It doesn't mean that we don't need human interference; on the contrary, we want to make use of human experience whenever possible --- machines will learn from humans when, for example, they are stuck, the computation diverges, the solution space is too big, and so on. We believe that human skills of problem solving will enable machines to think like us and to make plausible reasoning at the end.
We will soon open the following positions for this project. There will be a competitive salary and benefits package in line with top tier industrial R&D positions in UK.
Work Location: Edinburgh UK
Also, we are recruiting interns on mathematics or computer science. We hope you can help create benchmarks or libraries, and improve the design and implementation of the tool. You are required to have a strong mathematical background. Basic programming skills of Haskell and Python are necessary. Knowledge of recursive functions, Lambda calculus, formal logics, type theory, or category theory is preferred.
You are very welcome to join us on this ambitious exploration journey.
Informal enquiries on details of the project and these positions can be made to: Dr. Wei Chen
Open PhD position in the department of Computer Science and Engineering at the University of Gothenburg/Chalmers, Sweden. The student will work on the project "Enabling Reactive Synthesis through Runtime Verification? with Professor Nir Piterman. The student will join a team supported by an ERC Consolidator grant and the Swedish research council (vetenskapsrådet (VR)).
Research scope: formal methods, reactive synthesis, runtime verification, automata, games, temporal logics
Apply here.
Read more what it would be like here
The successful candidate will work on the project ?Enabling Reactive Synthesis through Runtime Verification?. Reactive synthesis - automatic production of programs from high-level descriptions of their desired behavior - is emerging as a viable tool for the development of robots and reactive software. In high level, this is like telling a robot what you would like it to do and automatically planning how to do it. Runtime verification is an approach for following programs through their execution to ensure that they work correctly. The project will improve the capabilities of reactive synthesis techniques through exploiting methods that are used for runtime verification. This will include both theoretical and practical contributions.
More concretely, the work will include the study of temporal logic, automata, and two player games. Temporal logic is used for describing in a high level the required behavior of a program, automata are used as an algorithmic tool for manipulation of logic formulae, and two-player games enable to consider strategies and programs. We will study these formalisms, analyze their properties, devise algorithms to manipulate and translate between them, as well as implement tools that will show the applicability of the developed techniques.
The aim of the doctoral (third-cycle) education is to acquire the knowledge and skills necessary to conduct independent research within computer science, and to contribute to the development of knowledge by writing a scholarly thesis.
PhD (third-cycle) education is through a fixed-term employment contract for 5 years. During these 5 years, most of the student?s time will be devoted to their research. They will also be assisting the department?s education by working 20% of their time on a teaching or supporting role. The 20% support component may be concentrated in certain parts of the year according to department?s needs (in consultation with the student). In addition, the student will have to undertake 60 Higher Education Credits in courses enriching their knowledge in computer science, supporting their research, and gaining general (scientific) skills.
Postdoc positions are available at the Dept. of Computing Science at Umea University (Umea, Sweden), within the research group on "Artificial Intelligence for Data Management" led by prof. Diego Calvanese. (This is part of a larger call aimed at filling in total 4 PhD and 4 Postdoc positions.)
We invite highly motivated applicants interested in carrying out foundational and/or applied research in the context of flexible and efficient management of large amounts of richly structured data, by relying on semantic technologies and (virtual) knowledge graphs. The research in the "AI for Data Management" group touches and combines the areas of:
The research initiative is part of the Wallenberg AI, Autonomous Systems and Software Program (WASP), Sweden's largest individual research program ever, a major national initiative for strategically motivated basic research, education and faculty recruitment, addressing research on artificial intelligence and autonomous systems.
The Postdoc positions are for 2 years, but funding is already available to extend them for further two years. Additional funding is available for travel.
For more details and for applying, see here. Application deadline is 30 June 2021.
There were no comments concerning the plans for revival of the Association of Automated Reasoning, following their publication in the last AAR newsletter issue. This means that the proposed changes will be implemented at some point. Currently, the new bylaws are under construction.