Tarskian geometry comes into play again, especially because it
offers obstacles quite different from other areas of
mathematics and logic. Not too long ago, from this area, I
offered, as a challenge, the proving of a theorem, Satz 3.17,
without the use of any diagram. In this column, I offer a
related, but far greater challenge, that of proving Satz 4.14,
again without the use of a diagram. (The
symbol "|" denotes logical or, and the
symbol "-" denotes logical not.)
% following is Satz 4.14
-Col(xa,xb,xc) | -E(xa,xb,xa1,xb1)
| E3(xa,xb,xc,xa1,xb1,insert5(xa,xb,xc,xa1,xb1)).
Satz 4.14 may prove challenging even if you include a diagram, and you might enjoy trying to meet that challenge.
As before, I also offer you some Tarskian geometry axioms, followed by some theorems and possible definitions. As to which of the axioms and which of the theorems and definitions will prove useful, I leave to you to discover.
% Some axioms for Tarskian geometry
E(x,y,y,x).
-E(x,y,z,v) | -E(x,y,z2,v2) | E(z,v,z2,v2).
-E(x,y,z,z) | x=y.
T(x,y,ext(x,y,w,v)).
E(y,ext(x,y,w,v),w,v).
-E(x,y,x1,y1) | -E(y,z,y1,z1) | -E(x,v,x1,v1) | -E(y,v,y1,v1) | -T(x,y,z)
| -T(x1,y1,z1) | x=y | E(z,v,z1,v1).
-T(x,y,x) | x=y.
-T(xa,xp,xc) | -T(xb,xq,xc) | T(xp,ip(xa,xp,xc,xb,xq),xb).
-T(xa,xp,xc) | -T(xb,xq,xc) | T(xq,ip(xa,xp,xc,xb,xq),xa).
-T(alpha,beta,gamma).
-T(beta,gamma,alpha).
-T(gamma,alpha,beta).
% Theorems and definitions
% following is Satz 2.1
E(xa,xb,xa,xb).
% following is Satz 2.2
-E(xa,xb,xc,xd) | E(xc,xd,xa,xb).
% following is Satz 2.3
-E(xa,xb,xc,xd) | -E(xc,xd,xe,xf) | E(xa,xb,xe,xf).
% following is Satz 2.4
-E(xa,xb,xc,xd) | E(xb,xa,xc,xd).
% following is Satz 2.5
-E(xa,xb,xc,xd) | E(xa,xb,xd,xc).
% following is Satz 2.8
E(xa,xa,xb,xb).
% following is Satz 2.11
-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xb,xa1,xb1) | -E(xb,xc,xb1,xc1)
| E(xa,xc,xa1,xc1).
% following is Satz 2.12
xq = xa | -T(xq,xa,xd) | -E(xa,xd,xb,xc) | xd = ext(xq,xa,xb,xc).
% following is Satz 2.13
-E(xb,xc,xa,xa) | xb=xc.
% following is Satz 2.14
-E(xa,xb,xc,xd) | E(xb,xa,xd,xc).
% following is Satz 2.15
-T(xa,xb,xc) | -T(xA,xB,xC) | -E(xa,xb,xB,xC)| -E(xb,xc,xA,xB)
| E(xa,xc,xA,xC).
% Following is Satz 3.1
T(xa,xb,xb).
% Following is Satz 3.2
-T(xa,xb,xc) | T(xc,xb,xa).
% Following is Satz 3.3
T(xa1,xa1,xb1).
% Following is Satz 3.4
-T(xa,xb,xc) | -T(xb,xa,xc) | xa = xb.
% Following is Satz 3.5a
-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xb,xc).
% Following is Satz 3.6a
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xb,xc,xd).
% Following is Satz 3.7a
-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xc,xd).
% Following is Satz 3.5b
-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xc,xd).
% Following is Satz 3.6b
-T(xa,xb,xc) | -T(xa,xc,xd) | T(xa,xb,xd).
% Following is Satz 3.7b
-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xb,xd).
% Following is Satz 3.13a
alpha != beta.
% Following is Satz 3.13b
beta != gamma.
% Following is Satz 3.13a
alpha != gamma.
% Following is Satz 3.14a
T(xa,xb,ext(xa,xb,alpha,gamma)).
% Following is Satz 3.14b
xb != ext(xa,xb,alpha,gamma).
% Following is Satz 3.17
-T(xa,xb,xc) | -T(xa1,xb1,xc) | -T(xa,xp,xa1)
| T(xp,crossbar(xa,xb,xc,xa1,xb1,xp),xc).
-T(xa,xb,xc) | -T(xa1,xb1,xc) | -T(xa,xp,xa1)
| T(xb,crossbar(xa,xb,xc,xa1,xb1,xp),xb1).
% Following is Satz 4.2
-IFS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xb,xd,xb1,xd1).
% Following is Satz 4.3
-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xc,xa1,xc1) | -E(xb,xc,xb1,xc1)
| E(xa,xb,xa1,xb1).
% Following is Satz 4.5
-T(xa,xb,xc) | -E(xa,xc,xa1,xc1) | T(xa1,insert(xa,xb,xa1,xc1),xc1).
-T(xa,xb,xc) | -E(xa,xc,xa1,xc1) |
E3(xa,xb,xc,xa1,insert(xa,xb,xa1,xc1),xc1).
% Following is Satz 4.6
-T(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | T(xa1,xb1,xc1).
% Following is Satz 4.11a
-Col(xa,xb,xc) | Col(xb,xc,xa).
% Following is Satz 4.11b
-Col(xa,xb,xc) | Col(xc,xa,xb).
% Following is Satz 4.11c
-Col(xa,xb,xc) | Col(xc,xb,xa).
% Following is Satz 4.11d
-Col(xa,xb,xc) | Col(xb,xa,xc).
% Following is Satz 4.11e
-Col(xa,xb,xc) | Col(xa,xc,xb).
% Following is Satz 4.12
Col(xa,xa,xb).
% Following is Satz 4.12b
Col(xa,xb,xa).
% Following is Satz 4.13
-Col(xa,xb,xc) | - E3(xa,xb,xc,xa1,xb1,xc1) | Col(xa1,xb1,xc1).
% definition of the function insert
insert(xa,xb,xa1,xc1) = ext(ext(xc1,xa1,alpha,gamma),xa1,xa,xb).
% definition 2.10
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | T(xa,xb,xc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | T(za,zb,zc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xb,za,zb).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xc,zb,zc).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xd,za,zd).
-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xd,zb,zd).
-T(xa,xb,xc) | -T(za,zb,zc) | -E(xa,xb,za,zb) | -E(xb,xc,zb,zc)
| -E(xa,xd,za,zd) | -E(xb,xd,zb,zd)| AFS(xa,xb,xc,xd,za,zb,zc,zd).
% definition 4.1
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | T(xa,xb,xc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | T(za,zb,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xc,za,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xc,zb,zc).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xd,za,zd).
-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xc,xd,zc,zd).
-T(xa,xb,xc) | -T(za,zb,zc) | -E(xa,xc,za,zc) | -E(xb,xc,zb,zc)
| -E(xa,xd,za,zd) | -E(xc,xd,zc,zd)| IFS(xa,xb,xc,xd,za,zb,zc,zd).
% definition 4.4
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa1,xa2,xb1,xb2).
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa1,xa3,xb1,xb3).
-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa2,xa3,xb2,xb3).
-E(xa1,xa2,xb1,xb2) | -E(xa1,xa3,xb1,xb3) | -E(xa2,xa3,xb2,xb3)
| E3(xa1,xa2,xa3,xb1,xb2,xb3).
% definition 4.10
-Col(xa,xb,xc) | T(xa,xb,xc) | T(xb,xc,xa) | T(xc,xa,xb).
Col(xa,xb,xc) | -T(xa,xb,xc).
Col(xa,xb,xc) | -T(xb,xc,xa).
Col(xa,xb,xc) | -T(xc,xa,xb).
% definition 4.15
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | Col(xa,xb,xc).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E3(xa,xb,xc,xa1,xb1,xc1).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xa,xd,xa1,xd1).
-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xb,xd,xb1,xd1).
-Col(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | -E(xa,xd,xa1,xd1)
| -E(xb,xd,xb1,xd1) | FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1).
By the length of this column, when compared with the earlier column focusing on Satz 3.17, you would assume (correctly) that 4.14 is far more difficult to prove, especially without a diagram. Again, I suggest that if you intend to form an approach, you might begin with attempts to prove various cited theorems.
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. The deadline for nominations for the Herbrand Award that will be given at CADE-26 is
15 April 2017
Nominations pending from previous years must be resubmitted in order to be considered.
Nominations should consist of a letter (preferably as a PDF attachment) of up to 2000 words from the principal nominator, describing the nominee's contribution, 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.
weidenbach (at) mpi-inf.mpg.de
with copies to
Martin Giese, Secretary of CADE Inc. and AAR
martingi (at) ifi.uio.no
The Woody Bledsoe Student Travel Award was created to honour the memory of Woody Bledsoe, for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to enable selected students to attend the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering part of their expenses.
The winners of the CADE 2017 Woody Bledsoe Student Travel Award will be partially reimbursed (up to value 750 EUR) for their conference registration, transportation, and accommodation expenses.
A nomination consists of a recommendation letter of up to 300 words from the student's advisor. Nominations for CADE 2017 should be sent by e-mail to the Program Committee Chair Leonardo de Moura, and at the same time to Martin Giese, Secretary of CADE Inc. and AAR.
Nominations must arrive no later than May 12, 2017. The winners will be notified by May 26, 2017.
The awards will be presented at CADE 2017; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award.
The awards are sponsored by CADE Inc.
Nominations are now invited for the 2017 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.2015 and 31.12.2016 are eligible for nomination for the award. The deadline for submission is 1 April 2017. Submission details follow below. Nominations can be submitted from 1 January 2017 and should be sent to the chair of the Jury, Anuj Dawar, by e-mail.
The Award
The 2017 Ackermann Award will be presented to the recipient(s) at the annual conference of the EACSL, 20-24 August 2017, in Stockholm (Sweden). The award consists of
The jury is entitled to give the award to more (or less) than one dissertation in a year.
Jury
The jury consists of:
How to submit
The candidate or his/her supervisor should submit
The submission should be sent by e-mail as attachments to the chairman of the jury, Anuj Dawar with the following subject line and text:
Submission can be sent via several e-mail messages. If this is the case, please indicate it in the text.
Letters of support and documents can also be faxed to:
Anuj Dawar
Ackermann Award
+44 1223 334678
The Jury has the right to declare submissions to be out of scope or not to meet the requirements.
The past few decades have seen major achievements in interactive theorem proving, such as the formalisation of deep mathematical theorems and significant bodies of theoretical computer science, as well as the verification of complex software and hardware systems. Too often, these impressive results have been published in abbreviated or fragmentary form in conference proceedings, or not at all. This special issue welcomes full-length papers describing past work not previously published in a journal, along with new developments of any length. Small, self-contained Proof Pearls and applications of all kinds are also welcome.
This special issue will be devoted to applications of interactive theorem proving in their full variety: formalised mathematics, formalised theory, formalised semantics, formal proofs of hardware or software systems. They can be large or small.
Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.
For more information, please see the JAR-milestone webpage.
Important Dates
1 Apr 2017 Submission Deadline
1 Oct 2017 Notification of accepted papers
1 Jan 2018 Final version
Important Dates
The past few decades have seen major developments and practical achievements in automated reasoning systems. For example, SAT solving has become an inherent part of the standard hardware production process; SMT solvers are now the backbone of most software verification techniques; first-order theorem provers have pushed the productivity of interactive theorem proving to a new level; computer algebra systems have solved difficult problems in mathematics and biology; knowledge representation systems have become indispensable for reasoning in the world wide web; automatic termination checkers routinely prove the termination of complex programs.
This special issue is dedicated to automated reasoning systems in their full variety along the following dimensions:
We welcome full-length papers describing past work not previously published in a journal as well as papers of any length describing new developments. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are also eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.
We encourage submissions that include most, if not all, of the following:
For more information and details about the submission process, please see here.
For this special issue of AMAI, we are seeking original contributions on various aspects of formalization of geometry having in view computational applications mainly oriented to proof but also to modeling in geometry. Relevant topics include (but are not limited to):
Important dates:
The 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII) will take place on the campus of Ljubljana University, Slovenia, between 12 and 15 June 2017. 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:
The (extended) submission deadline is March 17, 2017. See the conference home page for more information.
The Programme Committee invites submissions for contributions on all aspects of language, logic and computation. Work of an interdisciplinary nature is particularly welcome. Areas of interest include, but are not limited to:
Authors can submit an abstract of three pages (including references) at the EasyChair conference system.
The programme, including lectures and tutorials can be found on the TbiLLC website.
Important Dates
Workshops
There will also be a workshop on "Language entitled Signs and gestures -- exploring the divide between sign language and speech-accompanying gestures".
More information will be available on the TbiLLC website.
Important dates
Objectives and Scope
Applying formal methods may involve the usage of different formalisms and different analysis techniques to validate a system, either because individual components are most amenable to one formalism or technique, because one is interested in different properties of the system, or simply to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modeling and analysis; i.e., the combination of (formal and semi-formal) methods for system development, regarding both modeling and analysis. The conference covers all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.
Areas of interest include but are not limited to:
Submission Guidelines
iFM 2017 solicits high quality papers reporting research results and/or experience reports related to the overall theme of method integration.
We solicit papers in the following categories:
Invited Speakers
Best Paper Prizes
We are pleased to have received generous sponsorship from Springer for two Best Paper awards of 500 EUR each. These awards will be decided by the Programme Committee, and will be announced and awarded at the conference.
Workshops
iFM 2017 will be accompanied by a series of workshops. Further information is available from the conference website.
It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009), Winchester (UK, 2011), Warsaw (Poland, 2013) and Nijmegen (the Netherlands, 2015).
The seventh edition will be held in Ljubljana, Slovenia, colocated with MFPS XXXIII.
See the conference website for the topics of interest and submission guidelines.
Invited Speakers
Special Session On Metrics, Privacy And Learning (joint event with MFPS)
Best Paper And Best Presentation Awards
This edition of CALCO will feature two awards: a Best Paper Award whose recipients will be selected by the PC before the conference and a Best Presentation Award, elected by the participants.
Important dates:
Satellite Workshops: Calco Early Ideas And Calco Tools
The CALCO Early Ideas Workshop is intended to enable presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute.
The CALCO Tools Workshop is dedicated to tools based on algebraic and/or coalgebraic principles.
CALCO 2017 will run together with the CALCO Early Ideas Workshop, with dedicated sessions at the end of each conference day. CALCO Tools will take place on June 13.
Background:
MFCS conference series is organized since 1972. Traditionally, the conference moved between the Czech Republic, Slovakia, and Poland, while since a few years ago, the conference travels around Europe (in 2013 it was held in Austria, then in 2014 in Hungary, in 2015, in Italy). In 2016 the conference returned to Poland and in 2017 it will be held in Denmark.
MFCS is a high-quality venue for original research in all branches of theoretical computer science. The broad scope of the conference encourages interactions between researchers who might not meet at more specialized venues.
MFCS 2017 consists of invited lectures and contributed talks, selected by an international program committee of researchers focusing on diverse areas of theoretical computer science. The conference will be accompanied by workshops.
We encourage submission of original research papers in all areas of theoretical computer science, including (but not limited to) the following (alphabetically ordered):
All submitted papers will be reviewed by the program committee. Accepted papers will be collected into the conference proceedings.
Important Dates:
Abstract submission deadline: April 20th, 2017 (AoE)
Paper submission deadline: April 24th, 2017 (AoE)
Notification of authors: June 12th, 2017 (AoE)
Camera-ready copies due: June 22nd, 2017 (AoE)
Early registration deadline: June 23rd, 2017 (AoE)
Late registration deadline: August 7th, 2017 (AoE; afterward, only on-site registration)
Conference dates: August 21-25, 2017
Paper Submission:
Papers should be submitted electronically through EasyChair.
Submissions should be prepared using the LIPIcs style and have a length of up to 12 pages (excluding references and an optional appendix). Further details are available on the conference website.
Runtime verification is concerned with the monitoring and analysis of the runtime behaviour of software and hardware systems. Runtime verification techniques are crucial for system correctness, reliability, and robustness; they provide an additional level of rigor and effectiveness compared to conventional testing, and are generally more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair.
Topics of interest to the conference include, but are not limited to:
Application areas of runtime verification include cyber-physical systems, safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy.
We welcome contributions exploring the combination of runtime verification techniques with machine learning and static analysis. Whilst these are highlight topics, papers falling into these categories will not be treated differently from other contributions.
An overview of previous RV conferences and earlier workshops can be found at: http://www.runtime-verification.org.
Important Dates
Papers as well as tutorial proposals will follow the following timeline:
General Information on Submissions
All papers and tutorials will appear in the conference proceedings in an LNCS volume. Detailed information is available at the conference website.
Paper Submissions
There are three categories of papers which can be submitted: regular, short or tool papers. Papers in each category will be reviewed by at least 3 members of the Program Committee.
Tutorial Submissions
Tutorials are two-to-three-hour presentations on a selected topic. Additionally, tutorial presenters will be offered to publish a paper of up to 20 pages in the LNCS conference proceedings, not including references.
A proposal for a tutorial must contain the subject of the tutorial, a proposed timeline, a note on previous similar tutorials (if applicable) and the differences to this incarnation, and a brief biography of the presenter. The proposal should not exceed 2 pages.
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. Topics include, but are not restricted to:
SAT 2017 will take place in Melbourne, Australia alongside CP 2017 and ICLP 2017 from August 28th to September 1st, 2017 which is the week immediately following IJCAI 2017.
Important Dates
For more information please check the conference webpage.
Authors are invited to submit papers presenting original results on all aspects of learning in logic, multi-relational learning and data mining, statistical relational learning, graph and tree mining, relational reinforcement learning, connections with other learning paradigms, and learning in other logic-based knowledge representation frameworks.
Typical, but not exclusive, topics of interest for submissions include:
We solicit three kinds of papers:
Submission:
All Paper submissions will be electronic through the ILP 2017 easychair site. More information is available on the conference website.
A special issue of a journal is planned following the conference. It will be opened to everyone. This special issue welcomes conference submissions from all the three categories above, which should be significantly revised and extended to meet the journal criteria. They will be reviewed by the Program Committee.
Dates
Abstract registration (long paper): 28 April 2017
Long paper submission: 5 May 2017
Long paper notification: 9 June 2017
Late breaking and previously published paper submission: 28 June 2017
Late breaking and previously published paper notification: 3 July 2017
It is organized by the Department of the Foundations of Computer Science at the Faculty of Philosophy of the John Paul II Catholic University of Lublin, in co-operation with the journal Studia Logica (see http://www.studialogica.org and http://link.springer.com/journal/11225).
We call for relevant contributions applying the different approaches to:
A special session on obligations derived from permissions, related to the a special issue of Studia Logica, will be a part of the conference.
Invited Speakers
Paper Submission
Extended abstracts of a length between 1 and 3 pages (including references), should be submitted via EasyChair (https://easychair.org/conferences/?conf=trends2017). More information about the submission process is available on the conference website.
Publication
Authors are encouraged to submit papers presented at Trends in Logic XVII to Studia Logica journal, where they will be a subject of full reviewing process.
Important Dates
Deadline for submissions: May 31th, 2017
Notification of acceptance: June 30th, 2017
Deadline for early registration: July 31th, 2017
Conference: September 12th-15th, 2017
MEMOCODE's objective is to bring together researchers and practitioners interested in formal methods and models for system design and development to exchange ideas, research results, and lessons learned. System design covers the development of hardware, firmware, middleware, and application software for systems ranging from single embedded devices to highly networked CPS and systems in the IoT. In particular, MEMOCODE 2017 seeks research contributions on formal foundations, engineering methods, tools, and experimental case studies. Research areas of interest include, but are not limited to the following:
Important Dates
For submission details and other information, see the conference website.
FMCAD 2017 is the seventeenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.
FMCAD employs a rigorous peer-review process. Accepted papers are distributed through both ACM and IEEE digital libraries. In addition, published articles are made available freely on the conference page; the authors retain the copyright. There are no publication fees. At least one of the authors is required to register for the conference and present the accepted paper. A small number of outstanding FMCAD submissions will be considered for inclusion in a Special Issue of the journal on Formal Methods in System Design (FMSD).
Topics of Interest
FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods and their applications to computer- aided design. Topics of interest include (but are not limited to):
Important Dates (all deadlines are 11:59 pm anywhere on earth)
Part of the FMCAD 2017 program:
TABLEAUX/FroCoS/ITP 2017 will have a poster session, which is intended for descriptions of works in progress, student projects and relevant research being published elsewhere.
Submissions should be in English, in the form of at most one page abstract, ENTCS format containing title and authors name with affiliation. The files should be sent directly to Elaine Pimentel.
The deadline for posters submission is June 15, 2017. The notification will be sent to authors June 30th.
Proceedings of this session will not be published. Formatting instructions for posters will be made available soon.
For more information please contact the local organisers:IWIL 2017 will be held in conjunction with the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to:
We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice.
Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full paper (up to 15 pages) via the EasyChair page for IWIL-2017.
Details about the submission process can be found on the workshop's website.
Important Dates:
In association with 9th NASA Formal Methods Symposium (NFM) 2017
AFM is a one-day workshop centered around the use and integration of highly automated formal verification tools for specification, interactive theorem proving, satisfiability (SAT) and satisfiability modulo theories (SMT), model checking, program verification, static analysis, runtime verification, code generation, and testing, as well as interfaces, documentation, and education. AFM functions both as a user's meeting for SRI's tools such as PVS, SAL and Yices, and as a workshop for those interested in state of the art automation for formal methods generally.
Paper deadline: March 27, 2017. See the workshop web site for details.
We are holding the first Women in Logic (WiL) workshop as a LICS associated workshop this year. The workshop intends to follow the pattern of meetings such as Women in Machine Learning (WiML, http://wimlworkshop.org/) or Women in Engineering (WIE, (http://www.ieee-ras.org/membership/women-in-engineering) that have been taking place for quite a few years. Women are chronically underrepresented in the LICS community; consequently they sometimes feel both conspicuous and isolated, and hence there is a risk that the under-representation is self-perpetuating.
The workshop will provide an opportunity for women in the field to increase awareness of one another and one another's work, to combat the feeling of isolation. It will also provide an environment where women can present to an audience comprised of mostly women, replicating the experience that most men have at most LICS meetings; we hope that this will be particularly attractive to early-career women.
Topics of interest of this workshop include but are not limited to the usual Logic in Computer Science (LICS) topics. These are listed as automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security and privacy, rewriting, type systems and type theory, and verification.
Invited Speakers
Submission deadline is 31 March 2017. See the workshop web site for details.
The workshop will bring together three strands of investigation dealing with the model theory and complexity of numeric graph parameters and their generalization to other first order structures.
(A) Gurevich and Graedel in 1998 initiated the study of metafinite model theory to study descriptive complexity of numeric parameters. Metafinite model theory found most of its applications in databases and abstract state machines (ASM), but was not widely studied in connection to numeric combinatorial parameters.
(B) Courcelle, Makowsky and Rotics initiated a definability theory for graph polynomials in 2000 and proved metatheorems for graph polynomials and numeric structural parameters.
(C) Kotek, Makowsky and Ravve questioned wether the Turing model of computation was the right choice to discuss the complexity of numeric graph parameters and proposed alternatives using the Blum-Shub-Smale model of computation.
The aim of the workshop is to bring together researchers of these three strands in order to further explore and elaborate on the appropriate framework for the study of numeric structural parameters and polynomials and to investigate further metatheorems.
Keynote Speakers
Submission deadline is 7 April 2017. See the workshop web site for details.
The main goal of this workshop is to bring together key people from various subcommunities of automated reasoning such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community. The title of the workshop is indicative of the kind of discussions we would like to encourage:
Submission deadline is 12 May 2017. See the workshop web site for details.
The workshop focuses on theory, implementation, and applications of parallel constraint reasoning. The phenomenal recent success in constraint reasoning has made approaches previously deemed impractical within the reach of both industrial and academic applications. Since some time the technology for producing CPUs has hit a physical barrier for obtaining sequential speed-up through laying out transistors on a chip. Since speed-up is no longer achievable through sequential hardware, there is an ongoing shift to wide-spread parallel computing. The workshop program will be organized as a collection of high-quality invited talks.
See the workshop web site for details.
(Computer) Theorem Proving (TP) 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:
Submission deadline is 18 June 2017. See the workshop web site for details.
Most Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the Automated Deduction, Constraint/Logic Programming and Verification communities have centered around efficiently solving problems presented as Horn clauses. This workshop aims to bring together researchers working in the communities of Automated Deduction (e.g CADE), Constraint/Logic Programming (e.g., ICLP and CP) and Program Verification community (e.g., CAV, TACAS, and VMCAI) on the topic of Horn clause based analysis, verification and synthesis.
Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:
Submission deadline is 11 June 2017. See the workshop web site for details.
The workshop aims at discussing recent developments in implementing, applying benchmarking and comparing first-order theorem provers and their combinations with other systems. Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The workshop is going to to shed the light on on problems such as
Submission deadline is 1 July 2017. See the workshop web site for details.
The previous edition in Istanbul gathered more than 400 logicians from about 50 different countries. For the 6th edition we will follow the same format:
Timeline
Call for Workshops and Tutorials: Now - Deadline: April 11, 2017
First call for contributing talks: May 2017 - Deadline to submit an abstract: September 15, 2017
Notification: November 15, 2017
Early registration: December 1st, 2017
If you want to submit a workshop or a tutorial, send a proposal to vichy@uni-log.org by April 11, 2017 following the format of the previous edition:
The first DeepSpec Summer School on Verified Systems will be held in Philadelphia from July 17 to 28, 2017, preceded by an introductory Coq Intensive from July 13 to 15.
An overview of the program is available here. Applications are currently being considered on a space-available basis.
It is our greatest pleasure to announce the first edition of the School on Foundations of Programming and Software systems. The school is jointly funded by EATCS, ETAPS, ACM SIGLOG, and ACM SIGPLAN. The topic of the first edition is Probabilistic programming. It will take place in Braga, Portugal, May 29th - June 4th 2017.
Probabilistic programming languages are used for modelling and analysis purposes across multiple areas of computer science, including machine learning, security, and quantitative biology. In particular,they provide a rigorous foundation for machine learning where they are used to describe probabilistic models and to perform inference in presence of uncertain information. Probabilistic programs are also used in cryptography and in privacy for modelling and quantifying security. The goal of the school is to introduce attendants to theoretical and practical aspects of programming languages, and will propose courses that cover the following topics: semantics, analysis, verification, applications to machine learning, privacy, and security. The school will have lectures by Andy Gordon, Catuscia Palamidessi, Christel Baier, Dexter Kozen, Frank Wood, Hongseok Yang, Javier Esparza, Michael Carbin, Peter Selinger, Prakash Panangaden, Sriram Sankaranarayanan, and Vitaly Shmatikov.
For more information please check the school webpage
If you have any queries feel free to contact the organisers.
The "Marktoberdorf Summer School" is an 10-day event for young computer scientists and mathematicians, typically doctoral and post-doctoral researchers. It provides mini-courses on state-of-the-art topics in "Logical Methods for Safety and Security of Software Systems" and leaves ample room for interaction between participants and speakers.
Speakers and courses:
Apply online: https://asimod.in.tum.de/2017/participation.shtml
Deadline: April 9
The school introduces graduate students and researchers from academia and industry into research and methodology in both Satisfiability Checking (SAT/SMT) and Symbolic Computation with one focus on their interconnections. It combines a thorough introduction into the theory of both fields with lectures on state-of-the-art software systems and their implementation. This is supplemented with presentations by lecturers from industry discussing the practical relevance of the topics of the school.
Speakers and courses:
More information can be found on the school's web page.
Job description
You will be working on the ERC project AI4REASON
(http://ai4reason.org). The project's goal is to develop new combinations of AI, Machine Learning and Theorem Proving methods that learn reasoning guidance from large proof corpora and use such guidance to steer the automated reasoning processes at various levels of granularity. Our motivation is to
Topics of interest include:
The work will include close collaboration with several international partners: University of Innsbruck, Google Research, University of Miami, Radboud University Nijmegen and others.
Requirements
You should meet the following requirements:
You will enroll in the PhD program in Artificial Intelligence at CTU with an individual study plan.
Application
Inquiries and applications should be sent via email to
Josef Urban with "AI4REASON PhD" in the subject. When sending an application please include your CV together with a brief description of your research accomplishments and interests, including the names of two references.
Deadlines: March 1, 2017, or until the positions are filled. Earlier applications are welcome and and early start date is an advantage.
The Chair of Programming Methodology at ETH Zürich is looking for excellent candidates for newly-opened PhD positions. The successful applicant will join our research group and begin work along on a new project for two PhD candidates, beginning in 2017. The project will investigate the question of how to connect modern capability-based type systems (such as that employed by the Rust programming language), and formal program reasoning techniques, in order to develop a new kind of lightweight verification tool specifically targeted at enabling everyday programmers to reason about the correctness of their code. This work is part of our ongoing Viper project.
Key requirements for successful applications:
More details about the positions:
We invite applications for two postdoctoral researcher positions at Carnegie Mellon University. The researchers will be supervised by Anupam Datta and Matthew Fredrikson.
The researcher will work to develop the emerging area of computational accountability -- theories and tools to analyze big data systems in support of security and privacy goals. The technical approach involves a combination of methods from security and privacy, programming languages and verification, statistics and causality, applied to machine learning algorithms and implementations. The ideal candidate should have expertise in at least one of these areas and interest in the others.
More details on this research direction can be found here. Interested candidates can email their CV and short description of relevant research background to Anupam Datta and Matt Fredrikson with the subject "CMU Accountability Postdoc 2017".
Several Phd positions are available in my group at University Paris Diderot, France, on various topics related to the construction of reliable software running on top of shared-memory or distributed infrastructures.
The main focus is developing automated formal methods for distributed data structures (DDSs) like Amazon Simple Storage Service, Cassandra, Google AppEngine Datastore, MongoDB, etc., which are at the basis of a wide range of automated services. The design and the usage of such data structures are based on new principles, for which we currently lack rigorous engineering methodologies. Specifically, we lack design procedures based on precise specifications, and automated reasoning techniques for enhancing the reliability of the engineering process. The main objectives are to develop (1) coherent formal specifications that provide precise requirements at design time and explicit guarantees during their usage, (2) programming principles, compatible with these specifications, for building applications on top of DDSs, and (3) efficient automated reasoning techniques for debugging or validating DDSs implementations against their specifications.
I am looking for candidates with a strong background in Computer Science with an interest in formal methods, programming languages, and algorithms. Experience in distributed systems and software development would be advantageous.
Please look at my web page for more information related to my research interests, and please contact me if you would like to discuss about these positions.
For our new 5.5-year research project (ERATO MMSD, Metamathematics for Systems Design) we are looking for 10+ senior researchers and postdocs, together with research assistants (PhD students) and internship students.
This broad project aims to extend the realm of formal methods from software to cyber-physical systems (CPS), with particular emphases on logical/categorical metatheories and industrial application (esp. in automotive industry). The project covers diverse areas that include: formal methods, programming languages, software science, software engineering, control theory, machine learning, numerical optimization, user interface, mathematical logic and category theory.
For more about the project please visit http://www-mmm.is.s.u-tokyo.ac.jp/eratommsd/about.html
About the open positions http://www-mmm.is.s.u-tokyo.ac.jp/eratommsd/openpositions.html has more information (esp. how to apply/inquire).
Two of my projects (Scavenger and Skeptik) are going to participate in Google Summer of Code this year. Both projects are implemented in Scala. Scavenger is a first-order theorem prover, and Skeptik is a tool for compressing formal proofs. Undergraduate, M.Sc. and Ph.D. students are eligible to apply. More information can be found at http://www.aossie.org/.
Student application deadline for the google summer of code: April 3 16:00 UTC
Matryoshka is an ambitious research project that aims at developing efficient higher-order superposition provers and higher-order SMT (satisfiability modulo theories) solvers and integrating them in proof assistants. The project is funded by a European Research Council Starting Grant from March 2017 to February 2022. It is co-located between Vrije Universiteit Amsterdam (Jasmin Blanchette) in the Netherlands and Inria Nancy – Grand Est (Pascal Fontaine) in France.
Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. To make interactive verification more cost-effective, we propose to deliver powerful automation to users of proof assistants by fusing and extending two lines of research: automatic and interactive theorem proving. Our approach will be to enrich the superposition calculus and SMT with higher-order reasoning in a careful manner, to preserve their desirable properties. We will develop highly automatic provers building on modern superposition provers and SMT solvers, following a Russian doll architecture. To reach end users, these new provers will be integrated in proof assistants, including Coq, Isabelle/HOL, and the TLA+ Proof System.
We are looking for outstanding candidates for several Ph.D., postdoctoral, software engineer, and intern positions due to start in the next two years. Candidates should ideally have some experience with automatic or interactive theorem proving and be at ease with both theory and engineering. Please contact Jasmin Blanchette and Pascal Fontaine for more information.
We would like to thank the AAR board for trusting us with the duty of editing the AAR newsletter. We will do our best to keep its quality at the (high) level set by our predecessors.
To get started, we would like to learn a bit more about the audience of the newsletter. If you have five minutes to spare, we would be grateful if you can provide input by answering this short survey. The survey is anonymous, and all suggestions or opinions are welcome. Of course, you can always write directly at newsletter@aarinc.org to let us know of your opinion, or of any event that you want to see in the newsletter, including job opportunities, book publications and anything you would like the AR community to know about.