I am occasionally asked whether many readers of the AAR Newsletter try to meet the various challenges I offer and whether areas of mathematics are more interesting than areas of logic.
The answer is, I don't have enough evidence immediately in hand. But sometimes, a reader does ask for what might be termed a follow-up to an earlier column I have written.
In particular, a recent column I wrote on Boolean algebra led to a reader's asking about circle of proofs. In response, I focus here on Moufang loops and equations that define that area of mathematics, and yes, the question about the finding of a circle of pure proofs.
As background, decades ago I was told by a colleague at Argonne National Laboratory, that three equations had the property that, adjoining each alone to some other axioms, produced an axiom set of Moufang loops. That colleague also informed me that a question regarding the three equations remained unanswered. When I told the mathematician Ken Kunen about my intention to address that question, he informed me -- or asked, actually -- about a fourth equation to consider. Specifically, a proof existed that the first equation sufficed to deduce the second and that the second sufficed to deduce the third, but -- and here was the problem -- in order to deduce the first from the third to complete this circle of proofs, two more proofs were needed: a proof deducing the second from the third and then a proof deducing the first from the second.
So, rather than the pleasing existence of the sought-after three proofs for the circle, I sought a circle of pure proofs for four equations, the following. (I include more information than needed, noting that the percent sign means that from there to the end of the line is comment.)
x = x.
x * rs(x,y) = y. % right solvable
rs(x, x * y) y. % right solution is unique (implies left = cancellation)
ls(x,y) * y = x. % left solvable
ls(x * y , y) x. % left solution is unique (implies right = cancellation)
% identity:
1 * x = x .
x * 1 = x.
% left cancellation
% x*y != u | x*z != u | y = z.
% right cancellation
% y*x != u | z*x != u | y = z.
% Axiom, Moufang 1:
% (x * y) * (z * x) = (x * (y * z)) * x.
% Axiom, Moufang 2:
% ((x * y) * z) * y = x * (y * (z * y)).
% Axiom, Moufang 3:
% x * (y * (x * z)) = ((x * y) * x) * z.
% Axiom, Moufang 4:
% x * ((y * z) * x) = (x * y) * (z * x).
% A consequence of left and right surjective:
% It's all that is needed here.
% x * R(x) = 1.
% L(x) * x = 1.
% The following negate left and right inverse.
% y * e != 1.
% actually, L and R turn out to be the same in a Moufang loop
Your challenge (in effect, four challenges) consists in finding four proofs. You might begin by seeking a proof that, from the basic axioms with the Moufang 1 adjoined, you can deduce Moufang 2, with no constraint. Let that be your first challenge.
For the next three challenges, find proofs of Moufang 3 from Moufang 2, Moufang 4 from Moufang 3, and Moufang 1 from Moufang 4, each proof with no constraint.
Then, for the more exciting set of challenges that are consistent with the questions that were open, find the given circle of proofs, but find pure proofs. In other words, the proof of the second from the first must avoid the use of Moufang 3 and Moufang 4 to be pure.
Depending on the program you use -- I had in mind that you would be using an automated reasoning program to meet the challenges -- the last line of each proof might be the so-called flip of the goal. In other words, rather than proving s = t, your program proves t = s. If such is the case, the further challenge -- and not trivial according to my research -- is to prove the various Moufang items as given.
If you have used a Knuth-Bendix approach, the final set of challenges asks for proofs that are free of demodulation and that are forward, rather than backward or bidirectional. If you succeed in finding the four proofs for the circle of pure proofs, you will discover, I feel rather sure, that their lengths differ sharply.
As a forum for discussions and for sharing new ideas centered on automated reasoning, the second ARCADE workshop was held as a satellite event of CADE-27 in Natal. Building on the success of the first ARCADE 2017 in Gothenburg, this workshop encouraged non-technical position statements of 2-4 pages revolving around challenges, applications, directions, and exemplary achievements in automated reasoning.
Out of 12 submitted abstracts, the program committee selected 11 for presentation and discussion at the event. With 33 registrations and even more attendees, ARCADE was one of the largest workshops at CADE. In fact, several people booked the flight to Brazil only or mainly to attend ARCADE.
The workshop was divided into five topic blocks, consisting of one or two talks each.
All papers can be found on the ARCADE 2019 website. As organizers we are currently working on finding a platform to publish post-proceedings. To that end, authors will be invited to update and extend their original submissions while taking into account the feedback received during the event.
In summary, ARCADE 2019 offered a lively atmosphere for vivid discussions on a variety of current topics. We recommend to all of you readers to participate in the next edition of ARCADE - it’s exciting, fun, and there’s going to be a great dinner afterwards!
As organizers, we thank the authors for their interesting and thought-provoking input, and the audience for engaging in such animated and cheerful debates. We are, moreover, grateful to Pascal Fontaine, Christoph Weidenbach, and the local organizers for their great support in all kinds of organizational issues.
The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to
A nomination is required for consideration for the Herbrand Award. Nominations can be submitted at any time. The deadline for nominations to be considered for the Herbrand Award 2020 (which will be given at IJCAR 2020) will be in spring; however, we encourage people to prepare nominations early and not delay submission until the deadline! 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.
Philipp Rümmer, Secretary of AAR and CADE
The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, choosing the Herbrand Award selection committee, instituting new awards, etc.
The current members of the board of trustees are (in alphabetical order):
The terms of Jasmin Blanchette, Laura Kovács, Renate Schmidt, and Christoph Weidenbach end.
We are therefore seeking to elect four trustees.
An election will be held soon and all CADE members will receive a ballot.
The following candidates were nominated and their statements, in alphabetic order, are below:
It is a pleasure and honor to be nominated for the CADE board of trustees. CADE is my home conference: I attended it for the first time right after receiving my undergraduate degree, and I attended most editions since then. Automated deduction is at the heart of my research programme on the concept, design, implementation, and evaluation, both empirical and machine-independent, of methods for automated theorem proving, satisfiability modulo theories, and their integrations.
I served as AAR Secretary (1997-2004), CADE Secretary (1999-2004), CADE trustee (2004-10 and 2013-16), IJCAR Steering Committee Chair (2002-04 and Dec. 2009-Dec. 2010), Program Committee Chair of CADE-24 (2013), and CADE President (Dec. 2009-Dec. 2010 and 2013-16). As President, I led the trustees in instituting the Thoralf Skolem award, the CADE Best Paper award, and the SAT/SMT/AR Summer School. Early on, I was involved with the democratic reform of CADE, and was a founder of IJCAR, writing the IJCAR 2001 and 2004 manifestos. I always supported funding for the Woody Blesdoe Student Travel Award and geographical balance of conference locations.
I am in favor of co-locations for both CADE and IJCAR, and for more events in IJCAR: I am thrilled that ITP rejoins IJCAR in 2020. I am in favor of instituting a CADE Student Best Paper award for papers whose authors are all students, of extending the Skolem award to IJCAR, and engaging CADE/IJCAR on climate change (e.g., SIGPLAN and Climate Change). My vision for our conferences is to strive for scientific excellence, nurturing creativity, cross-fertilization of ideas, openness to both new theoretical paradigms and new applications, preserving historical ties (e.g., FLoC) while being open to new ones. We need to keep working on the visibility, recognition, and attractiveness of our field.
Being a CADE trustee is about service and leadership, or leadership understood as service in the highest sense. It is about listening, remembering, foreseeing consequences, taking responsibilities, ensuring communication and transparency. If elected, I would bring to the board experience, institutional memory, and my unfaltering enthusiasm and energy for our ever fascinating research field. More information on my research and professional service can be found at http://profs.sci.univr.it/~bonacina/.
My research covers various aspects of automated deduction, both theoretical and practical, mostly focused around SMT. CADE is my home conference; I attend CADE and IJCAR whenever possible. I particularly like CADE's tradition to welcome results on both theory and practice of automated reasoning. It is most necessary to provide visibility to implementation works, since they are very time consuming and of uttermost importance to validate theory and for applications. CADE should also not overlook more theoretical aspects that may have a less immediate but a longer term impact on automation of logic. Finally, automated deduction should not be understood in too tight a sense, and CADE should continue encouraging submissions from all fields where logic-based computer assisted reasoning is of importance.
My impression is that CADE, while being the major forum on automated deduction, is a particularly friendly and open conference. CADE should remain so. This requires continuous efforts. Supporting the younger members of our community should be a major objective for the Board of Trustees. The Board of Trustees has had a positive influence in this direction in the past — by setting up or encouraging, e.g. the Woody Bledsoe Awards, tutorials, summer schools, and best student papers — and should continue to actively support younger scientists, and be attentive that CADE remains open and friendly.
The current cycle of conferences, CADE alternating with IJCAR, and IJCAR as a part of FLoC every four years, is, I believe, the right organization for the current situation, since it preserves the specificity of CADE and of the other compound conferences of IJCAR. I however firmly think that there should be a tighter coordination between CADE and the friend conferences like FroCoS, ITP, and Tableaux, e.g. to adjust dates and locations. This will benefit everybody.
My research focuses on the combination of automated reasoning and symbolic computation for automating program analysis. Since 2010, I became the co-developer of the first-order theorem prover Vampire, leading the development of Vampire to support applications of program analysis. Hence, my interest covers both theoretical and practical aspects of automated reasoning. My research is mainly supported by an ERC Starting Grant 2014, Wallenberg Academy Fellowship 2014 and ERC Proof of Concept 2018.
I have been regularly attending CADE since 2008 and I became really active in the organization of CADE since 2016. In 2016, I had the honor of becoming a CADE Trustees. In my years as a trustee, I was mainly focused on two activities:
If I am elected as a CADE trustee again, I would further be determined to organize events supporting the career development of early-stage researchers. I believe that having more PhD/master students attending CADE is crucial, allowing "fresh-(wo)men" in automated reasoning to interact with more senior researchers in the field. I am therefore committed to further continue the tradition of the Woody Bledsoe student travel grants at CADE. I also plan to turn the deduction mentoring workshops (DeMent) into a workshop series, regularly taking place at CADE/IJCAR.
CADE should further maintain the balance between theoretical work, applications and tools. I very much support the organization and maintenance of the CASC System Competition. I would further be committed to strengthen the relation between CASC and SMT-COMP, given that reasoning about theories and quantifiers is a common hot topic in both competitions.
Automated reasoning techniques and tools are increasingly used in related areas, such as systems security, software verification, symbolic computation, and machine learning. I would therefore pay a special attention in strengthening the connection to top conferences in related areas, such as ISSAC, CAV, POPL, CSF, to only name a few.
I would also try to organize other applications-oriented events affiliated with CADE, similar to the very successful industry session "Formal Methods in Industry" at FLoC 2018. My aim with such events would be to have leading experts discussing challenges of using automated reasoning in industry, while also covering business perspectives of automated reasoning.
I have been attending CADE since 1994. I presented several papers at CADE and IJCAR and served on many program committees. Together with Amy Felty, I served as PC chair of the highly successful 25th edition in Berlin.
After spending more than ten years in Japan, since 2003 I lead a research group on computational logic in Innsbruck, in which automated deduction plays an important role. System descriptions and competitions (CASC) are an essential part of CADE. Several software tools (on certification, confluence, theorem proving, to name a few) are developed in Innsbruck and we initiate/organize/host competitions (CoCo, TermCOMP) and workshops (IWC, WST) to advance the development of tools.
One of the most important topics that needs to be addressed by the CADE trustees is the publication forum of the proceedings. More and more national funding agencies insists on open access publications. The current situation is very unsatisfactory. Open access is essential to ensure that CADE stays an attractive conference in the future. Springer charged authors 806,40 euros for gold open access for a CADE-27 paper. If this is not immediately paid by a funding agency (FWF in my case), authors are at the receiving end of several aggressive if not threatening email messages by Springer. This has to stop! If CADE cannot get a deal with Springer like ETAPS, where all published papers appear in gold open access, then I will actively push for a change of publication forum if elected as CADE trustee.
I further think CADE should adopt ideas implemented in other conferences, like welcoming short papers that describe interesting ongoing research, shortening talks to have more papers presented and thus more people attending. Moreover, tool submissions should come with artifact evaluation and the tools should be made available to the community.
I have had the privilege of serving on the board of trustees in 2008-2015 and 2016-2019. I was PC Chair of CADE-22, member of the Skolem award committee 2017 & 2019. I serve, or have served, on various other Steering Committees (TABLEAUX 2014-2019, FroCoS 2012-2019, BLC 2017-2019, PAAR since 2014). I therefore appreciate the important function of the board in securing good conference locations, appointing PC Chairs, constituting award committees, ensuring the success of various other activities in our area and providing leadership and representation for the area of automated reasoning.
If re-elected I will continue to focus my efforts in arguing for integrity, representativeness and responsibility in the workings of the board of trustees and the processes of all our various awards, and will continue to push for a review and revision of the new Herbrand Award process. In the interest of avoiding misunderstanding, there is no question the right persons have won the award and the working of the Herbrand Award Committee was beyond question. My issues relate to the timing of the appointment of the Herbrand award committee (after nominations have been received), the balance in the committee, its size, insufficient awareness and consideration of subtle conflicts and the creation of consequences, which carry the risk of diminishing the standing of the award and the credibility of the trustees (and would be detrimental for the community).
In this extraordinary time of blatant inaccuracy, positive misinformation and decline of moral frameworks, as academics and scientists we must defend basic scientific values and don't become complacent in upholding the interests and integrity of every member in every of the diverse subareas of automated deduction, awards winners, trustees, our conferences, the community as a whole and science in general.
My background
My main research involves the development and theoretical analysis of
reasoning methodologies and automated reasoning tools as well as
applying these in areas such as artificial intelligence, knowledge
representation, agent-based systems and mathematics. At present a very
strong focus of my work is the development of tools for transforming
ontologies such as forgetting, abstraction, difference tracking,
information hiding and hypothesis generation.
Other professional activities include (co-)chairing and (co-)organising various international conferences and workshops, and (co-)editing several books, conference/workshop proceedings, and special journal issues. I serve on the editorial boards of the Journal of Automated Reasoning, the Journal of Artificial Intelligence Research and the Journal of Applied Non-Classical Logic.
I'm a long standing member of the CADE community and have been the elected CADE president for the past three years. During this time the trustees and I have initiated a number of actions to further strengthen the impact of the CADE community. In addition to the support of senior researchers through the Skolem and Herbrand award, we have started measures for young researchers. The new and successful ARCADE workshop series serves as a forum for discussion at a lightweight entry level. It also offers the possibility for young researchers to have their first appointment as a workshop chair, supported by the trustees. The trustees further decided that student fees for the conference will now always include all social events, there will always be a best paper and best student paper award at CADE, and we will announce an automated reasoning PhD award by end of this year. Finally, and in particular through great commitment by our treasurer Neil Murray, we have founded CADE Inc at the state of New York without disturbing any financial operations. This step was necessary after CADE Inc. was dissolved by the state of Illinois. In case I'm re-elected I will continue my work on strengthening CADE as the prime conference on automated deduction.
The CADE Single Transferable Vote algorithm is part of the CADE bylaws. It is used for the election of the CADE trustees. In their paper "Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election Scheme." at CADE 2013, Bernhard Beckert, Rajeev Goré, and Carsten Schürmann formally analyzed the CADE STV Algorithm and pointed out several differences and weaknesses compared to standard STV algorithms. Since then, the respective CADE secretaries Martin Giese and Philipp Rümmer always compared the outcome of a CADE STV trustee election with standard STV algorithms. So far there was no difference in the eventual result. In addition, the CADE STV algorithm is a non-standard, CADE specific algorithm that is not supported by any automatic voting platform. As a result, the CADE trustee elections always had a manual component carried out by the secretary and the president.
For both above reasons, the CADE trustees suggest to move from the CADE STV algorithm to a standard algorithm that is supported by automatic voting platforms. We do not want to include the new algorithm in the bylaws because it will make any future change as difficult as this one. Instead the used algorithm will be made public on the CADE homepage outside the bylaws.
A vote on this motion will be held in conjunction with the 2019 CADE trustee election, and all CADE members will receive a ballot.
Technically, the CADE trustees suggest to change the bylaws as follows:
(CURRENT)to
Subsection 2.3 Election of Trustees
Elected members of the Board of Trustees shall be elected via email by the entire CADE membership using the Single Transferrable Vote system. The election will be held within thirty days of the business meeting that marks the close of nominations and shall be binding on the Trustees.
(NEW)
Subsection 2.3 Election of Trustees
Elected members of the Board of Trustees shall be elected electronically by the entire CADE membership. The CADE trustees decide on a voting procedure for the trustee election. The procedure will be published on the CADE homepage. The election will be held within thirty days of the business meeting that marks the close of nominations and shall be binding on the Trustees.
We invite proposals for sites around the world to host the international Conference on Automated Deduction (CADE) to be held in summer 2021. CADE typically merges into IJCAR (the International Joint Conference in Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome.
The deadline for proposals is 30 November 2019.
CADE's/IJCAR's recent location history is as follows:
The upcoming CADE/IJCAR event will be:
We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal deadline.
Proposals should address the following points that also represent criteria for evaluation:
Prospective organizers are encouraged to get in touch with the CADE Secretary and the CADE President for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers are encouraged.
The mission of ICCS is to harmonize the creativity of humans with the productivity of computers. The conference advances the theory and practice in connecting the user's conceptual approach to problem solving with the formal structures that computer applications need to bring their productivity to bear.
Simon Polovina
This Special Issue, which grew out of the International Conference on Conceptual Structures (ICCS 2019), focuses on the formal analysis and representation of conceptual knowledge, at the crossroads of artificial intelligence, human cognition, computational linguistics, and related areas of computer science and cognitive science. Recently, graph-based knowledge representation and reasoning (KRR) paradigms are getting more and more attention. With the rise of quasi-autonomous AI, graph-based representations provide a vehicle for making machine cognition explicit to its human users. Conversely, graphical and graph-based models can provide a rigorous way of expressing intuitive notions in computable frameworks. The aim of the ICCS 2019 conference is to build upon its long-standing expertise in graph-based KRR and focus on providing modeling, formal, and application results of graph-based systems. The Special Issue welcomes contributions from a modeling, application, and theoretical viewpoint:
Topics:
Submission Information:
Manuscripts should be submitted online at www.mdpi.com by registering and logging in to this website. Manuscripts can be submitted until the deadline. All papers will be peer-reviewed. Accepted papers will be published in the journal (as soon as accepted) and will be listed together on the special issue website. Research articles, review articles as well as short communications are invited. For planned papers, a title and short abstract (about 100 words) can be sent to the Editorial Office for announcement on this website. Submitted manuscripts should not have been published previously, nor be under consideration for publication elsewhere (except conference proceedings papers). All manuscripts are thoroughly refereed through a single-blind peer-review process. The submissions must contain at least 30% new material for being accepted in this journal.
Please visit the link in the beginning of the email for further details.
Deadline for manuscript submission: 31 January 2020
FSCD 2020 will be the fifth edition of the International Conference on Formal Structures for Computation and Deduction. IJCAR 2020 will be the tenth International Joint Conference on Automated Reasoning.
We invite proposals for workshops, tutorials or other satellite events, on any topic to related formal structures in computation, deduction and automated reasoning, from theoretical foundations to tools and applications.
Satellite events will take place on the 29 June and 4-5 July, before and after the main conference (30 June - 5 July). It is expected that satellite events would run for 1 or 2 days, and be open to participants of parallel events.
Proposals
Proposals must be limited to three pages and should be submitted by
email to the workshop chairs. Each proposal should consist of the
following two parts.
The organizers of satellite events are expected to create and maintain a website for the event; handle paper selection, reviewing and acceptance; draw up a tentative programme of talks; advertise their event through specialist mailing lists; prepare the informal pre-proceedings (if applicable) in a timely fashion; and arrange any post-proceedings. Some amount of financial support may be offered to workshops, depending on the number of participants.
The FSCD-IJCAR organizing committee will handle promotion of the event on the main conference website; integration of the event's programme into the overall timetable; registration of participants; arrangement of an appropriate meeting room; and provision of lunch and coffee breaks for participants.
Important Dates
ICALP 2020 and LICS 2020 will take place in co-location from 8th till 12th of July 2020. The conferences will be preceded by two days of joint workshops, held on July 6th and 7th. We invite proposals of workshops affiliated with ICALP-LICS 2020 on all topics covered by ICALP and LICS, as well as other areas of theoretical computer science.
Proposals should be submitted no later than November 30th, 2019 by sending an email to Frederic Blanqui. Due to limited space of the venue we might not be able to accommodate all the proposed workshops. You should expect notification on the acceptance of your proposal by mid December 2019.
A workshop proposal submission should consist of:
As for the format, a standard option is a one-day workshop consisting of invited talks by leading experts and of shorter contributed talks, either directly invited by the organizers or selected among submissions. Deviations from this standard are also warmly welcome, including a shorter or a longer time span than a full day, or other elements of the schedule like open problem sessions, discussion panels, or working sessions.
If you plan to have invited speakers, please specify their expected number and, if possible, tentative names. If you plan a call for papers or for contributed talks followed by a selection procedure, the submission date should be scheduled after ICALP 2020 and LICS 2020 notification, while the notification should take place considerably before the early registration deadline. In your submission please include details, in particular the time schedule, of the planned procedure of selecting papers and/or contributed talks. If you plan to have published proceedings of your workshop, please provide the name of the publisher. Please be advised that ICALP-LICS 2020 is not able to provide any financial support for publishing workshop proceedings.
We expect the workshops to be financially independent. The expenses related to the participation of invited speakers, production of workshop materials, etc. should be covered from independent sources. On top of standard ICALP/LICS registration fee there will be a moderate registration fee for the workshops that will cover coffee breaks. This workshop fee will be waived for maximum two invited speakers for each workshop.
IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR 2020 technical program will consist of presentations of high-quality original research papers, short papers describing interesting work in progress, system descriptions, and invited talks.
IJCAR 2020 will be co-located with the conference FSCD.
IJCAR 2020 is the merger of leading events in automated reasoning:
Topics:
IJCAR 2020 invites submissions related to all aspects of automated or interactive reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems or proof assistants are solicited.
IJCAR topics include the following ones:
Best paper award:
IJCAR 2020 will recognize the most outstanding submission with a best paper award at the conference.
Student travel awards:
Woody Bledsoe Travel Awards will be available to support selected students in attending the conference.
Important dates:
More information is available on the conference's web page.
FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, models of computation, semantics and verification in new challenging areas. The suggested, but not exclusive, list of topics for submission is:
Important Dates
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
More information is available on the conference's web page.
With its special focus theme on "Explainable AI and Responsible AI", the summit intends to promote the interplay between logical approaches and machine learning based approaches in order to make AI more transparent, responsible and accountable.
List of Topics
Submissions in all areas of artificial intelligence are welcome. Suggested topics include, but are not limited to:
Key Dates
More information is available on the conference's web page.
ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of four annual conferences, accompanied by satellite workshops.
Main Conferences (27-30 April)
TACAS '20 will host the 9th Competition on Software Verification (SV-COMP).
POST, which was an ETAPS conference 2012-2019, has been discontinued.
Important Dates
Satellite Events (25-26 April)
A number of satellite workshops will take place before the main
conferences.
More information is available on the conference's web page.
The Program Committee of the 24th European Conference on Artificial Intelligence (ECAI 2020) invites the submission of papers for the technical programme of the Conference. High-quality original submissions are welcome from research results and applications of all areas of AI. The following list of topics is indicative; other topics are welcome.
The Call for Papers is available here.
Workshops, tutorials and other events
In addition to its full programme of technical papers, ECAI2020 will feature many AI-related events for researchers, students and all attendants who are interested on contemporary AI. Separate calls have been issued for:
Futhermore, ECAI2020 will have a special focus on Starting Researchers, who will be able to participate in an specific program including the Doctoral Consortium, the Three Minutes Thesis Competition, the Lunch with an EurAI Fellow and the Job Fair.
Some Important Dates
More information is available on the conference's web page.
CiE 2020 is the 16th conference organized by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world.
Special Sessions
:Important Dates:
More information is available on the conference's web page.
The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric.
Suggested, but not exclusive, topics of interest include:
Important Dates
Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is given by anywhere on earth (AoE).
More information is available on the conference's web page.
LATA is a conference series on theoretical computer science and its applications. LATA 2020 will reserve significant room for young scholars at the beginning of their career. It will aim at attracting contributions from classical theory fields as well as application areas.
Scope:
Topics of either theoretical or applied interest include, but are not limited to:
Deadlines (all at 23:59 CET):
More information is available on the conference's web page.
TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2019 was held 11-14 June in Oslo, Norway. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings.
Submission to this post-proceedings volume is open to everyone, also to those who did not participate in the conference. We welcome high-quality descriptions of original work, as well as position papers, overview papers, and system descriptions. Submissions should be written in English, not overlapping with published or simultaneously submitted work to a journal or a conference with archival proceedings.
The scope of the post-proceedings is the same as the scope of the conference: the theory and practice of type theory. In particular, we welcome submissions on the following topics:
Important Dates
Details
Editors
The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming.
The TYPES areas of interest include, but are not limited to:
We encourage talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress.
Important dates:
More information is available on the conference's web page.
Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.
Topics
Dates
More information is available on the workshop's web page.
Reasoning is at the very heart of logic, constituting its subject matter. I n the last few decades, there has been considerable progress both in the pu rely logical analysis of reasoning and in applied logical investigations of various concrete subject domains, such as philosophical and scientific dis course, logic programming and everyday communication. Reasoning has been st udied from proof-theoretical as well as semantic standpoints. Along with fu rther elaboration of standard techniques (axiomatic systems, sequent calcul i and natural deduction) a range of other approaches (such as display calcu li, tableaux methods, hypersequent systems, etc.) and semantic modeling of logical systems are being developed. Moreover, there is a powerful traditio n of analyzing and evaluating reasoning patterns by means of informal logic and argumentation theory. Recent advances in these fields, in particular c onstructing theoretical models of argumentation and dialectical systems, ha ve proved promising. The aim of the conference is to bring together scholar s working in various areas of proof-theoretic, semantic, argumentative and informal logic analysis. The topics of interest may include, but are not li mited to:
Important dates
More information is available on the conference's web page.
In recent times, the verification of heap-manipulating programs, and static analyses in particular, has seen substantial success, largely due to the development of ‘Separation Logics’ (SLs). SLs provide embedded support for ‘local reasoning’ : reasoning about the resource(s) being modified, instead of the state of the entire system. This form of reasoning is enabled by new syntax (dedicated atomic proposition and separating connectives) and corresponding semantics. Such expressivity comes with the inherent difficulty of automating these logics. Combining this power with induction/recursion allows to concisely specify a large class of recursive data structures and programs, but further increases the computational burden.
The goal of this workshop is to bring together academic researchers and industrial practitioners focused on improving the state of the art of automated deduction methods for Separation Logics. We will consider technical submissions presenting work on the following topics (the list is not exclusive):
The workshop is affiliated with the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020).
Important dates (AoE):
More information is available on the workshop's web page.
ThEdu's programme comprised one invited contribution and four regular contributions, whose abstract are in the workshop web-page. Now postproceedings are planned to collect the contributions upgraded to full papers. The contributions' topics are diverse according to ThEdu's scope, and this is a call open for everyone, also those who did not participate in the workshop. All papers will undergo review according to EPTCS standards.
THedu'19 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.
Topics of interest include:
Important Dates
More information is available on the workshop's web page.
The meeting is a successor to Lean Together 2019.
The first three days will focus on formal methods in pure and applied mathematics, including interactive theorem proving, automated reasoning, verification of symbolic and numeric computation, and general mathematical infrastructure.
The last two days will be devoted to specifically to the Lean Theorem Prover and its core library, mathlib. Users and library developers will have opportunities to present work in progress and discuss plans for the future.
Attendance is free and open to the public, but we ask you to let us know by December 6 if you plan to come. If you are tentatively planning to attend, please tell us now and update us if your plans change. You register via the web page above, or contact the organizers, Jeremy Avigad and Robert Y. Lewis.
The meeting is supported by grant FA9550-18-1-0325 from the Air Force Office of Scientific Research. The contents do not necessarily reflect the views of the AFOSR.
More information is available on the workshop's web page.
We are welcoming applications for a Postdoc to join the Vampire team in Manchester to work on theory reasoning. There are a number of interesting possible research directions including, but not limited to, extending current successful work on theory instantiation and integration of SMT solvers into proof search. An ideal candidate would have some experience with developing or using theory reasoning techniques.
This role is suitable for those who have recently obtained (or are about to obtain) a PhD as well as those with more experience.
Full job details (and the link to apply) are available here (the job details are found by following a non-obvious link at the bottom of the page)
Please contact Giles Reger for all queries.
Graz University of Technology, Department of Computer Science and Biomedical Engineering invites applications for a Tenure Track Professorship in Formal Methods for Dependability.
We are looking for an excellent researcher with a background in formal methods for dependable secure systems. She or he is expected to carry out basic research in formal modeling, analysis, verification and synthesis and is interested in applications to security and/or artificial intelligence.
The professorship will be part of the Institute of Applied Information Processing and Communications and the research focus of the candidate should complement the current faculty positions of the institute.
With 30 years of research in information security, the Institute of Applied Information Processing and Communications (aka IAIK) is a well-established player in the field. More than 60 researchers work on topics like security architectures, side channels, cryptography, formal methods, identity management, and e-government.
Among the recent sparkling highlights of IAIK's research are the processor vulnerabilities known as "Meltdown" and "Spectre". IAIK cryptographers have contributed to major competitions in cryptography, like AES, SHA-3, and CAESAR; these contributions were always shortlisted or even won the competition. IAIK has built a strong presence in formal methods with a focus on reactive synthesis and, more recently, verification of security constructs.
The institute collaborates closely with research groups and industry partners around the globe. The recently announced Cybersecurity Campus Graz also creates a unique local environment. This new hub for information security unites basic research, education, technology transfer, and industry partners all under one roof.
The courses of IAIK typically are among the best evaluated of the computer science curricula. At bachelor's level, these courses are computer organization, operating systems, computer networks, systems programming, logic and computability, and information security.
Requirements
A relevant national or international university education with a completed doctoral/PhD degree.
Expected Qualifications
To ensure effective international representation of the research group and its work, excellent spoken and written competence in English is required. Specifically, willingness to teach courses in English is expected. Fluency in German or the willingness to acquire it is also required. The successful candidate is also expected to transfer her/his residence to the area of Graz.
Graz University of Technology aims to increase the proportion of women, in particular in management and academic staff, and therefore qualified female applicants are explicitly encouraged to apply. Until a balanced ratio of men and women has been achieved at the university, preference will be given to women if applicants are equally qualified.
Graz University of Technology actively promotes diversity and equal opportunities. Applicants are not to be discriminated against in personnel selection procedures on the grounds of gender, ethnicity, religion or ideology, age, sexual orientation (Anti-discrimination). People with disabilities and who have the relevant qualifications are expressly invited to apply.
Our Offer
The advertised position is a tenure-track career position for an initial period of 6 years. (pursuant to § 99 para. 5 of the Universities Act) After the conclusion of a qualification agreement, the job holder is appointed as Assistant Professor. After a positive evaluation of the qualification agreement, the position will be turned into a permanent position as Associate Professor. After a further competitive procedure, the promotion to Full Professor is possible. Graz University of Technology provides excellent working conditions in a lively scientific community combined with the outstanding living quality of the Graz area.
We offer an internationally competitive salary based on the profile of the applicant. The formal minimum annual gross salary for the position is € 59.003,00 per year, including social and health insurance. This corresponds to category B1 of the collective agreement for employees of Austrian universities.
Your Application
Interested applicants are requested to send a detailed application in electronic form, and should quote the position identification number 7050/19/021:
The interviews for the position are expected to take place in the week from 27 January 2020. Candidates are asked to be available in this period. For further questions, please contact the Dean’s office.
The Department of Computer Science at Aarhus University, Denmark, offers a considerable number of PhD and PostDoc positions in the areas of Logic, Semantics and Programming Languages. Our research spans a wide spectrum of topics concerning models and logics for programming languages and type theories, language-based security, blockchains, theoretical foundations and practical tools for program analysis, formal verification and model checking.
Aarhus University admits PhD students on the basis of a bachelor's degree (for 5 year PhDs) or a master's degree (for 3 year PhDs). If admitted, all tuition is covered, and a generous stipend is provided. Postdoc positions can be for 1 or 2 years, and with the possibility of renewal (depending on the individual projects and sources of funding).
Interested applicants at all levels are encouraged to contact the respective faculty for details, enclosing a CV and a short description of interests.
Aarhus University is realizing an ambitious multi-phase digitalization initiative which will help prepare researchers, students and the labour force for the digital transition of the future. The initiative aims at significant expansion of the Department of Computer Science for faculty and students.
Next deadline: November 1st, 2019
Information about the PhD program: here.
Several postdoc positions and PhD stipends are available at the Center for Advanced Software Analysis (CASA) at Aarhus University, Denmark, funded by the European Research Council.
The CASA center covers research in program analysis, type systems, testing, language design, and programming tools, with a particular focus on static analysis and automated testing for web and mobile apps.
The postdoc positions are at the level of Research Assistant Professor of Computer Science and are initially for one year, but they can be extended by mutual consent. We welcome researchers with clearly demonstrated experience and skills in one or more of the research areas mentioned above.
The PhD positions include full tuition waiver and a very competitive scholarship. Applications are welcomed from students with either a BSc or an MSc degree. Students with a strong background in Programming Languages will be preferred.
For more information, see this website or contact Professor Anders Møller.
Interested candidates should send an email containing a brief letter of interest and a CV. Applications will be considered until the positions are filled.
The formal methods group is led by Paul Attie, Clement Aubert, Harley Eades, and Alexander Schwarzmann. We are interested in state of the art theory and its application. Among our envisaged directions is the application of formal methods to cybersecurity and sophisticated distributed systems (both hardware and software). PhD students who expect to graduate within a year are encouraged to apply.
The formal methods group is located in the Georgia Cyber Center a $100 M facility which is ``the single largest investment in a cybersecurity facility by a state government to date.'' The Georgia Cyber Center seeks to prove the USA with a ``decisive advantage in cyberspace,'' by means of a unique industry-government-academia partnership. The Georgia Cyber Center hosts companies involved in cybersecurity work, and together with the US Army Cyber Command headquartered in Fort Gordon, Augusta, and local academia, provides a unique ecosystem where challenge problems from military and industry feed into academic research, and research results feed back into industry and government practice.
Please include in your application a CV, a statement of purpose, and contact information for at least three referees.
Benedikt Ahrens would like to invite applications for a 2-year postdoctoral position at the University of Birmingham, School of Computer Science. The postdoctoral researcher will work with Paige Randall North (Ohio State University) and him on a topic in the area of (homotopy) type theory; details can be discussed.
The position is funded by the EPSRC grant "A theory of type theories", PI Benedikt Ahrens.
The starting date of the position is somewhat flexible; it should be between late 2019 and mid 2020.
How to apply
There is no official job opening yet. Interested people are encouraged to contact Benedikt Ahrens by email in the first instance to discuss their research interests and details of the position.
About Birmingham
The School of Computer Science has a large and thriving Theoretical
Computer Science research group, with a particular focus on category
theory and its applications to the logical foundations of computer
science. Among our research interests are:
The group currently has 12 permanent staff and more than a dozen PhD students. They have a weekly seminar, as well as more informal meetings and reading groups. Information on all of this can be found on their webpage. They are regularly hosting international events in theoretical computer science in general and type theory in particular; recently, this included CSL 2018, 6WFTop, School and Workshop on Univalent Mathematics, and Midlands Graduate School.
The School of Computer Science at the University of Birmingham, UK, is continuously looking for strong PhD candidates. One particular field of interest is formal methods applied to distributed systems. Students broadly interested in this field of research are strongly encouraged to apply. Topics of particular interest are, for example:
Applicants must hold (or be about to obtain) a Masters or Bachelor degree in Computer Science. In addition, they must have a strong background in one of the following areas:
PhD positions are typically for 3.5 years and are fully funded, covering tuition fees and a bursary.
Please, do not hesitate to contact Vincent Rahli for further details. In addition, feel free to browse his webpage for more information on my research interests. The two following papers are especially relevant:
Additionally, the following page contains useful information regarding our lively theory group, which the successfully candidate would be part of.
Benedikt Ahrens would like to invite applications for a fully-funded PhD position in the School of Computer Science at the University of Birmingham, UK. The PhD student will work with him on topics related to categorical semantics of programming languages and computer theorem proving. Students broadly interested in these fields of research are strongly encouraged to apply. Topics of particular interest are:
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 free.
Please, do not hesitate to contact Benedikt Ahrens by email for further details. In addition, feel free to browse Benedikt Ahrens's webpage for more information on his research interests.
The theory group at Birmingham's School of Computer Science is very active, organising regular seminars and informal meetings. Many relevant international events frequently take place in Birmingham such as YaMCATS category theory seminar, Midlands Graduate School, and Workshops on Univalent Mathematics. For more information see here.
Information on how to apply is given here. However, interested candidates are strongly encouraged to contact Benedikt Ahrens in the first instance.
Universite Catholique de Louvain is seeking to recruit a PostDoc/Research engineer position in a full time position to work on a project on assistive code repair. The post is initially offered for one year, with options to extend for up to three years (project duration is three years from October 2019).
The main responsibilities of the successful candidate will be to:
The post holder will be working closely with researchers within the group at UCLouvain and industrial partners. The post holder will benefit from a strong research environment provided at UCLouvain and within the team. There will also be opportunities to collaborate on other related projects in the domains of security and verification.
The ideal candidate will hold a PhD or other significant experience in one or more of the following areas:
Information enquiries are welcome and should be directed to Dr Thomas Given-Wilson or Prof. Axel Legay.
Net salary is 2200-2500 euro per month (after taxes and social security).
Applications should be sent to both Dr Thomas Given-Wilson or Prof. Axel Legay.
Below is the description of postdoc positions. Phd positions are similar and can be found here.
This call can also be found here.
As part of the ERC Consolidator Grant "Certified Quantum Security" and the US Airforce project "Verification of Quantum Cryptography", we are looking for postdocs to work on verification of quantum cryptography (or more generally on quantum cryptography).
We will develop methods for the verification of proofs in quantum cryptography. Similar to what the EasyCrypt tool does in classical cryptography. The scope of the project covers everything from the logical foundations, through the development of tools, to the verification of real quantum protocols.
The ideal candidate would have experience in:
Of course, expertise in all those areas is very rare, so candidates who are strong in some of those areas and are interested in the others are encouraged to apply!
Please contact Dominique Unruh if you have more questions about the project, the required background, Estonia, the position itself, or the application process. I can also provide a detailed description of the overall research project.
The salary range is 30000-36000 Euro per year (depending on experience), which is highly competitive in Estonia due to low costs of living and low income tax rate (20%). Pension contributions and health insurance are covered by the employer.
Applications are accepted at any time (until all positions are filled), and positions can start as soon as possible. Positions are typically for 2-3 years (up to negotiation).
To apply, please send the following documents to Dominique Unruh:
The Chair of Software and Security (Prof. Bertrand Meyer) at the newly created Schaffhausen Institute of Technology has open positions for both PhD students and postdocs. We are looking for candidates with a passion for reliable software and a mix of theoretical knowledge and practical experience in software engineering. Candidates should have degrees in computer science or related fields: a doctorate for postdoc positions, a master’s degree for PhD positions. Postdoc candidates should have a substantial publication record. Experience in one or more of the following fields is a plus:
Compensation at both levels is attractive. Note that the PhD program is conducted in cooperation with partner universities.
Interested candidates should send a CV and relevant documents or links to Prof. Bertrand Meyer. They are also welcome to contact Prof. Bertrand Meyer for details.
The position is part of a new initiative in verified software supported by generous funding from Oracle. Initially, this will involve playing a leading role in research on verifying optimization passes of compilers. For the first three years, the position will have half the standard teaching duties allowing a greater focus on research and support for two PhD student scholarships and travel for research collaboration.
The primary purpose of this positions is to engage in teaching and research activities in Software Engineering, and play a pivotal role in developing software verification technology in the context of programming language implementation and to contribute to teaching, in Software Engineering and other related areas, course coordination and student supervision.
This position is located at our picturesque St Lucia campus, renowned as one of Australia’s most attractive university campuses, and located just 7km from Brisbane’s city centre. Bounded by the Brisbane River on three sides, and with outstanding public transport connections, our 114-hectare site provides a perfect work environment – you can enjoy the best of both worlds: a vibrant campus with the tradition of an established university.
Our Ideal Candidate
You should possess a PhD in Computer Science or Software Engineering, or a related field. You should have significant experience and a successful record of research achievements in areas including compilers, in particular, their optimization techniques, program analysis, semantics of programming languages, formal verification methods in programming, and the semantics of programming languages.
You should also possess a demonstrable capacity for teaching at both the undergraduate and postgraduate level, experience in postgraduate supervision and experience liaising with industry and external partners.
We value diversity and inclusion, and actively encourage applications from those who bring diversity to the University. Our Diversity and Inclusion webpage contains further information if you require additional support. Accessibility requirements and/or adjustments can be directed to recruitment@uq.edu.au.
What We Can Offer
This is a full-time continuing position at Academic level C/D. The full-time equivalent base salary will be in the range $117,319 – 135,276 for Level C and $141,261 – 155,627 for Level D plus super of up to 17%.
For further information see the following link.
Markus Kroetzsch and his colleages are looking towards a number of new job openings in their group at TU Dresden, in several projects. If you are seeking a fully funded research position in knowledge representation, AI, databases, or related areas, please feel free to contact him informally for further details. See here for more of their work and people.
Specifications:
Official, university-stamped job adverts will appear in due course.
Applications are invited for a postdoctoral position at the University of Minnesota related to an NSF-funded project entitled "A Higher-Order Framework for Meta-Theoretic Reasoning." The position is available immediately and is expected to be of duration of one to two years. Applications will be reviewed and acted upon as soon as they are received.
The project within which the appointment is to be made concerns the further development of a proof environment for reasoning about relational specifications that supports the so-called higher-order abstract syntax approach. A key component of this environment is the Abella proof assistant, which is based on a logic that incorporates a treatment of fixed-point definitions. One thrust for ongoing work is the enhancement of the underlying logic, for example through the addition of predicate quantification. The research group is also interested in building into the Abella system the capability to reason about specifications written in linear logic and dependently typed lambda calculi, and in investigating the benefits of the system in tasks such as compiler verification.
To participate successfully in the research described above, you would need to be broadly conversant with the areas of computational logic and programming languages and to have the mathematical and programming skills necessary for conducting original work in these areas. Prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as induction and co-induction, and familiarity with issues related to proof search in sequent calculi and other similar logical systems would help in engaging immediately with the research problems of interest.
To view the official announcement for this position, please visit this URL. This site also provides details such as the required qualifications for the position and serves as the portal for applications. To complete an application, you would need to submit a letter indicating your interest in the position, a current CV, one or two papers broadly related to the topics of research and the names and contact details of two people who are willing to serve as your references in the review process.
Please do not hesitate to contact Gopalan Nadathur if you have an interest in the position but would like answers prior to applying to questions related to matters such as the expectations, possible projects, and the suitability of your qualifications for the position.
The Institute of Information Security (the groups of Prof. Adrian Perrig and Prof. David Basin) and the Programming Methodology Group (Prof. Peter Müller) at ETH Zurich have multiple open positions for PhD students and Postdocs in a research project in the area of digital trust. The goal of this project is to develop a comprehensive, formally verified security architecture for communication in the physical and digital world. In particular, the project will develop protocols to transfer physical trust relationships into the digital world and store, manage, and use them. The design will take into account human (mis-)behavior from the outset. A particular emphasis is on the formal verification of the architecture both at the design and implementation level to rule out any undesired behavior.
We are looking for enthusiastic and outstanding Computer Science or Mathematics students and postdoctoral researchers with a strong background in some of the following topics:
ETH Zurich regulations require PhD students to hold a Masters or equivalent degree (e.g., Diplom). All candidates matching the profile above are encouraged to apply as soon as possible. We will process applications until all positions are filled. Successful candidates are expected to start soon after acceptance, but the starting date is negotiable.
Applications should include:
PhD students and Postdocs are paid employees of ETH Zurich. Salary and employment conditions are attractive. Zurich is a diverse and multicultural city which is consistently rated among the best cities in the world in which to live.
This is an announcement for two postdoctoral positions at ENS de Lyon, France.
These positions are funded by the ERC project CoVeCe.
This project covers fields such as
To apply, send an email to Damin Pous with your motivations (which part(s) of the project you would like to be involved in, why...), a brief CV, and the names of two persons who could recommend you. Please feel free to engage into a scientific discussion, or to ask me for more details about the project, the surrounding team (Plume), the lab (LIP), or Lyon's city.
The Department of Computer Science at Bucknell University seeks applications for two tenure-track positions at the Assistant Professor level in computer science beginning August 2020. We are interested in applicants working in any area of computer science, most particularly in those with research areas that expand the range of expertise in the department or that may lead to interdisciplinary collaborations. A PhD is required for this position. Candidates in the final stages of completing their doctoral work will be considered.
We seek candidates who will contribute to the teaching of courses in theoretical aspects of computer science or programming languages design, and core courses in our degree programs. Candidates will have opportunities to develop elective courses in their areas of expertise. We expect that candidates will develop a vigorous scholarly program that creates opportunities for student participation.
The department offers a BA and two ABET accredited BS programs, one in Computer Science and another in Computer Science and Engineering. We have a firm commitment to diversity, equity, and inclusion and to student-centered teaching. Our computing environment is Linux/Unix-based. More information about the department can be found here.
Review of applications will begin on November 1 and continue until the positions are filled. Candidates are asked to submit a cover letter, CV, a statement of teaching philosophy, a statement of research interests, a statement describing any past experience, training, or engagement with issues of diversity, equity, and inclusion, and three confidential letters of recommendation. Applications are only accepted through http://jobs.bucknell.edu. Questions should be directed to Professor L. Felipe Perrone, Chair of Computer Science (perrone@bucknell.edu).
About Bucknell
Bucknell University is a private, highly ranked, primarily undergraduate, national liberal arts institution that also offers strong professional programs in engineering, management, education, and music.
Bucknell University is an Equal Opportunity Employer. The university believes that students learn best in a diverse, inclusive community and is therefore committed to academic excellence through diversity in its faculty, staff, and students. Applications from members of groups that have been historically underrepresented in higher education are encouraged.
Bucknell is committed to creating a climate that fosters inclusion, growth, and development for a diverse student body, and seeks candidates who are also committed these goals.
Bucknell is committed to supporting the teacher-scholar model of faculty development. The teaching load is 5 courses per year. With a student-faculty ratio of about 9:1, small class sizes are a hallmark of the Bucknell educational experience. The university sponsors a range of activities to support the development of its faculty, including a Teaching-Learning Center and generous research support and leave policies.
Bucknell is located in Lewisburg, Pennsylvania, on the banks of the Susquehanna River. The Lewisburg area offers a combination of outdoor recreation opportunities and small-town amenities. In addition to the cultural and athletic events offered at the University and in town, the region offers strong schools and medical facilities, and an affordable cost of living. Bucknell is about three hours from Philadelphia, New York, Baltimore, and Washington, D.C.
There is an opening for a fully funded three-year PhD position (E-13 on the German TV-L scale, full time, no teaching obligation) at Friedrich-Alexander-Universität Erlangen-Nürnberg, located at the Chair of Theoretical Computer Science. The position is within the new DFG project "Coalgebraic Model Checking", with Stefan Milius and Lutz Schröder as PIs and with Daniel Hausmann collaborating on a second project position. The aim of the project is to develop a generic framework for model checking a wide variety of logics beyond the standard relational setting, such as probabilistic, graded, or alternating-time logics, based on the successful paradigm of coalgebraic logic.
The position is embedded into a large and active research group with a highly collaborative spirit. Erlangen's technical campus is situated within pleasant Franconia, and close to the vibrant city of Nuremberg. Please send applications or further inquiries to the PIs, Stefan Milius or Lutz Schröder.
Royal Holloway, University of London is looking for a postdoctoral research assistant to work on the EPSRC-funded project "String Constraint Solving with Real-World Regular Expressions" (EP/T00021X/1).
Project and Application Background
The successful applicant will contribute to the development of constraint satisfaction algorithms for string constraints using "real-world" regular expressions. That is, regular expressions using features such as capture groups and back-references that are not normally considered by theoretical research. In addition, the handling of length constraints represents a significant challenge.
The work will build upon the OSTRICH tool, which will be integrated with the JavaScript symbolic execution framework ExpoSE.
Ideal applicants will have a strong background in computer science or related areas and experience in at least one of logic, algorithms, programming language theory/implementation, formal language theory, and formal verification.
Research Environment
The project is led by Dr. Matthew Hague in the Department of Computer Science. It will proceed in close collaboration with Prof. Dr. Johannes Kinder (Bundeswehr University Munich), Prof. Dr. Anthony W. Lin (Kaiserslautern), and Dr. Philipp Rümmer (Uppsala). In addition, we will also collaborate with Prodo.dev in London.
Contact For informal enquiries please contact Matthew Hague. To apply, please visit this web page.
The School of Computing in the Faculty of Arts and Science at Queen's University invites applications for a Tenure-track faculty position at the rank of Assistant or Associate Professor in Software Engineering with a preferred starting date of July 1, 2020. In the case of an exceptional candidate, a tenured appointment at the rank of Associate Professor would be considered. All areas of Software Engineering are welcome. The following areas are of particular interest: Software Engineering with and for AI and Machine Learning, DevOps, Performance Engineering, Program Analysis, Testing and Software Quality.
The successful candidate must have a PhD or equivalent degree in Computer Science, Software Engineering or a related discipline completed at the start date of the appointment. The successful candidate is expected to play a major role in the delivery of graduate and undergraduate programs at the School of Computing. The main criteria for selection are academic and teaching excellence. The successful candidate will provide evidence of high quality scholarly output that demonstrates potential for independent research leading to peer-assessed publications and the securing of external research funding, as well as strong potential for outstanding teaching contributions at both the undergraduate and graduate levels, and an ongoing commitment to academic and pedagogical excellence in support of the School's programs. Candidates should demonstrate an ability to work collaboratively in an interdisciplinary and student-centred environment. The successful candidate will be required to make substantive contributions through service to the School, the Faculty, the University, and/or the broader community. Excellent interpersonal skills and exceptional oral and written communication proficiency are required. Salary will be commensurate with qualifications and experience. This position is subject to final budgetary approval by the University.
Queen's University is one of Canada's leading research-intensive universities. We are focused on being the quality leader in Canadian higher education and are dedicated to promoting research and scholarship of national and international distinction. The School of Computing has 29 full-time and 20 cross-appointed faculty, over 500 undergraduate students, and over 140 graduate students. The School offers undergraduate programs in Computer Science, Software Design, Biomedical Computing, Computing and Mathematics, Computing and the Creative Arts and Cognitive Science. The School also offers Master’s and Doctoral programs in Computer Science.
Queen's University is one of the oldest universities in Canada and has a global reputation for teaching and research excellence. The main campus is located within walking distance to the vibrant downtown area. Kingston is on the shore of Lake Ontario and near the Thousand Islands region of south-eastern Ontario. Kingston and the surrounding region boast a wide range of recreational opportunities and a rich arts and cultural community. In addition to Queen's University, Kingston is home to St. Lawrence College and the Royal Military College of Canada.
Additional information about Queen’s University, which may be of interest to prospective faculty members, can be found here.
The University invites applications from all qualified individuals. Queen's is committed to employment equity and diversity in the workplace and welcomes applications from women, visible minorities, Aboriginal peoples, persons with disabilities, and LGBTQ persons. All qualified candidates are encouraged to apply; however, in accordance with Canadian immigration requirements, Canadian citizens and permanent residents of Canada will be given priority.
To comply with federal laws, the University is obliged to gather statistical information as to how many applicants for each job vacancy are Canadian citizens / permanent residents of Canada. Applicants need not identify their country of origin or citizenship; however, all applications must include one of the following statements: "I am a Canadian citizen / permanent resident of Canada"; OR, "I am not a Canadian citizen / permanent resident of Canada". Applications that do not include this information will be deemed incomplete.
A complete application consists of:
The deadline for applications is October 31, 2019.
Applicants are encouraged to send all documents in their application packages electronically as a single PDF, to the Chair of Faculty Search Committee; alternatively, hard copy applications may be submitted to:
Faculty Search Committee Chair
The School of Computing
557 Goodwin Hall
Queen’s University
Kingston, Ontario K7L 3N6
CANADA
The University will provide support in its recruitment processes to applicants with disabilities, including accommodation that takes into account an applicant’s accessibility needs. If you require accommodation during the interview process, please contact Tom Bradshaw in the School of Computing.
Applications for a short-term programming internship at the University of Bergen are sought. The internship will happen in the context of the project "Automated Theorem Proving from the Mindset of Parameterized Complexity Theory".
The internship is open for students enrolled in a Master's or Ph.D. program in computer science, anywhere on earth.
Prospective applicants should have excellent programming skills in C++ and an excellent background in algorithms. Proficiency in automata theory is a great advantage.
Main activity:
The main activity will be the implementation of new parameterized
algorithms in the
field of automata theory. The language of use is C++.
Depending on your interests, you may also choose to be involved in the process of writing research papers related to the topics of the internship. Applicants with interest in writing scientific work will be given preference.
Requirements:
Financial support: We will reimburse expenses with the following:
Duration:
The ideal duration of the internship is 1 month. Slightly longer stays
are also possible.
Starting-Finishing Dates:
Flexible. Two ideal periods are specified below. But feel free to
suggest other dates, if the
suggested ones do not work for you.
Application: If the internship described above sounds interesting to you, please send the following information, in a single PDF file, to Mateus Oliveira. Please write INTERNSHIP in the subject field.
Deadline: We will start to review applications on 15 October. But applications will be accepted on a continuous base until the internship positions are filled.
For further questions, get in touch with Mateus Oliveira.
We invite applications for this full-time professorship until December 1. This full-time, permanent position is affiliated to the Institute of Logic and Computation at the Faculty of Informatics. The estimated starting date is in October 2020.
Research Area
The focus of this professorship lies on techniques and tools for Artificial Intelligence systems. Potential research topics include:
Profile
The successful candidate will have an outstanding academic record in Artificial Intelligence, in particular techniques and tools of AI Systems.
Essential Qualifications
Desirable Qualifications
We offer
Salary
In accordance with the Austrian Collective Agreement for University Staff, this position offers an annual minimum salary of € 71,822.80. The actual salary will be negotiated between the successful candidate and TU Wien and commensurate to his or her qualifications.
Application
Applications have to be addressed to Prof. Dr. Hannes Werthner, Dean of the Faculty of Informatics, sent as a single PDF and include:
TU Wien is committed to increasing female employment in leading scientific positions. Female applicants are explicitly encouraged to apply. Preference will be given to female applicants when equally qualified. People with special needs with appropriate qualifications are encouraged to apply. In case of queries, please contact the representative of people with disabilities of TU Wien, Mr. Gerhard Neustätter. Child care breaks will be handled in the same manner as in the ERC regulations for principal investigators applying to the Starting Grant.
Please note that the legally binding announcement of this position can be found in TU Wien’s University Gazette.
Two three-year post-doc positions in Semantics and Descriptive Complexity at Oxford and Cambridge.
There are two post-doctoral research positions open, one at Oxford and one at Cambridge, to work on a new EPSRC-funded project on "Resources and co-Resources: A junction between semantics and descriptive complexity" which is jointly led by Prof. Samson Abramsky FRS at Oxford, and Prof. Anuj Dawar at the University of Cambridge.
The positions are available to start as soon as possible, and are funded for 36 months.
The project seeks to explore ways in which methods from the study of logic and algorithms (specifically finite model theory and descriptive complexity) can be combined with methods from semantics (such as category theory) to build a cohesive algebraic theory of resources. This builds on recent work obtaining categorical accounts of essential constructions in finite model theory (by Abramsky, Dawar and Wang and Abramsky and Shah), as well as categorical accounts of quantum resources (by Abramsky, Barbosa, de Silva and Zapata). This work made essential use of monads -- seen as encapsulating quantum and other resources -- and of comonads, which encapsulate “coresources”, i.e. ways of limiting access to a structure corresponding to definability in various logics. The project will seek to apply these new tools to major results in descriptive complexity, to expand them to cover other important constructions, to find ways of combining accounts of quantum resources and logical co-resources, and to build a general theory of these.
There are separate application processes for applying for the two positions. Details of these and further information may be found at these webpages here and here.
For further questions or enquiries, contact Prof. Samson Abramsky or Prof. Anuj Dawar.
We are seeking applications for a fully-funded, 4-year PhD position in the Section of Theoretical Computer Science of the Vrije Universiteit Amsterdam (VUA). The goal of the project is the development of techniques for reasoning about automata that transform finite and infinite words (also known as transducers). For more details about the project, please check out here, and here. In this project, we will use and extend techniques from automata theory, combinatorics on words, logic, coalgebra and term rewriting.
Embedding
The principal investigator of this project is Joerg Endrullis with a background in term rewriting and automata theory. We will collaborate with Helle Hansen from Delft University of Technology (TU Delft) having expertise in logic and coalgebra. At the Vrije Universiteit Amsterdam we will collaborate with Femke van Raamsdonk with a background in higher-order rewriting, and Jasmin Blanchette working on formal verification and theorem provers.
Qualifications
Applicants should have a masters degree in computer science, mathematics, logic, or a closely related area. Knowledge of automata theory, coalgebra, logic, term rewriting or lambda calculus is considered an advantage. Fluency in English is important. Dutch language proficiency is not required.
Application
Please send applications by email to dr. Joerg Endrullis (+31 (0)20 5989886)
For more details on the salary and employment conditions, see the full vacancy text. Feel free to contact us for further information about the project and the position.
Formal applications must include:
Deadline
Review of applications will begin on December 1, 2019, and will continue until the position is filled.
Multiple positions are available at the Open University of The Netherlands and the Systems Software Research Group at Virginia Tech on projects on formal methods and reverse engineering of binaries. We are interested in decompilation: retrieving source code from a binary while maintaining a formal correctness proof that everything is sound. This will make bottom-up formal verification possible: applying formal verification to binaries, instead of to source code. If you have an interest in one of the fields of formal methods, (de)compilation, low-level assembly code or reverse-engineering, then you must certainly apply. We can hire both ''promovendi'' (PhD students) and postdocs on this project. Unique about the project is:
Applications can be done by sending your CV and a short application letter indicating your interest in the project via e-mail. For more information, see here.
The Section on Formal Methods for Safe and Secure Systems at the Department of Applied Mathematics and Computer Science (DTU Compute) of the Technical University of Denmark invites applications for an Associate/Assistant Professor in Formal Methods for Safe and Secure Systems.
Apply online and find details.
Application deadline: November 30th, 2019
Starting date: The position is available from July 1, 2020 or according to mutual agreement.
The section for Formal Methods of DTU Technical University of Denmark offers a PhD position funded by the Danish project ‘REDUCTO: A novel approach for the reduction of Boolean networks’.
The student will be supervised by PI of the project, Associate Professor Andrea Vandin, and by the head of section Alberto Lluch Lafuente in collaboration with
Apply online here
Project Description
Boolean networks (BN) are a graph-based well-established method to model biological systems. In order to accurately model systems, we often face models too complex to be interpreted or analyzed. Several reduction techniques exist to mitigate this problem. Our crucial hypothesis is that novel approaches to the reduction of BNs are needed, and that those can be developed by using a theoretical computer science approach. The project aims at developing novel mathematically-grounded techniques and tools to reduce and simplify complex BNs. The starting point will be recent work of the PI, presented e.g. in:
Several postdoc positions available in Sergei Ilya's group at School of Computing of National University of Singapore in the new project CertiChain, funded by NSOE-TSS. The positions are initially for two years with a possibility of extension.
The CertiChain project focuses on mechanising safety, liveness, and probabilistic security properties of distributed protocols, with a specific focus on Nakamoto-style consensus. I am looking for motivated candidates with a strong, internationally competitive research track record and research expertise in:
More details on the project can be found by this link below.
The NUS School of Computing is one of the world-leading departments in the areas of programming languages, software engineering, distributed systems, security and privacy. It provides a diverse and welcoming environment. Salaries at NUS are internationally competitive.
Do not hesitate to get in touch with Sergey Ilya if you are interested.
The Department of Electrical Engineering and Computer Science, Lassonde School of Engineering invites applications for a tenure track, professorial stream position in Software Engineering at the rank of Assistant Professor. The appointment will commence on July 1, 2020, subject to budgetary approval. We look for outstanding candidates in any area within Software Engineering, with a preference for those with expertise in formal method.
For details please see here
The Max Planck Institutes for Informatics (Saarbruecken), Software Systems (Saarbruecken and Kaiserslautern), and Security and Privacy (Bochum) invite applications for tenure-track faculty in all areas of computer science. Pending final approval, we expect to fill several positions.
A doctoral degree in computer science or related areas and an outstanding research record are required. Successful candidates are expected to build a team and pursue a highly visible research agenda, both independently and in collaboration with other groups.
The institutes are part of a network of over 80 Max Planck Institutes, Germany's premier basic-research organizations. MPIs have an established record of world-class, foundational research in the sciences, technology, and the humanities. The institutes offer a unique environment that combines the best aspects of a university department and a research laboratory: Faculty enjoy full academic freedom, lead a team of doctoral students and post-docs, and have the opportunity to teach university courses; at the same time, they enjoy ongoing institutional funding in addition to third-party funds, a technical infrastructure unrivaled for an academic institution, as well as internationally competitive compensation.
We maintain an international and diverse work environment and seek applications from outstanding researchers worldwide. The working language is English; knowledge of the German language is not required for a successful career at the institutes.
Qualified candidates should apply on our application website. To receive full consideration, applications should be received by December 15th, 2019.
The Max Planck Society wishes to increase the number of women in those areas where they are underrepresented. Women are therefore explicitly encouraged to apply. The Max Planck Society is also committed to increasing the number of employees with severe disabilities in its workforce. Applications from persons with severe disabilities are expressly desired.
The initial tenure-track appointment is for five years; it can be extended to seven years based on a midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.
The Computer Science and Engineering Department of the Instituto Superior Técnico (ULisboa) is carrying out an open search process for possible candidates to future openings for faculty career positions. This open search is targeted at possible candidates who have an interest in enrolling at the base level of the university professional career (assistant professor), in all scientific areas of the Department, namely:
Possible candidates should send to this email address a zip file containing the following materials:
The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with:
The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library.
This is the first release with polymorphic THF (TH1) problems. There are 644 polymorphic TH1 problems in 14 domains.
TPTP v7.3.0 is now available here. The TPTP-v7.3.0.tgz file contains the library, including utilities and basic documentation. Full documentation is online.
The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user, and be kept informed of such developments, please email Geoff Sutcliffe.
What's New in TPTP v7.3.0 Release v7.3.0, Fri Aug 2 16:17:10 EDT 2019
Changes from v7.2.0 to v7.3.0 for THF problems
Changes from v7.2.0 to v7.3.0 for TFA problems
Changes from v7.2.0 to v7.3.0 for FOF problems
Changes from v7.2.0 to v7.3.0 for CNF problems
In SyntaxBNF
VerifyThis is a program verification competition, which is annually held at ETAPS. During the competition, participants work for 90 minutes on relatively small but intriguing verification challenges.
With the VerifyThis Long-Term Challenge we would like to see how far the formal verification community can get within 6 months if they collaborate to verify a real-world software application.
The VerifyThis Long-Term Challenge is starting now, and it will be open until 29th of February, 2020. We would like to encourage everybody in the formal verification community to participate in this challenge, and to use their tools and technique to tackle parts of the challenges.
More information about the challenge is available here.
On this page, you can register your team, and subscribe to our mailing list. The mailing list will be used to for communication and collaboration between the participants, and it will allow you to stay up to date with the other teams' progress.
The results of the challenge will be presented during VerifyThis@ETAPS2020. In addition, we plan to prepare a special results with (individual and collaborative) solutions.
Welcome!
If this is the first time you receive this newsletter and you don't know why, the reason is most likely that you enjoyed great talks and a fun buggy ride at cade 2019. This makes you de facto a member of the Association for Automated Reasoning. That in turn means that from now on you will receive this newsletter. It is fairly low traffic, currently there is a new issue every three months or so.
In there you will find information relevant to the AR community at large, including among other things call for papers and job announcements. There are also columns contributed by various members of the AAR on topics of their choosing. If you want to contribute a column or advertise an event related to AR, you are welcome to do so. Just send me an email.
If you want to opt out, the one to contact is Philipp, the AAR secretary, that manages the list of members.