Editor's Warning
Due to the COVID-19 pandemic, it is likely that the information in the newsletter won't stay up to date for long. If you are interested in an event or a position, carefully check the data on the corresponding website or with the organisers.
In this column, you will be treated to aspects of group theory, where, as a reminder, the term group is used by mathematicians for a set that satisfies a set of axioms that I give almost immediately. In a group, the function f denotes product (multiplication), the function g denotes inverse, the symbol e denotes the identity, and the function h denotes commutator whose definition i shall also give.
f(e,x) = x. % left identity.
f(x,e) = x. % right identity.
f(g(x),x) = e. % left inverse.
f(x,g(x)) = e. % right inverse.
f(f(x,y),z) = f(x,f(y,z)). % associativity of product (multiplication).
h(x,y) = f(x,f(y,f(g(x),g(y)))). % definition of commutator.
Levi's theorem asserts the equivalence of two of the following three properties, namely properties 1 and 3.
h(h(x,y),z) = h(x,h(y,z)). % commutators have the property of being associative, property 1.
h(f(x,y),z) = f(h(x,z),h(y,z)). % commutators have the property of distributing over product, property 2.
f(h(x,y),z) = f(z,h(x,y)). % commutators have the property of being nilpotent of class 2, property 3.
The second property, one I referred to as property 2, is not part of Levi's theorem; this second property can be proved equivalent to either property 1 or property 3, each of which was just given.
Given the axioms you now have, my focus now is on proof length -- in particular, finding shorter proofs. Proof length, by definition in OTTER, is the number of deduced steps, regardless of which inference rule OTTER is applying. What constitutes a shorter proof? For our purposes, a shorter proof refers to a proof in which the number of deduced steps is fewer than the number of steps in the proof currently in focus. (Demodulators, shown in OTTER by a series of numbers, each referring to the clause being used as a demodulator, are not counted in the length of the proof that is offered.)
Why are shorter proofs interesting? One reason is that they are more elegant. (Arguably, other features, such as the avoidance of some lemma or the avoidance of deduced steps whose length is greater than one wishes, can also make a proof more elegant.) Another reason is that short proofs can save space in a published article or in an article submitted for publication. I once reduced a proof that was over nineteen pages long, before it was submitted for publication, to one that was just three pages long when submitted for publication. (The theorem under study and its proof were published by three authors, in alphabetic order, William McCune, R. Padmanabhan, and Robert Veroff. The aforementioned McCune, cited for his various achievement with his automated reasoning program called OTTER, also found a new single axiom for lattice theory, an axiom I present later.
How do you shorten a proof? Various techniques can be used. I will discuss a few here.
One technique involves finding, within a so-called total proof, subproofs of a key equation or formula. The so-called total proof is the real goal of the search, is the focus of the task under consideration. For example, you might be trying to prove that, from a given equation or formula in some area of mathematics or logic, such as lattice theory, you can deduce what is called a basis. In lattice theory, the more familiar basis is a set of six equations that is so powerful that any theorem of lattice theory can be deduced from the more familiar set of six equations, but, occasionally, the less familiar set of four equations is the target. (After I present the aforementioned McCune's single axiom for lattice theory, I shall present the more familiar 6-basis and then present the less familiar 4-basis.)
In the technique under discussion, the plan is to find a subproof to be used with the intention of extending the subproof to a total proof of the theorem in focus, a total proof that is shorter than that which you had in hand or had heard of or read in some book or paper. In my research, I often do find a shorter proof of the theorem in focus. However, sometimes in my research the use of the new subproof, if I find such, leads to a longer proof of the theorem in focus. I used this technique, called cramming -- which, for McCune's reasoning program OTTER, means adding proof steps to the set of support -- in tackling one of the challenges I issue in this column regarding the axioms I gave earlier, namely, to find from those axioms a proof of property 2 from property 3. I had in hand a proof of length 91, and among my experiments I found (or, rather, William McCune's automated reasoning program found) two subproofs, one of length 22 and the other of length 12. Substituting these subproofs separately into the original proof which, for McCune's OTTER means adding the steps of either subproof to the set of support, gave me two total proofs, the first of length 91 and the second of length 93. Yes, the shorter subproof -- 10 steps shorter -- resulted in a longer total proof, which was indeed both surprising and disappointing. Not so surprising, I have encountered similar results earlier in my research. Often, however, cramming leads to a shorter total proof of the theorem in focus. Because of what I have told you earlier in this column, I was again led to the following aphorism: shorter subproofs do not necessarily a shorter total proof make.
I have also used in my experiments a technique called ancestor subsumption, that McCune formulated for me many years ago in response to my interest in shorter proofs. Briefly it works in the following way. Assume that you have included set(ancestor_subsume), a command used by OTTER, in your input file, and that OTTER has deduced and retained a conclusion that I will call P. If a second proof of P is drawn, OTTER compares the two proof and retains the proof that is strictly shorter. Unfortunately, the aphorism about shorter subproofs applies also to ancestor subsumption.
Another way to find shorter proofs is to block the use of deduced steps, one at a time, that are present in a (total) proof found by the program and that you have in hand. I used this approach in 2015 when I was studying a single axiom by Meredith. By blocking the forty-eighth step of a 65-step proof that deduced the Lukasiewicz three-axiom system for classical propositional calculus, I obtained a 59-step proof. for yet one more example: in my attempt to find for McCune a shorter proof in lattice theory that derives from his new single axiom the aforementioned less familiar 4-basis that I present later, I successfully used cramming, ancestor subsumption, and the technique of blocking steps one at a time in a proof McCune had in hand in 2002, a proof that has length 50. I used the cited techniques in 2018 to obtain a 40-step proof that derives from his single axiom the less familiar 4-basis. (I now present McCune's new single axiom for lattice theory, the more familiar 6-basis, and, finally, the less familiar 4-basis.
(((y v x)^x) v (((z^ (x v x)) v (u^x))^v))^ (w v ((v6 v x)^ (x v v7))) = x
y ^ x = x ^ y
(y ^ x) ^ z = y ^ (x ^ z)
y ^ (y v x) = y
y v x = x v y
(y v x) v z = y v (x v z)
y v (y ^ x) = y
y v x = x v y
(x v y) v z = x v (y v z)
x ^ (x v y) = x
x v (x ^ y) = x
Challenges
So far as I know, no single approach to finding shorter proofs always succeeds.
That is why I find experimentation a delight!
To help you share my enthusiasm, I offer six challenges for you to attempt to meet, challenges involving properties 1, 2, and 3 for commutators.
The definition of a commutator was given rather early in this column.
In each case, you are asked to find a demodulation-free forward proof shorter than that which I now have in hand, proofs I obtained with OTTER.
I know of no shorter proof than that in focus in the six challenges.
(Recall that a forward proof is a proof that reasons forward from the axioms and hypotheses that present the problem, using the denial of the goal only as a so-called stopping point, to yield unit conflict or to yield the empty clause.
A demodulation-free proof is a proof in which demodulation plays no role in the deduction of the needed equations or formulas; therefore, a Knuth-Bendix approach is not the approach you will find of value in attempting to meet the challenges I give.)
Preamble
These notes were prepared following a request of the organizers of the Tableaux
2017 conference in Brasilia which celebrated the 25 th anniversary of Tableaux.
They were on display for the conference attendees, but have not been published otherwise. When I asked the editor of the AAR newsletter, Sophie Tourret, whether she thought my notes could be of interest to the AAR community,
she kindly encouraged me. The text below is a lightly edited version of the
one I prepared for the conference in Brazil.
* * *
While you see a chance take it
— Steve Winwood, 1980
* * *
In the Fall of 1991 I started writing up my Ph.D. thesis at the Computer Science Department of Karlsruhe University (now Karlsruhe Institute of Technology). It must have been around that time when I was approached by two somewhat more senior colleagues: Bertram Fronhöfer and Thomas Käufl. They asked whether I would be interested to co-organize a workshop dedicated to tableaux and related proof methods. Bertram was a senior Postdoc at TU Munich at the time and Thomas a postdoc in another research group in Karlsruhe. They felt that tableau calculi did’t quite get the attention they deserve at existing scientific meetings. I was not so sure about that myself (having had two papers about tableaux at CADE 1992), but I readily agreed that, in any case, it was an excellent idea to hold a dedicated meeting on tableaux and friends. After all, there was much research on tableaux methods in AI, as well as a lot of work by proof theorists, specifically on non-classical logics, that would never be submitted to CADE.
It was quite obvious that Bertram and Thomas were looking for a “junior partner” who would do some of the ground work. But since I could participate in the scientific aspects as well, this was just fine with me. Besides, it was generous of them to ask me in the first place. So we started to compose a CfP for a small, informal workshop. And we had just the right location: a typical, cosy Black Forest hotel in the tiny village of Lautenbach. Unreachable by public transport, but an affordable place, offering warm, Southern-German hospitality. We booked it for 18–20 March, 1992. They had room for at least 30 people—plenty!
In 1991 the World Wide Web was gestating, but it had not been born yet. There was email, there were ftp servers, and there was a social network: Usenet newsgroups. I was kind of active in groups such as comp.ai, where you could discuss with luminaries like John McCarthy (I will never forget his signature: “He who refuses to do arithmetic is doomed to talk nonsense”). It was also ok to post the occasional CfP—so that’s what I did. And I spammed every person and every mailing list in my addressbook with the Tableaux CfP.
A few days before the deadline, first submissions started to arrive in the mail (physical, of course!). And they just didn’t stop coming. In the end, we had over 30 of them! But there was a little problem: we had no programme committee, it was just us three organizers, and a quite short deadline for notification, too. What to do? Luckily, there was an obvious solution: we simply accepted everything. In the preface of the proceedings we spun this into a virtue: “We thought it was desirable to interchange ideas and experiences between a broad audience working on classical and non classical logics. A refereeing process would have contradicted this purpose. Thus every talk was accepted . . . ”. Translation: “We simply couldn’t be bothered to read 30 papers in four weeks, so we decided to take the easiest path and we’ll just keep our fingers crossed that we don’t end up with too much nonsense.” Young colleague—beware of pompous bullshit!
So far, so good. The hotel was informed that we need all their available rooms. Registration was opened. More rooms in the village were allocated. More registrations. Are there perhaps any private rooms in Lautenbach? In the end we had, I believe around 50 participants. And they came from all over the world, not mainly from Germany and a few neighbouring countries, as thought originally. But there is no public transport to Lautenbach. Too far for a taxi ride, too. So we provided travel instructions: please be at Karlsruhe central train station on 17. March, 1992 between 3pm and 5pm. There will be a (single) shuttle bus to bring you to Lautenbach. Can this work? — It did! I can still picture myself, standing in the arrival hall of Karlsruhe station, holding up a placard with Tableaux Workshop written on it, getting curious glances from passers-by. But then Charles Morgan from Canada strolled towards me, Don Loveland from the USA, Tadashi Araragi from Japan, and, unbelievably, Rod Girle, Rajeev Goré, and Mark Grundy from Australia who had been traveling for more than 24 hours.
It was an exciting meeting, crammed with talks and discussions. In the evenings the Kirsch (distilled cherry schnaps) flowed freely. And I was (co-)organizing my first meeting: I chaired a session for the first time in my life. Established researchers spoke to me with respect—while I still had to defend my thesis six weeks later (in retrospect, it seems I had not been bothered by this at all).
Quite unexpectedly, a community had been formed. Everyone present agreed that we must repeat the workshop. But why did it happen at all in this form? Of course, at that time, there were far fewer conferences and workshops to compete with than nowadays. Perhaps people with a background in proof theory appreciated the opportunity to mingle with computer scientists. And I got a little bit carried away when advertising it. But honestly, I cannot rationally explain, why so many people came to an obscure first-time workshop to an obscure place, organized by (at least for my part) obscure people. Perhaps, one day, there will be a Star Trek episode with a time warp story that explains it all . . .
An attempt to explain why Tableaux persisted for so long might be easier: I believe this has to do with a few decisions that were initially taken —quite randomly— and quickly established themselves as a tradition that set Tableaux slightly apart from other meetings which helped to establish a community: the main organizers are also PC members and some or all of them are the PC co-chair(s); a tendency to go to slightly off-the-grid places that offer nice surroundings and decent food; from the start, Tableaux was an open, inclusive event, intended to bring together researchers with varying interests: proof theorists and implementors, classical and non-classical logics; and finally: Tableaux was initiated and driven by non-established people. Of the editors of the first three proceedings, only two had tenured positions at the time and not a single one was in a senior position (associate or full professor). It must also be said that the more senior figures in the background, Peter Deussen in Thomas Käufl’s case, Peter Schmitt in mine and Joachim Posegga’s case, Dov Gabbay in Marcello D’Agostino’s and Krysia Broda’s case, Harald Ganzinger in David Basin’s case, while being generous with their advice and encouragment, did not impose themselves on us—we had free reign.
In hindsight, I think it was the combination of a slightly non-standard setup, of topical inclusiveness, and giving young talents a chance that made it possible for Tableaux to survive for so long while competing with an ever growing number of meetings and for an ever decreasing amount of available time of those who come to them.
In any case, during the Lautenbach workshop, Camilla Schwind kindly offered to host the next workshop in Marseille. In true Tableaux spirit, the meeting was (of course!) not actually in Marseille, but in the Centre International de Rencontres Mathématiques, in the middle of the stunning coastal Calanques landscape. Would Camilla have held up her offer, if she had known then that over one hundred people would come to Marseille in 1993? Who knows, but then none of us had any idea this would happen. At least, this time we had a proper programme committee. In the end, there were 28 papers in the 250 page proceedings which were published as a Technical Report of Max-Planck-Institute Saarbrücken that also generously paid for the printing. Invited speakers were Mark Stickel as well as Melvin Fitting, a legend in tableau calculi even then.
In this situation, many people asked a completely reasonable question: why is Tableaux a workshop and not a conference? After all, we had the size, the peer review system, the internationality, the quality. The only missing piece were proceedings with an international publisher. But would we then not loose some of our openness? Would people still submit to Tableaux? Hitherto the proceedings had been Technical Reports, so Tableaux papers could be resubmitted to a “proper” conference afterwards. It was a difficult step to take which only in hindsight seems obvious. For the moment, it was decided to invite selected papers to a special issue of the Journal of Automated Reasoning. This was engineered by Graham Wrightson, who was in the Editorial Board. A double special issue of JAR with 12 articles dedicated to Automated Reasoning with Analytic Tableaux appeared in Oct/Dec 1994.
Tableaux 1994 was held in Abingdon, a small town not far from Oxford (you see the pattern?) and organized mainly by Krysia Broda and Marcello D’Agostino from Imperial College, London. It was the last Tableaux with informal proceedings. We had outgrown the workshop format. In 1995, Tableaux had internationally published proceedings in Springer’s LNAI series which it has continued to do ever since. The informal, friendly spirit in which Tableaux meetings were being organized prevailed, however. Only in 2000 we formed a proper Steering Committee. This was necessary to prepare the first IJCAR held in Siena in 2001. I became the first SC president and served in that role until 2003.
* * *
Epilogue
Looking back 27 years—there was an unexpected, narrow window of opportunity. We grabbed it and did the best we could. I guess this is my message
in this note for younger colleagues: take your chance when it comes around,
because you might not see it a second time.
I am happy about my role in setting up Tableaux back then and I am even happier to see that the conference is still going strong after all this time. May it prosper!
* * *
Acknowledgments
I am very much indebted to all people mentioned above, most of all to Bertram
Fronhöfer and the late Thomas Käufl. I want to specifically thank Peter Schmitt
who gave me both freedom and support when I was a PhD student in his
group. Cláudia Nalon and her organization team had the idea to commemorate 25 Years of Tableaux at the conference in Brasilia. Without her gentle
prompting these notes would never have been written. Sophie Tourret encouraged me to submit this text to the AAR Newsletter. — Thank you all!
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 three CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2020.
The current members of the board of trustees are (in alphabetical order):
The terms of Jürgen Giesl, Marijn Heule, and Andrew Reynolds end. Marijn Heule and Andrew Reynolds may be nominated for a second term, whereas Jürgen Giesl has already served two consecutive terms and cannot be nominated this year.
The term of office of Nicolas Peltier as IJCAR 2020 programme chair ends after the IJCAR conference; he will be replaced by one of the programme chairs of CADE-28. As outgoing ex-officio trustee, Nicolas Peltier is eligible to be nominated as elected trustee.
In summary, we are seeking to elect three trustees.
Nominees must be AAR members. Nominations can be made by any CADE member, either by e-mail or in person at the CADE business meeting at IJCAR 2020; since nominators must be CADE members, they must have participated at at least one of the CADE or IJCAR conferences in the years 2017-2020. 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 Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to:
A nomination is required for consideration for the Herbrand Award. Nominations can be submitted via email to the President of CADE Inc. The deadline for nominations to be considered for the Herbrand Award 2020 is:
31 May 2020
The Herbrand Award 2020 will announced virtually at IJCAR 2020, but it is planned to have an additional ceremony at CADE~28 in 2021. Nominations pending from previous years must be resubmitted in order to be considered.
For more details, please check the Herbrand Award webpage.
Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contributions (including the relationship to CADE), along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to
Christoph Weidenbach, President of CADE Inc.with copies to
Philipp Rümmer, Secretary of AAR and CADE Inc.
Due to the current health situation, the submission deadline for nominations has been postponed to July, 1.
PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1 January 2018 and 31 December 2019 are eligible for nomination for the award.
See the call for nomination in the previous issue of the AAR newsletter.
Informatics Europe proudly announces the fifth Minerva Informatics Equality Award devoted to initiatives seeking to encourage and support the careers of women in Informatics research and education. The fifth of this annual award will be presented in October 2020 and is sponsored by Google.
The Informatics Europe Minerva Informatics Equality Award recognises best practices in Departments or Faculties of European Universities or Research Institutes and Labs that have been demonstrated to have a positive impact for women. On a three-year cycle the award will focus each year on a different stage of the career pipeline:
The 2020 Award is devoted to gender equality initiatives and policies supporting the transition of female PhD and postdoctoral researchers into faculty positions.
The Award seeks to celebrate successful initiatives that have had a measurable impact on the careers of women within the institution. Such initiatives can serve as exemplars of best practices within the community, with the potential to be widely adopted by other institutions. Submissions will need to demonstrate the impact that has been achieved.
For 2020 examples of impact could include an improved career development and better agreements on career planning for female PhD students and postdocs as recorded in objective surveys of staff experience, and increasing numbers of female faculty.
The Award carries a prize of EUR 5,000.
The Award will be given to a Department or Faculty to be used for further work on promoting gender equality. To be eligible, institutions must be located in one of the member or candidate member countries of the Council of Europe, or Israel. Institutions associated with members of the WIRE Working Group and of the Award committee are not eligible. The Award committee will review and evaluate each proposal. It reserves the right to split the prize between different applications. Moreover, noteworthy runners up may also be included as exemplars of best practice in future Informatics Europe publications.
Deadlines:
The Association for Computing Machinery recently chartered a Presidential Task Force to gather and disseminate guidance on best practices for virtual conferences, aimed at the many conference organizers moving their events online right now.
The task force report, Virtual Conferences: A Guide to Best Practices, is now available on the ACM web site It offers a comprehensive survey of issues, organizational strategies, and technology platforms for successful virtual meetings.
We hope that you and others in your field will find this report useful. If you do, we would love to hear about it! And naturally if you have any suggestions for improvement, we would love to hear those too; the PDF document linked above includes a pointer to a live Google Doc where you can leave suggestions and comments if you like. If you have recently organized a virtual conference or are organizing one now, we would especially like to include your experiences (how you organized it, how it went, what people thought, a summary of any post-conference survey results, your advice for future conferences, etc.) and add it (or better yet a pointer to it) to the appendix that we’ve provided for such experience reports.
Due to the ongoing Covid-19 pandemic, IJCAR 2020 will be held as a virtual meeting, as will the co-located FSCD 2020 conference and the associated workshops.
The current state of IJCAR and FSCD's satellite events is detailed below. There have been many deadline extensions and there will certainly be more to come so check it out on the web sites .
June 29-30
June 29
June 30
July 5-6
July 5
The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-J10 will be held on the 2nd July 2020, during the 10th International Joint Conference on Automated Reasoning.
CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of:
The competition organizer is Geoff Sutcliffe. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. Further details and registration information are available here.
Registration of systems for CASC-J10 is now invited. System registration closes on 5th June. Please register early so that adequate resources can be allocated.
DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW!
CoCo 2020 will run live during IWC 2020, the 9th International Workshop on Confluence, which is held in Paris on June 30 as part of the Paris Nord Summer of LoVe.
Problems submitted by May 15, 2020 (via the COPS web interface) will be considered for CoCo 2020. In addition, there is the option to submit secret problems after the tool submission deadline.
All competition categories in CoCo 2019 will run in 2020. Further details can be found here.
Synopsis
The interest expressed for the workshop was such that the PC
decided to publish a proceedings volume, in spite of our decision to
cancel the event after the IJCAR became a remote meeting.
Our proposal received the approval for publication on the part of EPTCS.
ThEdu'20 Scope:
Computer Theorem Proving is becoming a paradigm as well as a
technological base for a new generation of educational software in
science, technology, engineering and mathematics. The workshop brings
together experts in automated deduction with experts in education in
order to further clarify the shape of the new software generation and
to discuss existing systems.
Important Dates
Topics of interest include:
More information is available on the workshop's web page.
Together with the LPAR steering committee, the LPAR-23 organisers have decided to cancel LPAR-23 in Alicante, in May 2020. We will not organize LPAR-23 in May 2020 as an online conference either. Rather, we will "merge" LPAR-23 with LPAR-24, offering the authors of accepted LPAR-23 papers the possibility, if they wish, to present their work at LPAR-24 in Tobago, January 2021. Details on LPAR-24 will be announced in summer/fall 2020.
The EPiC proceedings of LPAR-23 will however be published in time, as planned in May 2020.
Due to the current medical situation related to the coronavirus COVID-19 outbreak, the Organizing Committee of CiE2020, in agreement with the CiE Steering Committee, has decided to hold the conference virtually, without a physical gathering.
The organizers are committed to recreate the usual CiE climate under the new conditions.
More information is available on the conference's web page.
In view of the chaotic situation in many places of the world due to the pandemic, we are sorry to inform you that we definitely will not be able to maintain the physical event of the MFPS and QPL 2020 conferences in Paris or, indeed, anywhere else in the world.
We are still working out the details of how to hold a virtual meeting. At a minimum, we plan to offer the opportunity to upload pre-recorded lectures to an online conference platform. More information on the concrete modalities (offline videos, forum, online discussion platform, etc) will be forthcoming.
Conference proceedings of the accepted papers will still be published as usual.
More information is available on the conference's web page.
Homotopy Type Theory is a new area at the intersection of mathematics and computer science, combining ideas from several well-established fields: logic and type theory, homotopy theory, and formalization of mathematics.
The HoTTEST Conference of 2020 is a week-long online meeting, building on our series of HoTT Electronic Seminar Talks (HoTTEST). The conference will feature 10 talks by leading experts in the area. Familiarity with Homotopy Type Theory will be assumed.
Invited speakers
More information is available on the conference's web page.
ATVA 2020 is the 18th in the ATVA series of symposia intended topromote research in theoretical and practical aspects of automatedanalysis, verification and synthesis in Asia by providing a forum forinteraction between the regional and international researchcommunities and industry in the field.
ATVA 2020 solicits high-quality submissions on, but not limited to,the following topics:
Important Dates
More information is available on the symposium's web page.
Foremost, the TIME 2020 organizing committee hopes you are all in good health!
We announce that TIME 2020, co-located with BOSK 2020, will allow for virtual attendance. Thus, the paper submission and the selection process will run just as expected, and physical participation in the symposium will not be a prerequisite for publication. Whether the symposium will allow also a physical attendance will be decided in the coming weeks together with the BOSK 2020 organizers. Reduced registration fees will be allowed for virtual participants. We thus warmly invite you all again to submit your papers to TIME 2020.
STAY SAFE!
Aims & Scope
Since 1994, the TIME International Symposium on Temporal Representation and Reasoning aims to bring together researchers in the area of temporal reasoning in Computer Science. TIME 2020 encompasses three tracks, but has a single program committee. The conference will be organized as a combination of technical paper presentations, keynote talks, and tutorials.
Tracks
Following a long-standing tradition, submission topics include (but are no limited to):
Important Dates
More information is available on the symposium's web page.
The PPDP 2020 symposium brings together researchers from the declarative programming communities, including those working in the functional, logic, answer-set, and constraint handling programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for analyzing, performing, specifying, and reasoning about computations, including mechanisms for concurrency, security, static analysis, and verification.
Submissions are invited on all topics related to declarative programming, from principles to practice, from foundations to applications. Topics of interest include, but are not limited to:
Important dates
More information is available on the symposium's web page.
Important Note:
We are continuously monitoring the COVID-19 situation
from local authorities and the World Health Organization. ICLP 2020 is
half a year away, and we are confident that COVID-19 emergency will pass
over and the conference will be held in September, as planned. And, if
necessary, alternative solutions, such as postponement, remote
presentations, etc will be looked into and identified.
Scope
Contributions are solicited in all areas of logic programming and related
areas, including but not restricted to:
Important Dates
More information is available on the conference's web page.
Static analysis is widely recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of Static Analysis Symposia has served as the primary venue for the presentation of theoretical, practical, and application advances in the area.
Topics
The technical program for SAS 2020 will consist of invited lectures
and presentations of refereed papers. Contributions are welcomed on
all aspects of static analysis, including, but not limited to:
Important Dates (updated)
More information is available on the symposium's web page.
The aim of the FMICS conference series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.
QONFEST 2020: FMICS 2020 is part of the QONFEST umbrella conference comprising also:
Virtual FMICS
Amid the recent COVID-19 situation, the organization committee decided that QONFEST 2020, including FMICS 2020, will be organized on-line. Accepted papers will be published as planned, by September 2020, but no physical meeting/presentations will take place. We plan that the authors will record their talks and discuss them with the conference participants online.
Topics
Topics of interest include (but are not limited to):
Important Dates
More information is available on the conference's web page.
We hope that by September the situation will improve and we will be able to have a traditional-style conference, otherwise alternative solutions will be available (e.g., remote presentations). The proceedings will be published independently of the conference format.
Scope
The aim of the LOPSTR series is to stimulate and promote international
research and collaboration on logic-based program development in any
language paradigm.
LOPSTR 2020 will be co-located with PPDP, WFLP and Microservices.
Topics
Topics of interest cover all aspects of logic-based program development
(including in domain-specific languages), all stages of the software
life cycle, and issues of both programming-in-the-small and
programming-in-the-large, including:
Important Dates
More information is available on the symposium's web page.
The aim of GandALF 2020 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-fertilisation.
Papers focused on formal methods are especially welcome. Authors are invited to submit original research or tool papers on all relevant topics in these areas. Papers discussing new ideas that are at an early stage of development are also welcome. The topics covered by the conference include, but are not limited to, the following:
Important Dates
More information is available on the symposium's web page.
In recent years, we have witnessed a proliferation of approaches that integrate several modelling, verification and simulation techniques, facilitating more versatile and efficient analysis of software-intensive systems. These approaches provide powerful support for the analysis of different functional and non-functional properties of the systems, complex interaction of components of different nature as well as validation of diverse aspects of system behaviour. The iFM conference series is a forum for discussing recent research advances in the development of integrated approaches to formal modelling and analysis. The conference covers all aspects of the design of integrated techniques, including language design, verification and validation, automated tool support and the use of such techniques in software engineering practice.
Areas of interest include but are not limited to:
COVID-19
Due to the disruptions caused by the COVID-19 pandemic, we have decided that iFM 2020 will not take place physically and will be replaced by a virtual event. However, the paper selection process will not be affected: an LNCS proceedings will be prepared as usual. We will announce the plans for how the virtual conference will take place in the following weeks (in time for the paper submission deadline).
Authors of all of accepted papers:
Important dates
More information is available on the conference's web page.
CILC (Italian Conference on Computational Logic) is the annual conference organized by GULP (Group of researchers and Users of Logic Programming). It will be co-located with the 36th International Conference on Logic Programming (ICLP 2020)
Since the first event of the series, which took place in Genoa in 1986, the annual GULP conference represents the main opportunity for users, researchers and developers working in the field of computational logic to meet and exchange ideas. Over the years the conference broadened its horizons from the specific field of logic programming to include declarative programming and applications in neighboring areas such as artificial intelligence and deductive databases.
The topics of interest include, but are not limited to, the following:
Important Dates - Tentative schedule
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.
POPL 2021 will welcome contributions from all members of the community. Independent of what will happen with global Covid-19 crisis and the complications of its aftermath, authors and other participants will be given the choice to participate in-person or remotely.
Scope
The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages. The symposium is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.
Important Dates:
More information is available on the symposium's web page.
We are continuously monitoring the COVID-19 situation from local authorities and the World Health Organization. KR 2020 is still 5 months away, and we are confident that COVID-19 emergency will pass over and the conference will be held in September, as planned. And, if necessary, alternative solutions, such as postponement, remote presentations, etc will be looked into and identified.
We invite submissions of abstracts of papers previously published in journals and conference proceedings for the Recent Published Research Track. The track is designed to provide a forum to discuss recent research on topics related to KR that may not be immediately familiar or easily accessible to the KR community. The track seeks papers that fall into one or both of the following two categories:
Important Dates
More information is available on the conference's web page.
The aim of the colloquium is to bring together practitioners and researchers from academia, industry and government to present research results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing. ICTAC also aims to promote research cooperation between developing and industrial countries. The proceedings will be published as a volume of Springer's LNCS series.
Concerning COVID-19
The Program Chairs and the Steering Committee of ICTAC 2020 are
closely following the situation regarding COVID-19 and will take
appropriate measures if and when needed, following the recommendations
of relevant national and international bodies, such as the World
Health Organization. These measure will be adapted to the actual
situation and may e.g., include the possibility of remote paper
presentations or a full electronic implementation of the conference.
Objectives and Scope
Established in 2004 by the International Institute for Software
Technology of the United Nations University (UNU-IIST), the ICTAC
conference series aims at bringing together researchers and
practitioners from academia, industry and government to present
research and exchange ideas and experience addressing challenges in
both theoretical aspects of computing and the exploitation of theory
through methods and tools for system development. ICTAC also aims to
promote research cooperation between developing and industrial
countries.
The topics of the conference include, but are not limited to:
Important Dates
More information is available on the colloquium'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.
News
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.
Because of the Covid-19 pandemic, ECAI 2020 has been rescheduled to August 29 - September 2, and SR 2020 will be held on the 29th of August.
Strategic reasoning is a key topic in multi-agent systems research. The extensive literature in the field includes a variety of logics used for modeling strategic ability. Results from the field are now being used in many exciting domains such as information system security, adaptive strategies for robot teams, and automatic players capable to outperform human experts. A common feature in all these application domains is the requirement for sound theoretical foundations and tools accounting for the strategies that artificial agents may adopt in the situation of conflict and cooperation.
The SR international workshop series aims at bringing together researchers working on different aspects of strategic reasoning in computer science, both from a theoretical and a practical point of view.
Topics of Interest:
The topics covered by SR include, but are not limited to, the following:
Important Dates:
More information is available on the workshop's web page.
The DL workshop is the major annual event of the description logic research community. It is the forum in which those interested in description logics, both from academia and industry, meet to discuss ideas, share information and compare experiences. The 33rd edition will be collocated with the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020 and the 18th International Workshop on Non-Monotonic Reasoning, NMR 2020.
Workshop Scope
We invite contributions on all aspects of description logics, including, but not limited to:
Important Dates
More information is available on the workshop's web page.
To make the behavior of knowledge-based systems comprehensible, they need to be able to explain their decisions. In principle, decisions based on logical reasoning are easy to explain since one can 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 since proofs and counter-models may be very large, and thus it may be hard to comprehend why they demonstrate a certain result. In automated deduction, the problem of explaining why a consequence does or does not follow from a given set of axioms has been considered for a long time. In knowledge representation and reasoning, efforts in this direction are more recent, and were usually restricted to certain sub-areas of KR.
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.
NMR is the premier forum for results in the area of nonmonotonic reasoning. Its aim is to bring together active researchers in this broad field within knowledge representation and reasoning (KRR), including belief revision, uncertain reasoning, reasoning about actions, planning, logic programming, preferences, argumentation, causality, and many other related topics including systems and applications.
NMR 2020 is co-located with KR 2020 and DL 2020. In particular, NMR 2020 will share a joint session with DL 2020.
As in previous editions, NMR 2020 aims to foster connections between the different subareas of nonmonotonic reasoning and provide a forum for emerging topics. We especially invite papers on systems and applications, as well as position papers and papers addressing benchmark issues. The workshop will be structured by topical sessions fitting to the scopes of accepted papers.
Important Dates
More information is available on the workshop's web page.
The international Workshop on Functional and (constraint) Logic Programming (WFLP) aims at bringing together researchers, students, and practitioners interested in functional programming, logic programming, and their integration. WFLP has a reputation for being a lively and friendly forum, and it is open for presenting and discussing work in progress, technical contributions, experience reports, experiments, reviews, and system descriptions.
The 28th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2020) will be organized by the University of Bologna, Italy, as part of Bologna Federated Conference on Programming Languages 2020 and it will be held entirely on-line due to the coronavirus pandemic.
Topics
The topics of interest cover all aspects of functional and logic
programming. They include (but are not limited to):
Important Dates
More information is available on the workshop's web page.
The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models.
Topics of interest for EXPRESS/SOS 2020 include, but are not limited to:
We especially welcome contributions bridging the gap between the above topics and neighbouring areas, such as, for instance:
Important Dates
More information is available on the workshop's web page.
Due to the ongoing Covid-19 pandemic, the Tenth Summer School and Formal Techniques and the First Formal Methods in the Field Bootcamp have been postponed until further notice. Registration will be closed for now and will reopen once the event has been rescheduled. If you have already registered, we will contact you when we have a new schedule.
Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the tenth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions.
The fifth international autumn school "Proof and Computation" will be held from 20th to 26th September 2020 in Fischbachau near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy.
Scope
Courses
Working Groups
There will be an opportunity to form ad-hoc groups working on specific
projects, but also to discuss in more general terms the vision of
constructing correct programs from proofs.
Applications
Graduate or PhD students and young postdoctoral researches are invited to
apply. Applications (e.g. a self-introduction including research interests
and motivation) should be sent to Chuangjie Xu.
Students are required to provide also a letter of recommendation, preferably from the thesis adviser.
Deadline for applications: 30 May 2020. Applicants will be notified by 20th June 2020.
Financial Support
Successful applicants will be offered **full-board accommodation** for
the days of the autumn school. There are NO funds, however, to reimburse
travel or further expenses, which successful applicants will have to
cover otherwise.
The workshop is supported by the Udo Keller Stiftung (Hamburg), the CID (Computing with Infinite Data) programme of the European Commission and a JSPS core-to-core project.
More information is available on the school's web page.
RW 2020 is part of "Declarative AI 2020: Rules, Reasoning, Decisions and Explanations" (DeclarativeAI 2020)
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. In 2020, the broad theme of the school is Declarative Artificial Intelligence.
As in the previous years, lectures in the summer school will be given by a distinguished group of expert lecturers.
Due to the current situation regarding the spread of the COVID-19 coronavirus, Declarative AI 2020 will be held as an ONLINE event.
Confirmed Lectures
Important Dates
More information is available on the school's web page.
The International School on Rewriting (ISR) is aimed at master and PhD students, researchers, and practitioners interested in the study of rewriting concepts and their applications. ISR has been initiated and is promoted by the IFIP Working Group 1.6 on Term Rewriting.
The plan was to hold ISR 2020 (this year) at UCM Madrid, organized by Narciso Marti Oliet. Due to the COVID-19 pandemic, this is impossible.
Narciso offered, and the Steering Committee strongly supports, to move that school to 2021 (next year) in the same place. All the scheduled speakers indicated that they will be available to teach their course in 2021.
This is a call for proposals for hosting and organizing ISR 2022.
The International School on Rewriting (ISR) is aimed at master and PhD students, researchers, and practitioners interested in the study of rewriting concepts and their applications. ISR has been initiated and is promoted by the IFIP Working Group 1.6 on Term Rewriting.
The proposals for ISR 2022 are to be sent to the ISR steering committee by Monday, June 1st, and to be presented at the upcoming meeting of the IFIP WG 1.6 (on-line meeting on or around June 30, co-located with FSCD 2020, details to be announced as they become available) The decision about hosting and organizing ISR 2021 will be taken by a vote of the IFIP WG 1.6 members present.
Information on ISR as bylaws and previous schools is available here.
A proposal for hosting and organizing ISR 2022 should address the following points:
If you consider presenting a proposal for organizing ISR 2022 or have any questions, please contact the chair of the ISR steering committee.
The deadline for submitting the finished proposal is June 1st, 2020.
In order to achieve geographic diversity, proposals to host ISR 2022 outside Europe will be prioritized.
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 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.
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:
Application Deadline
The annual deadline for applications is November 30th.
Questions?
Please do not hesitate to send an email.
There is currently a PhD position available at Radboud University Nijmegen (the Netherlands) in the area of Higher-Order Term Rewriting with Logical Constraints. The position is for four years, and comes with a competitive salary and very attractive employment conditions.
Interested students who either already hold a Master's degree in computer science, mathematics, or a related area, or who will complete such a degree before September, are encouraged to apply. The application deadline is 31 May.
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 analysis, and in particular analysis of functional programming languages. 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 λ-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; in particular, higher-order term rewriting systems offer a natural model to analyse functional programming languages.
In this project, your task will be to develop techniques to analyse properties of higher-order term rewriting systems with logical constraints, and apply these techniques towards program analysis. You can build on several existing approaches, but will have a lot of freedom to define your own direction.
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
You can apply here, or ask for more information by e-mail to Cynthia Kop.
Note that the deadline for applications is set at 31 May, and the project can start immediately when a PhD candidate is hired, or later in discussion (but no later than September).
Our Team
The BINary-level SECurity research group (BINSEC) is a dynamic team of 8 junior and 2 senior researchers. The group has frequent publications in top-tier Security, Formal Methods and SE conferences. We work in close collaboration with other French or international research teams, industrial partners and national agencies. The team is part of CEA, one of the best ranked research institution in the world, with an annual budget of €4.7 billion and about 16K staff members across France.
Our Work
The team has high-level expertise in several code analysis approaches, including binary-level formal methods, symbolic execution, abstract interpretation, SMT solving and fuzzing. We apply these techniques to improve the security of software at the binary level, covering notably continuous security analysis, code hardening and patching, advanced vulnerability detection, criticality assessment, backdoor detection, verification-oriented decompilation, malware analysis or binary-level formal verification. Additional information can be found here or here.
Your Mission
The goal of your postdoc will be to leverage recent advances in program analysis, software verification and/or machine learning to develop methods and tools supporting security analysis at the binary level. This includes (but is not limited to) vulnerability analysis, code hardening, reverse engineering and malware analysis. In particular, you will be strongly encouraged to explore innovative solutions combining both program analysis and machine learning.
You will get involved in EU or industry-funded projects, together with senior members of the group. You will be expected to solve challenging research problems, implement your solutions into evaluated prototypes, publish at top conferences and journals, mentor students and broadly participate to the scientific life of the group. All positions comprise theoretical work as well as prototyping (preferably in OCaml) and experimental evaluation. We recognize that postdocs may need to spend a fraction of their time applying for permanent positions and we will support you in advancing your career.
Job Requirements
Successful candidates should have a Ph.D. in Computer Science (or be near completion), they should be proficient in English and have excellent programming skills. We are mainly looking for applicants with an excellent research track record in program analysis, formal methods, software security and/or machine learning. However, candidates with background in programming languages, compilation, empirical software engineering, architecture or system may also be considered.
Hiring Procedure
Interested applicants should send their CV to Sébastien Bardin as soon as possible (and at the very last before October 2020), as applications will be reviewed immediately as they arrive (first come first served). Each position will have a duration of 2 years and will be allowed to begin starting from 2 months after a successful interview, but not later than December 2020.
Remuneration Package
Remuneration for the postdoc includes a gross salary ranging from 33 kEUR to 39 kEUR per year, full access to the French healthcare, social care and pension system, as well as several other benefits, like coverage of 50% of all your Parisian public transport fees.
Working and Living in Paris
Our offices are located in Plateau de Saclay, south of Paris, the French biggest research and industry cluster. Our welcome agency France Accueil is available to help you find your home and settle here. Most of us live either in the wooden and quiet southern suburbs of Paris or closer to the bustling center of the city. Paris is the capital of France, a metropolis of 12.5 million people and one of the most visited travel destination in the world.
If you are interested in doing a PhD in Australia, using Isabelle to verify compiler optimizations, please read on...
We have two PhD positions available part of a new project funded by Oracle Labs Australia to model and verify sophisticated compiler optimisations in the Graal Java compiler. Graal is a high-performance polyglot virtual machine (VM) that not only supports JVM-based languages such as Java, Scala, Kotlin and Groovy, and LLVM-based languages like C and C++, but also more dynamic languages like Python and JavaScript. This research project focuses on verifying optimization passes of the Graal compiler, using the Isabelle interactive theorem prover.
For more details please see here.
We are looking for a motivated student interested in pursuing a PhD on developing mathematical foundations for Cyber-Security resilient Software Architectures, architectures that are resilient by default while relying on formal methods techniques.
The research position is at the Department of Software Engineering of Rochester Institute of Technology, RIT, NY, USA. The candidate will conduct their work as part of the center for Cyber-Security. Ideal candidates should have some background in one of the following ares a) software architectures b) formal methods c) discrete mathematics. The work encompasses theoretical research work as well as the ability to implement software tools. PhD stipends at RIT are between 28K and 32K USD.
The candidate will conduct their work as part of the Software Design and Productivity Lab, led by professor Mehdi Mirakhorli.
Relevant papers:
For informal and formal inquiries: contact Email.
Two PhD positions in Logic, Gothenburg (Sweden)
The Department of Philosophy, Linguistics, and Theory of Science invites applications for two PhD positions in Logic. One position is available on the research project Modal mu-calculus: A study in descriptive complexity lead by Bahareh Afshari funded by the Swedish Research Council. The second position is open to all topics in mathematical, philosophical and computational logic within the expertise of the Logic Group.
The Department of Computer Science at the University of Copenhagen is seeking candidates for a full professorship in Theoretical Computer Science (TCS). More specifically, we are inviting exceptional candidates from the broad fields of algorithms, complexity, and cryptography including privacy.
We are looking for an outstanding, experienced researcher with an innovative mind-set and intellectual curiosity to strengthen and complement the research profile of the Algorithms and Complexity Section, headed by Professor Mikkel Thorup. The Algorithms and Complexity Section is part of an exciting environment including the Basic Algorithms Research Copenhagen (BARC) centre, joint with the IT University of Copenhagen, and involving extensive collaborations with the Technical University of Denmark (DTU) and Lund University on the Swedish side of the Oresund Bridge. We aim to attract top talent from around the world to an ambitious, creative, collaborative, and fun environment. Using the power of mathematics, we strive to create fundamental breakthroughs in algorithms and complexity theory, but we also have a track record of start-ups and surprising algorithmic discoveries leading to major industrial applications.
The University of Copenhagen was founded in 1479 and is the oldest and largest university in Denmark. It is often ranked as the best university in Scandinavia and consistently as one of the top places in Europe. Within computer science, it is ranked number 1 in the European Union (post-Brexit) by the Shanghai Ranking.
The department offers a friendly and thriving international research and working environment with opportunities to build up internationally competitive research groups. Working conditions at the University of Copenhagen support a healthy work-life balance and Copenhagen is a family-friendly capital city.
The application deadline is May 24, 2020. See here for the full announcement with more information and instructions how to apply. Inquiries about the position can be made to Head of Section, Professor Mikkel Thorup and Head of Department, Professor Mads Nielsen.
The Institute of Computer Sciences of the Czech Academy of Sciences (ICS CAS), Prague, Czech Republic, invites applications for one tenure-track position in Computer Science. We especially seek applicants from fields that in one way or other contribute to the automation of formal reasoning, such as:
The closing date for application is 31st May 2020
More details can be found here.
Keywords: software security, binary code, program analysis, formal methods, vulnerabilities, adversarial codes
Several PhD positions are available in the BINSEC research group, Software Security Lab, CEA LIST, in the area of binary-level software security analysis, to begin as soon as possible at Paris-Saclay, France. Positions are three-year long.
Topics:
Our general objective is to leverage recent advances in software verification, security analysis and machine learning in order to propose advanced methods and tools
for supporting low-level security investigations, such as (but not limited to) vulnerability analysis, code protection, reverse engineering or malware analysis.
In that context, we propose 3 funded PhD positions on the following problems:
The candidates are expected to solve challenging research problems, implement their results in working prototypes, publish at top conferences or journals, and broadly participate to the scientific life of the group. All positions comprise theoretical work as well as prototyping (preferably in OCaml) and experimental evaluation.
The W3Proof project at Inria Saclay proposes to build the foundations for a distributed Web-like platform for developing, sharing, and certifying formal proofs, independent of any particular proof assistant.
We are looking for a Ph.D. candidate to work on this project. Candidates should know the basics of proof theory, lambda-calculus, and distributed systems technology (including cryptographic constructions for signing and tracking of provenance, content-based naming, etc.).
This Ph.D. student position is offered by Inria and the work will be done within the Partout team at the LIX laboratory of Ecole Polytechnique.
If you are interested in this Ph.D. position, submit
All inquiries and application material should be sent to Dale Miller or to Kaustuv Chaudhuri. We expect the position to start in October 2020, but there is some flexibility with the exact start dates.
We hope to make decisions on this position by at least 10 May 2020.
More information is available here.
The GSSI - Gran Sasso Science Institute offers seven, four-year PhD fellowships in Computer Science for the academic year 2020/21. The fellowships include a yearly salary of € 16,159.91 gross, free accommodation at the GSSI facilities and use of the canteen. The official language for all PhD courses is English.
Applications must be submitted through the online form by Thursday, 11 June 2020 at 5 pm (Italian time zone).
Computer Science at the GSSI and its PhD programme
The Computer Science group at the GSSI carries out high-quality, interdisciplinary research on algorithms, formal methods, and software analysis and development.
Further information on the group, its members, activities, current research projects, guests, wide international network and vibrant research environment can be found here.
The PhD program in Computer Science at the GSSI fosters theoretical and applied research on the above-mentioned fields, and equips young researchers with the knowledge and skills to successfully tackle the future challenges in the digital era.
The group of formal methods at GSSI is interested in formal models of concurrent and distributed systems. In this context, a few topics of interest are software quality, software verification, behavioural types, modelling and analysis of social networks and cyber-physical systems. The formal methods group is currently involved in several national and international projects such as BehAPI, IT-Matters, SEDUCE, OPEL and TheoFoMon.
About the Gran Sasso Science Institute
The GSSI-Gran Sasso Science Institute is an international PhD school and a centre for research and higher education in the areas of Computer Science, Mathematics, Physics and Social Sciences. The GSSI was founded in 2012 in L'Aquila (Italy) as Centre for Advanced Studies of the National Institute for Nuclear Physics (INFN) and was then established in March 2016 as a School of Advanced Studies providing post-graduate education. Through day-to-day collaboration and interaction, researchers and students have the opportunity to build a sound knowledge of research methods and to engage in interdisciplinary research, innovative approaches for scientific investigation and multicultural exchanges. In addressing the complexity of today's world, the GSSI is committed to removing all barriers between its areas of study and research. The dissemination of scientific results towards society and the promotion of cultural events for the generic public are among the goals of the GSSI.
More details are available here.
We have a fully-funded three-year PhD position in formal methods for information security. This is a joint doctorate (cotutelle) between IRISA (Rennes, France) and Heriot-Watt University (Edinburgh, Scotland). The student will obtain a PhD degree from both universities.
For more details, see here.
The deadline for applications is Friday, May 15, 2020, but applications will be considered until the position is filled.
For all inquiries please contact Barbara Fila and Saša Radomirović
AI Secure and Explainable by Construction:
We encourage interested applicants to contact us informally ASAP.
The project has sufficient flexibility to mitigate the effect of COVID-19, i.e. by accommodating later start date and remote working.
The project spans several subjects: type theory, automated and interactive theorem proving, security, AI and machine learning, autonomous systems, natural language processing and generation, legal aspects of AI. It will cover two main application areas: autonomous cars and chatbots, drawing from expertise and infrastructure provided by industrial partners working in these two areas. The project has a significant international span, with 12 partners from Academia and Industry in Europe (France, Germany, Israel, the Netherlands, Norway) and the US. Researchers joining this project will have excellent opportunities to travel to international conferences, organise scientific events, spend time with industrial partners, collaborate with academic leaders in the field, develop their own research profiles as well as gain experience in other AI and CS disciplines.
For further information, and instructions how to apply, please visit here.
Due to the covid-situation, the deadline for applications is extended till May, 31. The appointment starts from September, 2020 and can be delayed upon mutual agreement.
Applicants can can join one of the established research groups or propose their own research topic. The initial appointment is for one year, with the possibility of extension for another two years.
We are looking for candidates with background in Mathematics/Computer Science/Artificial Intelligence, which have a strong research record in at least one of these fields:
Teaching obligations are minimal: successful applicants are expected to give lectures on research topics they specialize in.
Novosibirsk Scientific Center is
For details about the positions please, visit here.
In addition, short term paid visits are possible.
Informal inquiries are welcome and should be directed to Dr. Denis Ponomaryov.
Benedikt Ahrens invites applications for a fully-funded PhD position in the School of Computer Science at the University of Birmingham, UK.
Topics of interest include:
Students broadly interested in one of these fields of research, or a related field, are strongly encouraged to apply.
Applicants should hold, or be about to obtain, a Masters or Bachelor degree in Computer Science or Mathematics.
The PhD position is fully funded, covering tuition fees and a tax-free scholarship. Healthcare is provided.
For further details please send an email to Benedikt Ahrens and see his website.
The theory group at Birmingham's School of Computer Science is very active, organising regular seminars and informal meetings, such as the YaMCATS category theory seminar, Midlands Graduate School, and Workshops on Univalent Mathematics. For more information see here.
Information on how to apply is given on this website. However, interested candidates should contact Benedikt Ahrens in the first instance.
The University of Innsbruck invites applications for a 4 year PhD position in the Computational Logic research group. Candidates must hold a master degree in computer science or mathematics. Knowledge of term rewriting and automated deduction is desired. Candidates close to obtaining a master degree are also invited to apply. Knowledge of German is not required. The position is an official university position with 15 September 2020 as starting date. The main task will be to pursue research leading to a dissertation. The position comes with teaching obligations of 2 hours per semester. The minimum gross salary (stipulated by collective agreement) for this position amounts to € 1.465 per month (14 times).
The official job advert (code MIP-11245) appeared here.
Applications (including CV, list of presentations, motivation letter, possible research topics) must be submitted electronically here.
We look forward to receiving your online application (code MIP 11245) until May 27, 2020
Informal inquiries may be addressed to Aart Middeldorp
The city of Innsbruck, which hosted the Olympic Winter Games in 1964 and 1976, is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of the Alpine environment and urban life in this historic town provides a high quality of living.
Further information is available from the following links:
CertiK is a world-leading cybersecurity firm based in NYC that focuses on smart contract analysis and blockchain auditing. It was founded by prof. Ronghui Gu (Columbia) and prof. Zhong Shao (Yale), drawing on their research about formal verification.
Currently the CertiK research department is developing an operating system kernel (CertiKOS) and a certified compiler (DeepSEA), both of them verified using the Coq proof assistant. We are looking for summer interns to help us transition these from academic research projects into production-ready software.
Available project include adding new system calls needed to run useful applications on CertiKOS; adding new language features, optimizations, or new verified backends to DeepSEA; and laying the foundations for decentralized proof-checking. The internship is suitable for current master/phd students, or strong undergraduates looking for research experience. Because of the current Covid-19 epidemic, these positions are completely remote.
Qualifications You should be familiar with one of the following areas:
Please send applications via this web site.