When I was a grad student in mathematics, the proofs I usually saw in class were what I think of as forward proofs. Such a proof begins with its assumptions, axioms of the field under study, and zero or more additional hypotheses.
In contrast to a forward proof, I cannot recall seeing in any of my graduate courses in mathematics what I term a backward proof. Such a proof begins with the denial of the theorem to be proved and works backward, eventually producing the negation (or denial) of some axiom or additional assumption for the theorem in focus. A so-called bidirectional proof also exists; again, I never saw one in my graduate mathematics courses. Such a proof includes statements some of which follow from axioms and, if present, hypotheses of the theorem in focus, while others follow from the denial or negation of the goal.
At this point I will concentrate on forward proofs, but the observations and challenges that follow apply also to so-called backward proofs and bidirectional proofs.
Implicit steps, demodulation, and automated reasoning
Often, many steps in a mathematical proof -- especially in a paper intended for publication -- are omitted from the proof.
The referee has to (in effect) guess at the missing steps, and sometimes the verification by the referee of the proposed proof is indeed difficult.
For a trivial example, applying associativity implicitly and repeatedly to obtain a third step from two others in a problem from group theory can present difficulty and can be easily overlooked.
Much subtler is the implicit use of some lemma or theorem proved earlier in the intended publication.
Such implicit and hidden aspects are often treated as obvious; that is, the parents may be cited, but other aspects are not.
In automated reasoning, the object that corresponds to such an implicit use in mathematics is a demodulator -- an equality that encodes, for example, associativity. In OTTER, such an equality is referenced by its number. And the number of demodulators cited with a single derived equation in the proof can make a huge difference in the reading of the proof. Let me give you an example.
Many years ago, William McCune (the developer of the automated reasoning program OTTER) proved the Robbins conjecture true -- that is, he produced a proof from a program he authored, a program different from OTTER. Among his other successes, some of the proofs he obtained with OTTER offered single lines depending on a large number of demodulators. When I showed that proof to the mathematician Ken Kunen, he commented that the huge set of demodulators, for a single line of the proof was too much to cope with. Indeed, he found the resulting equation difficult to verify because of so many implicit moves that were (in effect) made after the two parents were treated with paramodulation -- moves implicitly made because of many lines of numbers corresponding to demodulators.
Challenges in group theory
With this background, I now offer shortly several relevant challenges, challenges taken from group theory.
Since the axioms for a group are vital to the challenges issued here, I give these and the definition of commutator,
where the function f denotes product, the constant e denotes identity,
the function g denotes inverse, and the function h denotes commutator.
f(e,x) = x. % left identity
f(x,e) = x. % right identity
f(g(x),x) = e. % left inverse
f(x,g(x)) = e. % right inverse
f(f(x,y),z) = f(x,f(y,z)). % associativity
h(x,y) = f(x,f(y,f(g(x),g(y)))). % definition of commutator
In particular I focus on a theorem of Levi, in which he asserts the equivalence
of the following two properties in group theory, not assuming that either holds for all groups.
h(h(x,y),z = h(x,h(y,z)), commutator is associative, property 1
f(h(x,y),z) = f(z,h(x,y)), commutator has the property of nilpotent class 2, property 3
As it turns out, if I have been informed correctly, a third property (the following) is equivalent to each of the two cited properties.
f(h(x,z),h(y,z)) = h(f(x,y),z), commutator distributes over product, property 2
And now for the challenges.
In the first challenge I ask you to prove the equivalence of all three properties. In other words, find six proofs: prove property 2 from property 1, 3 from 1, 3 from 2, 1 from 2, 2 from 3, and finally 1 from 3.
In the second challenge, I ask you to find a circle of pure proofs for the three. Specifically, I am asking you to find a set of three proofs consisting of a proof that the second property follows from the first in which the third property does not occur; a proof that the third is provable from the second with the first not occurring in the proof; and a proof that the first is provable from the third with the second property excluded from the proof.
When and if you succeed, I offer more difficult challenges. In particular, for each of the six proofs you have found, you are to find (1) a forward proof, (2) a proof free of demodulators, and (3) a forward proof for each that is also free of demodulators. In cases in which the proof you may have found is backward or bidirectional, and in the case in which demodulators are present, I believe you will find that two rather disconnected procedures are required, one for producing a forward proof and one for removing demodulators.
A research challenge
For those of you ready to face a challenge that is more a type of research, I offer the following.
Specifically, you are asked to find methods to convert bidirectional or backward proofs to forward and to find a procedure to remove any and all demodulators from proofs that rely on such.
Should you wish some insight into the possible difficulty regarding demodulation removal, I include the following lines taken from a 197-step OTTER proof proving that property 1 implies property 3.
934 [back_demod,476,demod,809,383,383,383,797,797,797,797,797,797,418,418,
418,383,383,383,383,383,383,383,383,383,383,809,383,383,383,383,383,383,383,
383,383,383,383,383,383,383] f(h(x,h(y,z)),f(u,f(z,f(x,f(y,f(g(x),f(g(y),
f(g(z),f(y,f(x,f(g(y),f(g(x),g(u)))))))))))))=h(x,h(y,h(z,u))).
383,382 [] f(f(x,y),z)=f(x,f(y,z)).
797,796 [para_from,434.1.1,392.1.1.2,flip.1] g(f(x,y))=f(g(y),g(x)).
As line 934 indicates, the proof relies on 38 demodulators,
where 383 corresponds to the associativity of product, in the function f,
and 797 is a step occurring earlier in the proof, a step you might view as
a lemma if written out for a detailed paper being submitted for publication.
If you find six proofs each of which is a forward proof free of demodulation, I would very much enjoy the opportunity to examine that proof. My e-mail address is wos@mcs.anl.gov.
An extended version, including a list of publications, appears in Formal Aspects of Computing (2019)
Zohar Manna, founding father of the study and application of formal methods for software and hardware verification, died peacefully at his home in Netanya, Israel on August 30, 2018, after a long and marvelously productive career. He is survived by his wife Nitza and their four children and five grandchildren. He was 79.
Over a career spanning nearly half a century, Zohar had profound impact on most aspects of formal methods and automated reasoning. He was a deep thinker who laid the foundations for tools that are now coming into widespread use. He pioneered program verification and program synthesis, two fields that were then at the theoretical edge of computing, but which today help form the foundations of artificial intelligence and help assure the reliability of extraordinarily complex software. His work has inspired several generations of researchers. His manifold research interests included, in particular, the design and verification of concurrent, reactive and hybrid systems. His students and colleagues dedicated their research careers to the hardest problems in automated reasoning, including program semantics, partial correctness, termination, invariant generation, program synthesis, program transformation, planning, proof methodology, temporal reasoning, natural language understanding, non-clausal proof search, and decision procedures. Each of these activities is today a thriving independent field of research.
Zohar received his bachelor’s and master’s degrees in mathematics from the Technion in Haifa in 1961 and 1965, respectively, serving as a scientific programmer in the Israel Defense Forces from 1962 to 1964. Afterwards, he attended Carnegie Mellon University in Pittsburgh (together with one of us, Richard), where he earned his Ph.D. in computer science in the spring of 1968 under the guidance of Robert W Floyd and Alan J. Perlis both Turing Award recipients. Upon graduating CMU, Zohar joined Stanford University as an assistant professor of computer science, where, among other activities, he worked with John McCarthy. Zohar returned to Israel in 1972 to the Department of Applied Mathematics at the Weizmann Institute of Science in Rehovot, first as an associate professor and from 1976 on as full professor (where he supervised the dissertation of the other one of us, Nachum). In 1978, he was recruited back to Stanford as a full professor (taking Nachum along with him), dividing his time between Stanford and Weizmann until 1995, at which point he resigned the latter appointment. He remained at Stanford University until his retirement in 2010.
Zohar’s 1968 dissertation, entitled Termination of Programs, used second-order logic to formalize the problem of termination for abstract programs and demonstrate decidable subclasses of the termination program. Whereas Floyd’s own approach to termination required the invention of inductive assertions and well-founded orderings, Zohar’s approach made stronger demands on the theorem prover, which had to be second order. Richard Lipton calls it “one of the coolest PhD theses ever.” He authored or coauthored 9 books and close to 200 scholarly articles, plus more than 50 technical reports (Weizmann, Stanford, SRI), which served as a rapid mode of dissemination of pre-publication cutting-edge research. All are all models of clarity and comprehensiveness. His magnificent textbook, Mathematical Theory of Computation (1974), was extraordinarily influential; it was translated into Bulgarian, Czech, Hungarian, Italian, Japanese, and Russian. It pioneered the logical analysis of programs for correctness vis-à-specifications and for termination properties. For very many of today’s computer scientists, this book was their introduction to formal methods.
Richard Waldinger was Zohar’s chief collaborator on program synthesis. In 1970, they published a groundbreaking paper, “Toward automatic program synthesis” (CACM ). Eventually they moved to a purely “deductive” approach in which, to construct a program meeting a desired condition for a given input, one proves the existence of an output entity that satisfies that condition. The proof is restricted to be sufficiently constructive so that a program that computes the satisfying output can be extracted. Conditional expressions are introduced via case analysis in the proof; recursion is introduced by application of recursion induction. Perhaps the most practical application of deductive program synthesis came from its use by NASA in the Amphion project, which synthesized programs for analysis of data from interplanetary missions. Zohar and Richard also developed a non-clausal reasoner that better served the need for doing an inductive proof in a resolution-theorem-proving framework. This collaboration culminated in the two-volume book, The Logical Basis for Computer Programming (1985 and 1990).
Zohar played a central rôle in the study of applications of temporal logic. His most cited works are on the formal analysis of reactive systems, much of which was done in collaboration with Amir Pnueli. In the late seventies, the two of them embarked on their seminal study of applications of temporal modal logics to verification of concurrent programs. This long-term collaboration culminated in two landmark volumes and in the STeP prover.
Zohar was universally acclaimed and deeply appreciated as a consummate teacher. Even as a graduate student, his first talk, describing his thesis research, was polished and professional. The courses he taught include “Logic and Automated Reasoning” and “Formal Methods for Concurrent and Reactive Systems.” Moshe Vardi has divulged that “His course was one of my favorite all-time computer science courses. It convinced me that logic has a real place in computer science.”
When Nachum took Zohar’s course at Weizmann in 1974, Mathematical Theory of Computation was in galley proofs, and exercises were assigned from them. Besides laboring to solve the problems, Nachum would take pleasure in proofreading for errors and typos, for which Zohar was quite grateful. Later, when preparing their textbooks, Zohar and Richard would give students handouts in which three small errors had been deliberately introduced into each chapter. As part of their homework, students were asked to find these errors. If they found more than the three, so much the better. This worked well as long as Zohar and Richard kept good records of where the errors had been secreted, so they could be removed prior to publication. For several years, students would read successive versions of the manuscript, sprinkled with deliberately introduced errors.
Zohar’s international cachet is reflected in the honors he accrued, including: the ACM Programming Systems and Languages Award (1974); a Guggenheim Fellowship (1981); the F. L. Bauer Prize from the Technical University Munich (1992); Fellowship in the ACM (1993); doctor honoris causa from École nor- male supérieure de Cachan (2002); and a Fulbright Fellowship (2002). In 2016, he (together with Richard Waldinger) received the Herbrand Award for Distinguished Contributions to Automated Reasoning from CADE “for his pioneering research and pedagogical contributions to automated reasoning, program synthe- sis, planning, and formal methods.” He was also associate editor of Acta Informatica and of Theoretical Computer Science and a board member of the International Institute for Software Technology of the United Nations University in Macao. His fifty coauthors and collaborators read like a computer-science hall of fame. When he turned sixty-four in 2003, many of his graduate students, research collaborators, and computer- science colleagues gathered in Sicily for a symposium on subjects related to Zohar’s manifold contributions in the field. Their breadth and depth serve as a tribute to Zohar’s lasting impact on the field. In addition, a liber amicorum was prepared in tribute: Verification – Theory and Practice (2003).
From the point of view of the success of academic descendants in computer science, Zohar ranked #2 in the list of “The Best Nurturers in Computer Science Research” (B. Kumar M. and Y. N. Srikant, SIAM International Conference on Data Mining, 2015). He took immense pride in his students and their spiritual heirs. All told, he supervised thirty doctoral students (and has close to 300 Ph.D. descendants). Zo- har and his students developed powerful methods for theory of computation (Cadiou, Chandra, Vuillemin, Shamir), program verification (Katz, Chang, Kapur, de Alfaro, Bjørner, Uribe, Sipma, Finkbeiner, Colón, Sankaranarayanan, Slanina, Bradley), program transformation and synthesis (Dershowitz, Scherlis, Wolper, Anuchitanukul), temporal and real-time logics (Moszkowski, Abadi, Alur, Henzinger, McGuire, Sánchez), logic programming (Malachi, Baudinet), and theorem proving (Zarba, Zhang, Bradley). Zohar’s students all recount how much more than just superb academic guidance they received from him. Each has volumes of tales to tell of the sound advice, sage counsel, joie de vivre, and the vibrant example of both hard work and great play set by Zohar. Zohar’s devotion to his students is legendary. 2When the Dershowitzes first arrived at Stanford, Zohar was out of town. Nitza collected Nachum and wife, Schulamith, from the San Francisco airport at 3 a.m. Zohar and Nitza proceeded to host the newlywed couple at their home until they found a place for themselves. Another example of Zohar’s unsung generosity is this acknowledgment by Marin Vlada (now a professor of computer science at the University of Bucharest): “I must also thank Professor Manna who in 1977 sent me [his book and several scientific articles]. I was a student, and I used everything he sent me to advance my undergraduate work. I must admit that I was very surprised by his kindness, considering that Romania is separated from the U.S.A. by a very large ocean. . . . Thank you very much sir!”
Zohar and Nitza’s children recall a house full of life and guests, and Friday night family dinners, but most of all, they remember the family camping trips. They toured the world extensively, paying special attention to nature reserves and beaches. There are dozens of albums with Zohar’s exquisite photography, another one of his many talents. A more mathematical talent of Zohar’s was counting cards at blackjack, leading to his being blacklisted by some casinos. “He laughed that it was one of his greatest achievements,” his son recalls. Above all, family and friends remember a person who enjoyed the fullness of life, was humble despite his accomplishments, and was devoted to all who came into his orbit. He will be sorely missed.
An election was held from November 16 to November 30 2019 to fill four positions on the board of trustees of CADE, Inc.
Six candidates were nominated (in alphabetical order): Maria Paola Bonacina, Pascal Fontaine, Laura Kovács, Aart Middeldorp, Renate Schmidt, and Christoph Weidenbach.
The participants of the last three CADE/IJCAR conferences were invited to vote, and a total of 240 ballots were sent by electronic mail on November 16. By November 30, 83 valid ballots had been returned, which translates to a participation rate of 34.5% (as compared to 21.1% in 2018, 9.1% in 2017, 11.2% in 2016, 11.0% in 2015, 10.0% in 2014, 11.8% in 2013, 13.0% in 2012, 16.2% in 2011).
The four candidates elected are Pascal Fontaine, Laura Kovács, Aart Middeldorp, and Christoph Weidenbach.
The counting of the votes according to the single transferable vote algorithm described in the CADE Bylaws is detailed near the end of this newsletter.
After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:
On behalf of the AAR and CADE Inc., I would like to thank Jasmin Blanchette and Renate Schmidt for their service on the board of trustees since 2016, and Maria Paola Bonacina for running in the election.
Congratulations to Laura Kovács and Christoph Weidenbach, who were re-elected, and to Pascal Fontaine and Aart Middeldorp, who will join the board as new members!
In conjunction with the 2019 CADE trustee elections, a vote on a motion brought forward by the CADE trustees was held. The CADE trustees suggested to move from the CADE STV algorithm to a standard algorithm that is supported by automatic voting platforms, and to change the CADE 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.
The 240 ballots sent out to the CADE members on November 16 included a question about this change. By November 30, 84 valid answers had been sent back for the question, while one person preferred to abstain:
This means that more than 30% of the people voted on the question, and more than two-third voted in favor of the proposed change.
By Article IX of the bylaws, the change has therefore been accepted, and the bylaws have been updated accordingly.
Zulip is successfully used by the Lean community to communicate. It bridges the gap between long-form mailing lists and interactive messaging, with excellent support for threading (which allows to follow in-depth discussions without drowning in unrelated noise), streams and topics, and the convenience of quick messages and replies when needed.
We have an instance of zulip which is used for Matryoshka and Zipperposition development, and would like to open it further to the wider ATP community. Streams allow sub-communities to have their own space (e.g. a Vampire specific stream, or one for CASC). The lean zulip server demonstrates that good communication tools can help communities thrive, make it easier for newcomers to ask questions, and lower friction for discussions.
An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see: here, here and here.
The 2019 Alonzo Church Award was given jointly to Murdoch J. Gabbay and Andrew M. Pitts for their ground-breaking work introducing the theory of nominal representations. Previous awardees are listed here.
Eligibility and Nominations
The contribution must have appeared in a paper or papers published within
the past 25 years. Thus, for the 2020 award, the cut-off date is January 1,
1995. When a paper has appeared in a conference and then in a journal, the
date of the journal publication will determine the cut-off date. In
addition, the contribution must not yet have received recognition via a
major award, such as the Turing Award, the Kanellakis Award, or the Gödel
Prize. (The nominee(s) may have received such awards for other
contributions.) While the contribution can consist of conference or journal
papers, journal papers will be given a preference.
Nominations for the 2020 award are now being solicited. The nominating letter must summarize the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness.
Nominations should be submitted to Thomas Eiter by April 1, 2020.
Presentation of the Award The 2020 award will be presented at CSL 2021, the annual conference of the European Association for Computer Science Logic, which is scheduled to take place in Athens in January 2021. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared.
Award Committee
The 2020 Alonzo Church Award Committee consists of the following five members: Mariangiola Dezani, Thomas Eiter (chair), Javier Esparza, Radha Jagadeesan, Natarajan Shankar
Nominations are now invited for the 2020 Ackermann Award. PhD dissertations in topics specified by the CSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1.1.2018 and 31.12.2019 are eligible for nomination for the award.
The deadline for submission is 1 April 2020. Submission details follow below.
Nominations can be submitted from 1 January 2020 and should be sent to the chair of the Jury, Thomas Schwentick.
The Award
The 2020 Ackermann award will be presented to the recipient(s) at CSL
2021, the annual conference of the EACSL.
The award consists of:
The jury is entitled to give the award to more (or less) than one dissertation in a year.
The Jury
The jury consists of:
How to submit
The candidate or his/her supervisor should submit
Since 2002, the Association for Logic, Language, and Information (FoLLI) has been awarding the annual E.W. Beth Dissertation Prize to outstanding Ph.D. dissertations in Logic, Language, and Information, with financial support of the E.W. Beth Foundation. Nominations are now invited for the best dissertation in these areas resulting in a Ph.D. degree awarded in 2019.
The deadline for nominations is the 15th of April 2020.
Qualifications:
The prize consists of:
Only digital submissions are accepted, without exception. Hard copy submissions are not allowed. The following documents are to be submitted in the nomination dossier:
All pdf documents must be submitted electronically, as one zip file, via EasyChair. In case of any problems with the submission one should contact the chair of the committee Mehrnoosh Sadrzadeh.
The prize will be awarded by the chair of the FoLLI board at a ceremony during the 32nd ESSLLI summer school in University of Utrecht, August 3-14, 2020.
Beth dissertation prize committee 2020:
The TABLEAUX Steering Committee is now calling for bids to host the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods ("TABLEAUX") in 2021. TABLEAUX typically merges into IJCAR (the International Joint Conference on Automated Reasoning) in even years. Previous TABLEAUX/IJCAR conferences took place in London/UK (TABLEAUX 2019), Oxford/UK (IJCAR 2018), Brasília/Brazil (TABLEAUX 2017), Coimbra/Portugal (IJCAR 2016), Wrocław/Poland (TABLEAUX 2015), Vienna/Austria (IJCAR 2014), Nancy/France (TABLEAUX 2013), Manchester/UK (IJCAR 2012), Bern/Switzerland (TABLEAUX 2011), Edinburgh/UK (IJCAR 2010), and Oslo/Norway (TABLEAUX 2009). See here for a complete list of previous conferences.
A bid should cover at least the following aspects:
Bids that consider co-locating TABLEAUX with other conferences, such as FroCoS or ITP, are strongly encouraged. In 2013, 2015 and 2019 TABLEAUX was co-located with FroCoS (the International Symposium on Frontiers of Combining Systems) and in 2017 TABLEAUX was co-located with FroCoS and ITP (the International Conference on Interactive Theorem Proving).
The leader or leaders of the winning bid will become the Conference Chair or Co-Chairs of TABLEAUX 2021. Traditionally they will also become the PC Chair or Co-Chairs; the final decision on this will be made by the TABLEAUX Steering Committee. The PC Chair or Co-Chairs will create a PC in consultation with the TABLEAUX Steering Committee and will also be expected to edit the conference proceedings.
The bid should be limited to 10 pages and should be submitted as PDF file to Jens Otten.
The deadline for submissions is April 26th, 2020.
The TABLEAUX Steering Committee will decide which bid to accept and announce a decision as soon as possible after the deadline.
Perspective organizers are encouraged to register their intention informally and to get in touch with the TABLEAUX Steering Committee for informal discussion.
More information about the TABLEAUX conference and its history can be found here.
As a novelty this year, and additionally to the standard CfP, RAMICS is also calling for short contributions and posters. We are hence calling for presentations of original, unfinished, already published, or otherwise interesting work within the topics of the RAMICS conferences. The submission can be in the form of a poster, an abstract, a paper submitted to or published at another conference, etc. Short contributions will not be published in the conference proceedings.
Important Dates:
More information is available on the conference's web page.
The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world.
List of Topics:
New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to:
Important Dates
More information is available on the conference's web page.
TTCS is a bi-annual conference series, intending to serve as a forum for novel and high-quality research in all areas of Theoretical Computer Science. The conference is held in cooperation with the European Association for Theoretical Computer Science (EATCS). The proceedings will be published in the Springer LNCS series.
TTCS is organized in 2 tracks. Topics of interest include but are not
limited to:
Track A: Algorithms and Complexity
Important Dates
More information is available on the conference's web page.
The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the premier annual meeting for researchers focusing on the theory and applications of the propositional satisfiability problem, broadly construed. In addition to plain propositional satisfiability, it also includes Boolean optimization (such as MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning.
Scope
SAT 2020 welcomes scientific contributions addressing different aspects of the satisfiability problem, interpreted in a broad sense. Topics include, but are not restricted to:
Out of Scope
Papers claiming to resolve a major long-standing open theoretical question in Mathematics or Computer Science (such as those for which a Millennium Prize is offered), are outside the scope of the conference because there is insufficient time in the schedule to referee such papers; instead, such papers should be submitted to an appropriate technical journal.
Important Dates
More information is available on the conference's web page.
Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. The initiative consists of a conference series together with volumes based on the conferences. Information about the AiML series can be obtained here.
Topics
We invite submissions on all aspects of modal logic, including:
Dates
More information is available on the conference's web page.
Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information.
CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration.
CICM 2020 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to
Important Dates
More information is available on the conference's web page.
Knowledge Representation and Reasoning (KR) is a well-established and lively field of research. In KR a fundamental assumption is that an agent's knowledge is explicitly represented in a declarative form, suitable for processing by dedicated reasoning engines. This assumption, that much of what an agent deals with is knowledge-based, is common in many modern intelligent systems. Consequently, KR has contributed to the theory and practice of various areas in AI, including automated planning and natural language understanding, and to fields beyond AI, including databases, verification, software engineering, and robotics. In recent years, KR has contributed also to new and emerging fields, including the semantic web, computational biology, cyber security, and the development of software agents.
The KR conference series is the leading forum for timely in-depth presentation of progress in the theory and principles underlying the representation and computational management of knowledge.
Scope
We solicit papers presenting novel results on the principles of KR that clearly contribute to the formal foundations of relevant problems or show the applicability of results to implemented or implementable systems. We also welcome papers from other areas that show clear use of, or contributions to, the principles or practice of KR. We also encourage "reports from the field" of applications, experiments, developments, and tests.
Topics of interest include, but are not limited to:
Tracks
In addition to the main conference track, KR2020 will host the following tracks and sessions:
Important Dates
More information is available on the conference's web page.
RuleML+RR is part of "Declarative AI 2020: Rules, Reasoning, Decisions and Explanations" (DeclarativeAI 2020)
The 4th International Joint Conference on Rules and Reasoning (RuleML+RR 2020) is the leading international joint conference in the field of rule-based reasoning. Stemming from the synergy with the DecisionCAMP summit, which brings together leading decision management authorities, vendors, and practitioners, one of the main goals of RuleML+RR is to build bridges between academia and industry in the area of rule-based reasoning and applications.
RuleML+RR 2020 aims to bring together rigorous researchers and inventive practitioners, interested in the foundations and applications of rules and reasoning in academia, industry, engineering, business, finance, healthcare, environment, and other application areas. It provides a forum for stimulating cooperation and cross-fertilization between the many different communities focused on the research, development, and applications of rule-based systems.
Topics
RuleML+RR welcomes research from all areas of Rules and Reasoning, including topics from our 2020 theme: explainable algorithmic decision-making. The topics of the conference include:
Important Dates
More information is available on the conference's web page.
The ICALP and the LICS steering committee have agreed together with the conference chairs in Beijing to relocate the two conferences. ICALP and LICS 2020 will take place in Saarbrücken, Germany, July 8-11 (with satellite workshops on July 6-7).
We are very grateful to our colleagues in Beijing, for the organization so far, to the colleagues from Saarbrücken, who generously accepted this challenging task, and to all members of the TCS community who offered their help in this difficult situation.
ICALP (International Colloquium on Automata, Languages and Programming) is the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS). ICALP 2020 will be hosted on the Saarland Informatics Campus in Saarbrücken, in co-location with LICS 2020 (ACM/IEEE Symposium on Logic in Computer Science).
Topics:
ICALP 2020 will have the two traditional tracks A (Algorithms,
Complexity and Games - including Algorithmic Game Theory, Distributed
Algorithms and Parallel, Distributed and External Memory Computing) and
B (Automata, Logic, Semantics and Theory of Programming). Papers
presenting original, unpublished research on all aspects of theoretical
computer science are sought.
Typical, but not exclusive topics are:
Track A
Important Dates
More information is available on the conference's web page.
The ICALP and the LICS steering committee have agreed together with the conference chairs in Beijing to relocate the two conferences. ICALP and LICS 2020 will take place in Saarbrücken, Germany, July 8-11 (with satellite workshops on July 6-7).
We are very grateful to our colleagues in Beijing, for the organization so far, to the colleagues from Saarbrücken, who generously accepted this challenging task, and to all members of the TCS community who offered their help in this difficult situation.
MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.
Topics include, but are not limited to, the following:
Important Dates:
More information is available on the conference's web page.
Overview and Scope
SEFM aims to bring together leading researchers and practitioners
from academia, industry, and government, to advance the state of
the art in formal methods, to facilitate their uptake in the
software industry, and to encourage their integration within
practical software engineering methods and tools.
Topics of interest include, but are not limited to, the following aspects of software engineering and formal methods:
Important Dates
More information is available on the conference's web page.
Since the first conference held in Marseille in 1982, the International Conference on Logic Programming (ICLP 2020) has been the premier international event for presenting research in logic programming.
Scope
Contributions are solicited in all areas of logic programming, including but not restricted to:
Important Dates
More information is available on the conference's web page.
Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.
List of topics:
Important dates:
More information is available on the EACSL web page.
All the following events are affiliated with either IJCAR 2020 or FSCD 2020 and are part of the Paris Nord Summer of LoVe 2020, also including Petri Nets 2020.
The 9th International Workshop on Confluence (IWC 2020) aims at promoting further research in confluence and related properties. Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The workshop aims at promoting further research in confluence and related properties.
Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool supports, certification as well as new applications.
Topics
The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. IWC 2020 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research.
Important Dates
More information is available on the workshop's web page.
Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory.
The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory.
Submission Dates
More information is available on the workshop's web page.
The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilization of ideas from the different communities interested in termination (e.g., working on computational mechanisms, programming languages, software engineering, constraint solving, etc.). The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications.
Topics:
The 17th International Workshop on Termination welcomes
contributions on all aspects of termination. In particular, papers
investigating applications of termination (for example in complexity
analysis, program analysis and transformation, theorem proving, program
correctness, modeling computational systems, etc.) are very welcome.
Topics of interest include (but are not limited to):
Competition:
Since 2003, the catalytic effect of WST to stimulate
new research on termination has been enhanced by the celebration
of the Termination Competition and its continuously developing
problem databases containing thousands of programs as challenges
for termination analysis in different categories, see here.
In 2020, the Termination Competition will run shortly before WST and the main venues (IJCAR-FSCD), and the results will be presented at IJCAR or FSCD.
Important Dates:
More information is available on the workshop's web page.
The automation of logical reasoning is a challenge that has been studied intensively in fields including mathematics, philosophy, and computer science. PAAR is the workshop on turning this theory into practice: how can automated reasoning tools be built that work and are useful in applications? PAAR covers all aspects of this challenge: which theories, logics, or fragments are well-behaved in practice, and connect well to application domains? which reasoning tasks are tractable and useful? which algorithms are able to solve real-world instances? how should automated reasoning tools be designed, implemented, tested, and evaluated?
The goal of PAAR is to bring together theoreticians, tool developers, and users, to concentrate on the practical aspects of automated reasoning. The workshop welcomes high-quality contributions of any kind, including new research results, presentation of work in progress, presentation of new tools, new implementation techniques, new application domains, or case studies.
Topics include, but are not limited to:
Important dates
More information is available on the workshop's web page.
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems.
Topics of interest include:
Important Dates
More information is available on the workshop's web page.
The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.
Important dates
More information is available on the workshop's web page.
The Women in Logic workshop (WiL) provides an opportunity to increase awareness of the valuable contributions made by women in the area of logic in computer science. Its main purpose is to promote the excellent research done by women, with the ultimate goal of increasing their visibility and representation in the community. Our aim is to:
Topics of interest include but are not limited to:
Important Dates
[N.D.L.R: At the moment this newsletter is published, there seem to be no website for WiL 2020, hence I have also included the submission instructions below]
Submissions
Abstracts should be written in English (1-2 pages), and prepared using the Easychair style.
The abstracts should be uploaded to the WiL 2020 Easychair page as a PDF file before the submission deadline of April 22, 2020, anywhere on Earth.
UNIF 2020 is the 34th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of making two terms equal, finding solutions for equations or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc. Traditionally, the scope of the UNIF workshops has covered the topic of unification in a broad sense. Topics of interest to this forum include, but are not limited to:
The International Workshop on Unification (UNIF) is a yearly forum for researchers in unification theory and related fields to meet old and new colleagues, to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for young researchers and scientists working in related areas to get an overview of the state of the art in unification theory.
Important Dates
More information is available on the workshop's web page.
Symbolic Computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions.
The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces for tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop is to provide an opportunity to discuss, share knowledge and experience across both communities.
The topics of interest include but are not limited to:
Key Dates
More information is available on the workshop's web page.
This workshop brings together researchers of the ITP community to compete in a "proving contest".
While programming contests (e.g. ACM ICPC, International Olympiad in Informatics) challenge large numbers of participants to solve algorithmic problems within a short time, we envision proving contests to entice proof engineers to formally prove small but interesting problems from mathematics or computer science.
A [prototype contest system](https://competition.isabelle.systems/) is currently used for teaching and hosting proving contests in Coq, Isabelle, and Lean.
The workshop will be organized around an onsite contest, supplemented with informal discussions.
In order to conduct a stimulating contest we solicit interesting tasks.
A contest typically lasts for two hours and consists of around five problems with varying difficulty.
A problem:
Submissions from (potential) competition participants are allowed.
Examples can be found at the current "Proving for Fun" contest system, e.g. here.
Submissions can be made via email to Simon Wimmer by the date indicated below.
Important Dates
More information is available on the workshop's web page.
Non-classical logics – such as modal logics, conditional logics, intuitionistic logic, description logics, temporal logics, linear logic, dynamic logic, deontic logics, fuzzy logic, paraconsistent logic, relevance logic, free logic and natural logic – have many applications in AI, Computer Science, Philosophy, Linguistics and Mathematics. Hence, the automation of proof search in these logics is a crucial task.
The ARQNL workshop aims at fostering the development of proof calculi, automated theorem proving systems and model finders for all sorts of quantified, i.e. first- or higher-order, non-classical logics. The workshop will provide a forum for researchers to present and discuss recent developments in this area. These contributions may range from theory to system descriptions and implementations. Contributions may also outline relevant applications, describe problem formalizations, example problems and benchmarks. We welcome contributions from computer scientists, linguists, philosophers, and mathematicians.
Research papers (up to 15 pages), and short papers, talk abstracts, or system demonstrations (up to 8 pages) are solicited. The deadline for submitting papers is April 26th. Proceedings will be published in the CEUR Workshop Proceedings.
More information is available on the workshop's web page.
The Vampire 2020 workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas.
Important Dates
More information is available on the workshop's web page.
The DeMent 2020 workshop will provide mentoring and help on career development for young researchers working in automated reasoning, with the overall aim to attract and help them to establish themselves as researchers in automated reasoning. The workshop will address challenges of the academic life and give insight in industrial research. For doing so, the workshop will include talks from leading experts of automated reasoning in academia and industry, and will also include presentations on career-planning.
The workshop aims to reach and attract master students, PhD students and young postdocs as participants.
Important Dates
More information is available on the workshop's web page.
The aim of the workshop is to bring together researchers and users of SMT tools and techniques. Relevant topics include but are not limited to:
Important Dates
More information is available on the workshop's web page.
WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers.
Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are:
Important Dates
More information is available on the workshop's web page.
Collocated with ETAPS 2020.
The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as a formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends.
Important Dates
More information is available on the workshop's web page.
Collocated with ETAPS 2020.
GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials.
Areas of interest include:
Important Dates
More information is available on the workshop's web page.
Collocated with ETAPS 2020.
Logic programming is a framework for expressing programs, propositions and relations as Horn clause theories, with the purpose of performing automatic inference in these theories. Horn clause theories are famous for their well-understood declarative semantics, in which models of logic programs are given inductively or coinductively. At the same time, Horn clauses give rise to efficient inference procedures, usually involving resolution. Logic programming found applications in type inference, verification, and AI. While logic programming was originally conceived for describing simple facts, it was extended to account for much more complex theories. This includes higher-order theories, inductive and coinductive data, and stochastic/probabilistic theories.
The aim of this workshop is to bring together researchers that work on extensions of logic programming and inference methods, and to foster an exchange of methods and applications that have emerged in different communities.
Topics
The central idea of this workshop is to discuss the theory of logic
programming and associated topics that have as well the goal to
automatically infer knowledge and proofs. Our intention is to bring
together researchers that work on the numerous topics that contribute to
automatic proof inference and foster an exchange that may lead to advances
in the theory of logic programming.
Topics of interest include, but are not limited to, the following:
Important Dates
More information is available on the workshop's web page.
Collocated with ETAPS 2020.
Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses, and many recent advances in the Constraint/Logic Programming, Verification, and Automated Deduction communities have centered around efficiently solving problems presented as Horn clauses.
This workshop aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE), on the topic of Horn clause based analysis, verification and synthesis.
Horn clauses have been advocated by these communities at different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.
Aims and Scope
Topics of interest include but are not limited to the use of Horn
clauses, constraints, and related formalisms in the following areas:
Important dates
More information is available on the workshop's web page.
Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and programming languages, supporting tool development and reasoning.
Topics of Interest:
Topics of interest include, but are not limited to:
Important Dates:
More information is available on the workshop's web page.
Strategic reasoning is a key topic in multi-agent systems research. The extensive literature in the field includes a variety of logics used for modeling strategic ability. Results from the field are now being used in many exciting domains such as information system security, adaptive strategies for robot teams, and automatic players capable to outperform human experts. A common feature in all these application domains is the requirement for sound theoretical foundations and tools accounting for the strategies that artificial agents may adopt in the situation of conflict and cooperation.
The SR international workshop series aims at bringing together researchers working on different aspects of strategic reasoning in computer science, both from a theoretical and a practical point of view.
SR 2020 will be held with ECAI 2020.
Topics ef Interest:
The topics covered by SR include, but are not limited to, the following:
Important Dates:
More information is available on the workshop's web page.
Symbolic Computation is the science of computing with symbolic objects (terms, formulae, programs, representations of algebraic objects etc.). Powerful algorithms have been developed during the past decades for the major subareas of symbolic computation: computer algebra and computational logic. These algorithms and methods are successfully applied in various fields, including software science, which covers a broad range of topics about software construction and analysis.
Meanwhile, artificial intelligence methods and machine learning algorithms are widely used nowadays in various domains and, in particular, combined with symbolic computation. Several approaches mix artificial intelligence and symbolic methods and tools deployed over large corpora to create what is known as cognitive systems. Cognitive computing focuses on building systems which interact with humans naturally by reasoning, aiming at learning at scale.
The purpose of SCSS 2020 is to promote research on theoretical and practical aspects of symbolic computation in software science, combined with modern artificial intelligence techniques.
Scope
SCSS 2020 solicits submissions on all aspects of symbolic computation
and their applications in software science, in combination with
artificial intelligence and cognitive computing techniques. The topics
of the symposium include, but are not limited to the following:
Important Dates
More information is available on the workshop's web page.
The 1st International Competition on Model Counting (MC 2020) is a competition to deepen the relationship between latest theoretical and practical development on the various model counting problems and their practical applications. It targets the problem of counting the number of models of a Boolean formula. MC 2020 aims to identify new challenging benchmarks and to promote new solvers for the problem as well as to compare them with state-of-the-art solvers. The MC 2020 follows a direction in the community of constraint solving, where already many competitions have been organized such as on ASP (7 editions), CSP (19 editions), SAT (19 editions), SMT (14 editions), MaxSAT Evaluation (13 editions), QBF (8 editions). MC 2020 invites submission of collections of (weighted) model counting instances in the s tandard DIMACS-based submission formats as given at the competition tracks.
Submission Procedure
A benchmark submission should consist of a single zip or gzipped tar package,
containing the instance files and a description of the benchmarks. Please
use appropriate file naming conventions, where suited. Ideally, each instance
file name should contain a short descriptive part for the problem domain as
well as the parameters used for generating the instance as applicable.
The benchmark description must be submitted as PDF. The description
should include author information with affiliations, a description of the problem
domains, a description of the parameters used for generating the instances,
and the file name convention. References should be used as appropriate.
The benchmark descriptions will be posted on the MC 2020 website.
Furthermore, the organizers are considering publishing the collection of system
and benchmark descriptions on arxiv.
Deadline
Please submit benchmarks by email
using the subject title "MC 2020 benchmark submission" by March 5, 2020,
23:59 AoE the latest.
More information is available on the competition's web page.
Two MOOCs (massive open online courses) on Automated Reasoning have been launched at the platform for online courses Coursera. After entering name and email address, they are accessible for free. Only for getting answers on quizzes and getting a certificate afterwards, payed registration is required. Both MOOCs present the material in small video lectures of around 10 minutes each, on an undergraduate level, only some basic knowledge of logic and programming is assumed. The lecturer is prof Hans Zantema from Eindhoven University of Technology.
The first one is Automated Reasoning: satisfiability. It can be accessed via coursera. After a general introduction it consists of 21 video lectures covering both several examples of SAT/SMT and underlying theory (resolution, DPLL, Tseitin transformation, simplex method). It was launched in September 2018; currently it has reached around 1200 participants.
The second one is Automated Reasoning: symbolic model checking. It can also be accessed via coursera. After a general introduction it consists of 16 video lectures on CTL model checking and the underlying BDD technology. It was launched in January 2020.
The EPIT is a French thematic school proposing, on an yearly basis, an intensive 5-day long training, specializing on a particular topic in theoretical computer science. It is primarily addressed to PhD students, Post-doctoral researchers and junior academics.
The 2020 edition of the EPIT will be centered around Homotopy Type Theory, a research topic at the junction of Computer Science and Mathematics. Our hope is hence to provide an introduction that is accessible to researchers in both areas.
Pre-registration is now open, please visit the registration page to know more.
For any question, please contact the organisation.
As the number of places is limited, we have fixed a deadline for pre-registration to March 15, 2020
More information is available on the school's web page.
MOVEP is a five-day summer school on modelling and verification of infinite state systems. It aims to bring together researchers and students working in the fields of control and verification of concurrent and reactive systems.
MOVEP 2020 will consist of ten invited tutorials. In addition, there will be special sessions that allow PhD students to present their on-going research (each talk will last around 20 minutes). Extended abstracts (2-3 pages) of these presentations will be published in informal proceedings.
Important Dates (AoE)
More information is available on the school's web page.
The School, funded by Sao Paulo Research Foundation (FAPESP), celebrates the 90th anniversary of Newton da Costa and aims at:
The program comprises 9 courses and 9 plenary talks delivered in English by experts in each topic, as well as oral presentations (LED Talks) and poster sessions by the students.
Topics to be covered include:
The event will select 100 fully-funded participants (50 grantees from all states of Brazil and 50 international grantees). Funding includes airfare, medical insurance, accommodation and meals throughout the two weeks.
Undergraduate, graduate students and postdoctoral fellows (up to 5 years after completion of the Ph.D) from all countries are encouraged to apply.
More information is available on the school's web page.
The School of Computer Science at the University of Nottingham is seeking applications for 10 fully-funded PhD studentships for Home/EU students starting on 1st October 2020.
Applicants in the area of the Functional Programming Laboratory are strongly encouraged! If you are interested in applying, please contact a potential supervisor as soon as possible:The studentships are for three and a half years and include a stipend of £15,009 per year and tuition fees. Applicants are normally expected to have a first-class Masters or Bachelors degree in Computer Science or a related discipline, and must obtain the support of a potential supervisor in the School prior to submitting their application. Initial contact with supervisors should be made at least two weeks prior to the closing date for applications.
Eligible successful applicants are expected to apply for a EU VC Scholarship. Informal enquiries may be addressed to Kathrleen Fennemore. To apply, please submit the following items by email to Marc Williams:
Closing date for applications: Friday 6 March 2020.
Multiple Research Faculty and Postdoctoral positions are available with the Systems Software Research Group at Virginia Tech on DARPA-funded projects on program analysis and verification. A particular focus of the positions is automated reasoning of unintended, emergent program behaviors (e.g., weird machines) and verifying their non-exploitability. Additional thrusts include verified decompilation and verified recompilation.
Computer science/engineering PhD graduates with a background and publication record in verification, security, or program analysis are sought. Background in theorem proving (e.g., Coq, HOL4, etc), program analysis techniques, low-level system software including assembly code, ISA semantics, and functional programming are highly desirable. The positions have no teaching obligations.
Interested candidates are requested to contact Prof. Binoy Ravindran with a CV or for any questions.
The Faculty of Science at the University of Copenhagen offers a considerable number of attractive Ph.D. fellowships with application deadline February 13, 2020.
The Programming Languages and Theory of Computation (PLTC) section at the Department of Computer Science (DIKU) welcomes proposals and applications in all aspects of programming languages and systems, computability and complexity theory. We specifically encourage applications in functional programming language theory, design and implementation technology, type theory, type systems, type-based analysis, inference and synthesis.
We research semantic, logical and algorithmic foundations of computing and programming, in particular functional programming; design and implement novel programming and domain-specific languages for emerging and future computer architectures (GPUs, reversible/quantum computing); research and develop secure, private, scalable and verifiable decentralized systems (including blockchain and distributed ledger systems) and smart contract technology; apply to and derive impetus from a number of computer science (e.g. machine learning, probabilistic programming, computational finance, database systems, and logic) and application domains in collaboration with academic and industrial collaborators.
Requirements are solid, documented programming language theory foundations, a good command of English, and willingness to live in the world's most livable city.
We encourage you to send your academic CV documenting your qualifications for programming languages and systems research to a faculty member of the PLTC section prior to applying for a Ph.D. stipend to align your and our interests.
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, including 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: May 1st, 2020
Information about the PhD program can be found here.
The Faculty of Science at the University of Copenhagen announces 25 PhD openings within the TALENT programme co-funded by EU Horizon 2020, for a range of topics that includes computer science in general, and could well involve the theory and practice of SAT solving, constraint programming, and/or MIP solving in particular.
The deadline for applications is February 13, 2020, and the positions are meant to start in August 2020.
More detailed information can be found on the TALENT PhD positions web page and on the TALENT web page, but briefly, the objective of the TALENT programme is to facilitate early independence of the PhD students and fast-track their careers in academia or industry. TALENT is a unique programme by requesting, as part of the application procedure, the applicants to devise their own interdisciplinary PhD project.
In EU Horizon 2020, the University of Copenhagen is number two in Europe when it comes to attracting Marie-Sklodowska-Curie Actions, and Faculty of Science researchers have received 38 grants from the European Research Council within this program. The Faculty of Science is also host to 6 Centers of Excellence financed by the Danish National Research Foundation, and the Basic Algorithms Research Copenhagen (BARC) center at the CS department is a world-leading centre for fundamental algorithmic research. The PhD School at the Faculty of Science, in which the TALENT PhD students will be enrolled, has over 1,000 students, out of which more than half come from outside of Denmark, originating from 71 different countries.
Informal enquiries are welcome and may be sent to Jakob Nordström.
The Department of Computer Science at Lund University invites applications for postdoc and PhD positions focused on SAT solving and combinatorial optimization.
The postdocs and PhD students will be working in the research group of Jakob Nordström, which is currently in transition from KTH to a combined location at Lund University and the University of Copenhagen on either side of the Oresund bridge.
Much of the activities of the research group revolve around the themes of efficient algorithms for satisfiability in propositional logic (SAT solving) and lower bounds on the efficiency of methods for reasoning about SAT (proof complexity). On the practical side, one problem of interest is to gain a better understanding of, and improve, the performance of current state-of-the-art SAT solvers based on conflict-driven clause learning (CDCL). We are even more interested in exploring new algebraic or geometric techniques (such as Groebner bases or pseudo-Boolean solving) that could potentially yield exponential improvements over CDCL. We also believe that there should be ample room for technology transfer with related areas such as SMT solving, constraint programming (CP), and/or mixed integer linear programming (MIP), and so the research project will likely involve such areas.
The application deadline is February 10, 2020. See here and here for the full announcements with more information and instructions how to apply. Informal enquiries are welcome and may be sent to Jakob Nordström.
There are currently several open/competitive positions in the Tyrex research team which is a joint team between Inria and CNRS and UGA and Grenoble-INP local universities. In the Tyrex team, we investigate data-centric programming techniques to facilitate information and knowledge extraction, from database, programming languages and data analytics perspectives.
This includes, but is not limited to, a range of topics, including the design of domain specific programming languages together with their foundations (e.g., type systems, algebras, language design, synthesis of distributed programs), large scale and distributed data management (query optimization, graph management and information extraction from raw data), data science and artificial intelligence and knowledge extraction and inference (machine learning on and with property and knowledge graphs, predictive analytics, combined reasoning and learning from symbolic and numerical data).
A variety of positions are available at different levels:
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 are hiring a Postdoc in a large 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 postdoctoral researchers with a strong background in some of the following topics:
In addition to research, the responsibilities of the position include project management, in particular, coordination among the involved research groups, lightweight reporting to the funding agency, and outreach to potential industrial users of the developed solutions.
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:
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.
An election was held to fill 4 positions. Maria Paola Bonacina, Pascal Fontaine, Laura Kovacs, Aart Middeldorp, Renate Schmidt, and Christoph Weidenbach were nominated. 83 valid ballots were returned. Therefore, in each iteration of the single transferrable vote algorithm described in the CADE Bylaws, a candidate is elected if she or he gets at least 42 first preference votes. Otherwise, the votes of the candidate with the least first preference votes are redistributed.
The following table reports the initial distribution of preferences among the candidates:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | 5th pref. | 6th pref. | no supp. |
| Maria Paola Bonacina | 12 | 12 | 11 | 10 | 8 | 13 | 17 |
| Pascal Fontaine | 20 | 21 | 16 | 9 | 11 | 2 | 4 |
| Laura Kovacs | 10 | 12 | 16 | 23 | 7 | 7 | 8 |
| Aart Middeldorp | 10 | 11 | 10 | 12 | 13 | 15 | 12 |
| Renate Schmidt | 6 | 12 | 15 | 15 | 13 | 12 | 10 |
| Christoph Weidenbach | 25 | 14 | 12 | 5 | 11 | 8 | 8 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Renate Schmidt, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | 5th pref. | no supp. |
| Maria Paola Bonacina | 15 | 12 | 16 | 6 | 17 | 17 |
| Pascal Fontaine | 21 | 25 | 14 | 17 | 2 | 4 |
| Laura Kovacs | 10 | 14 | 24 | 20 | 7 | 8 |
| Aart Middeldorp | 11 | 13 | 12 | 13 | 22 | 12 |
| Christoph Weidenbach | 26 | 17 | 12 | 11 | 9 | 8 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Laura Kovacs, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | no supp. |
| Maria Paola Bonacina | 16 | 17 | 16 | 17 | 17 |
| Pascal Fontaine | 25 | 27 | 23 | 4 | 4 |
| Aart Middeldorp | 13 | 14 | 20 | 24 | 12 |
| Christoph Weidenbach | 29 | 23 | 10 | 13 | 8 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Aart Middeldorp, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Maria Paola Bonacina | 21 | 18 | 27 | 17 |
| Pascal Fontaine | 30 | 35 | 14 | 4 |
| Christoph Weidenbach | 32 | 24 | 19 | 8 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Maria Paola Bonacina, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Pascal Fontaine | 43 | 36 | 4 |
| Christoph Weidenbach | 38 | 37 | 8 |
Now, Pascal Fontaine reaches at least 42 first preference votes, and is elected.
To find the next elected candidate, we redistribute the votes of Pascal Fontaine and get the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | 5th pref. | no supp. |
| Maria Paola Bonacina | 12 | 21 | 8 | 12 | 13 | 17 |
| Laura Kovacs | 13 | 19 | 25 | 11 | 7 | 8 |
| Aart Middeldorp | 14 | 11 | 17 | 14 | 15 | 12 |
| Renate Schmidt | 10 | 18 | 16 | 15 | 14 | 10 |
| Christoph Weidenbach | 33 | 13 | 8 | 13 | 8 | 8 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Renate Schmidt, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | no supp. |
| Maria Paola Bonacina | 17 | 21 | 11 | 17 | 17 |
| Laura Kovacs | 14 | 27 | 25 | 9 | 8 |
| Aart Middeldorp | 16 | 15 | 18 | 22 | 12 |
| Christoph Weidenbach | 35 | 16 | 15 | 9 | 8 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Laura Kovacs, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Maria Paola Bonacina | 20 | 28 | 18 | 17 |
| Aart Middeldorp | 19 | 25 | 27 | 12 |
| Christoph Weidenbach | 43 | 19 | 13 | 8 |
Now, Christoph Weidenbach reaches at least 42 first preference votes, and is elected.
To find the next elected candidate, we redistribute the votes of Christoph Weidenbach and get the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | no supp. |
| Maria Paola Bonacina | 21 | 17 | 12 | 16 | 17 |
| Laura Kovacs | 24 | 24 | 18 | 9 | 8 |
| Aart Middeldorp | 18 | 22 | 16 | 15 | 12 |
| Renate Schmidt | 19 | 15 | 22 | 17 | 10 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Aart Middeldorp, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Maria Paola Bonacina | 26 | 19 | 21 | 17 |
| Laura Kovacs | 33 | 26 | 16 | 8 |
| Renate Schmidt | 22 | 26 | 25 | 10 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Renate Schmidt, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Maria Paola Bonacina | 36 | 30 | 17 |
| Laura Kovacs | 43 | 32 | 8 |
Now, Laura Kovacs reaches at least 42 first preference votes, and is elected.
To find the next elected candidate, we redistribute the votes of Laura Kovacs and get the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Maria Paola Bonacina | 26 | 21 | 19 | 17 |
| Aart Middeldorp | 27 | 27 | 17 | 12 |
| Renate Schmidt | 27 | 24 | 22 | 10 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Maria Paola Bonacina, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Aart Middeldorp | 41 | 30 | 12 |
| Renate Schmidt | 39 | 34 | 10 |
No candidate reaches at least 42 first preference votes.
By redistributing the votes of Renate Schmidt, one gets the following table:
| Candidate | 1st pref. | no supp. |
| Aart Middeldorp | 71 | 12 |
Now, Aart Middeldorp reaches at least 42 first preference votes, and is elected.
To summarize, the 4 candidates elected are Pascal Fontaine, Christoph Weidenbach, Laura Kovacs, and Aart Middeldorp.