In this column, logic is again in focus. Here I offer substantial challenges for you in the context of what I call proof elegance. Of course, as usual, books, papers, and the Web are off limits when attempting to meet a challenge.
As many of you know, I spend much of my time in the pursuit of elegant proofs, as evidenced by my frequent reference to the most obvious aspect of elegance -- proof length. The history of mathematics and of logic is peppered with studies by various mathematicians and logicians focusing on proof length. But many other aspects of proof elegance also merit study. For example, the avoidance of some lemma, the avoidance of some term, the identification of an axiom that is not needed because of being dependent on the remaining axioms -- each aspect offers challenging problems to solve. If you or a colleague find notions of proof elegance intriguing, you might browse in a book I coauthored with Gail Pieper, "Automated Reasoning and the Discovery of Missing and Elegant Proofs".
In this column, two aspects are in focus: axiom dependence and term avoidance. The area of concern is an old friend from a column from late 2013, namely, many-valued or infinite-valued sentential calculus.. Hyperresolution together with the following clause provides what is needed, where the function i denotes implication and the function n, found in the axioms for infinite-valued logic, denotes negation.
-P(i(x,y)) | -P(x) | P(y).
In other words, for the challenges that follow, the inference rule to be used is condensed detachment. The original axiom system for multivalued logic is the following.
% Just the implicational axioms: A1-A3
P(i(x,i(y,x))).
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(i(i(x,y),y),i(i(y,x),x))).
% Following is MV4.
P(i(i(n(x),n(y)),i(y,x))).
% Following is MV5.
P(i(i(i(x,y),i(y,x)),i(y,x))).
Your first challenge is to prove that the last of the five given formulas is in fact unneeded in the sense that it is a dependent axiom, deducible from the first four. On May 27 2001, I found, with Bill McCune's OTTER, a proof one of whose steps relied on what I call double negation, the following.
146 (heat=1) [hyper,45,137,49] P(i(n(n(x)),i(y,x))).
And, you may have guessed, your second challenge is to prove the dependence of MV5 with a sequence of deduced steps none of which contains a double-negation term, a term of the form n(n(t)) for some term t. Proofs avoiding double-negation terms are more elegant, at least to some of us.
Your third challenge, if met, would answer a question I have been trying to answer for fifteen years or more. The challenge is to find a proof of the dependence of the fifth of the five axioms, relying on condensed detachment of length strictly less than 30, regardless of the presence of double-negation terms. If you meet this challenge, please send me such a proof. I have many proofs of the dependence of MV5 on the other four, each of which has length 30.
Some of you would enjoy other challenges whose answer I know not. I offer you the following. Does there exist a proof of the dependence of MV5 on the other four axioms such that its variable richness, to be defined, is 3? The variable richness of a proof, another aspect of elegance, equals the maximum, among the deduced steps, of the number of distinct variables in a formula or equation in the proof. I have a proof of variable richness 4.
For another challenge, one that is perhaps more familiar to you, I offer the challenge of what might be termed lemma avoidance. Specifically, at various occurrences in the literature, you can find a proof of the dependence of the fifth of the five axioms for infinite-valued logic where the proof relies on the following, sometimes named 2.22, 3.5, and 3.51.
P(i(i(i(x,y),i(z,y)),i(i(y,x),i(z,x)))).
P(i(i(x,y),i(n(y),n(x)))).
P(i(i(i(x,y),i(x,z)),i(i(y,x),i(y,z)))).
Your challenge is to find a proof of the cited dependence that avoids the use of all three lemmas; no constraint is placed in the context of double negation. If you decide to first prove the cited three lemmas, the last of the three, 3.51, may turn out to be quite difficult to prove.
The concern in the next challenge is a type of distributivity. For this challenge, I ask for a proof of a type of distributivity, called 43b, the following given in its negated form.
-P(i(i(i(n(i(a,n(b))),n(i(a,n(c)))),n(i(a,n(c)))),n(i(a,n(i(i(b,c),c)))))) | $ANS(3_43b).
When I sought a proof of 43b, I had great difficulty avoiding double negation. So, the challenge is to find a proof of 43b that avoids double negation. I note that of the challenges issued in this column, this last one may be arduous.
Mike Gordon, who died last summer, devoted his research career to hardware verification. According to former colleagues, his interest in that topic dates from the 1970s, when he was working with Robin Milner at the University of Edinburgh on the development of Edinburgh LCF (Logic for Computable Functions). Although LCF was to become the foundation of practically every subsequent interactive theorem prover, including Mike's HOL system, his early ideas on hardware verification represented a completely independent strand of work.
An Edinburgh technical report dated 1981 (revised 1982) gives the earliest comprehensive overview of Mike's ideas for hardware verification. He was already looking at register transfer systems and not merely at gates. He was certainly aiming for full functional verification of implementations against specifications, as opposed to some sort of bug finding. The report is 74 pages long and full of extended examples.
These ideas evolved considerably over time. That 1981 report envisaged specifying the semantics of hardware devices using Scott domains, reflecting Mike's background in denotational semantics. In 1982, Mike moved to the University of Cambridge as a Lecturer (equivalent to an Assistant Professor). I joined him there as a post-doc to work on the continued development of LCF. Within a year, a new and improved "Cambridge LCF" was available as a basis for building new tools, and Mike launched his LCF_LSM (Logic For Sequential Machines. LSM was based on Robin Milner's CCS (Calculus of Communicating Systems). Once again, Mike was applying tools from his Edinburgh background to the problem of hardware verification. CCS was generally applied to concurrent programming, but it could be applied to hardware as well. Already in 1983, Mike had specified and verified a microcoded computer using LCF_LSM. Avra Cohn, Mike's wife, joined in the research and by 1987 had formally verified substantial aspects of a real-world processor (the Viper microprocessor, designed at the UK's Royal Signals and Radar Establishment) using LCF_LSM.
Another milestone was Mike's 1988 adoption of higher-order logic as the specification language. Already with LCF_LSM, Mike had abandoned Scott domains with their troublesome and seemingly irrelevant undefined values and partial orderings. For a while, he may have believed that advanced examples might need this more sophisticated semantic basis, but higher-order logic represented a final break from that possibility. At a time when first-order logic was strongly preferred by both mathematicians and computer scientists (notably John McCarthy), the adoption of higher-order logic was a radical choice. Mike always gave credit for this idea to Keith Hanna of the University of Kent, but if so, it must be noted that Hanna soon came to prefer even richer formalisms based on dependent types.
The advantage of higher-order logic over first-order logic was that variables could range over predicates and functions. Predicates could denote hardware components, while functions could represent the signals on the wires connecting these components. Through existential quantification, internal wires could be hidden. Functions could represent signals indexed by time, families of wires or even families of components. Best of all, the process of hardware specification and verification was suddenly being done in a standard, if slightly esoteric, form of predicate logic. Specialised primitives did not require extending the formalism and were nothing but logical definitions, essentially abbreviations. And the theory of this formalism had been completely worked out by Alonzo Church already in 1940. Mike's HOL system closely followed Church's axioms and formal development.
Three years later, in 1991, Sara Kalvala could already write a paper entitled "HOL Around the World" listing research projects using HOL, mainly for hardware verification, at a great many institutes. And because higher-order logic is a general-purpose formalism, users were not confined to hardware verification and soon found a great variety of other applications. To mention just two early examples, John Harrison considered the problem of floating-point verification and was soon verifying numerical algorithms, while Joe Hurd tackled the verification of probabilistic algorithms. Such applications required formalising substantial chunks of mathematical analysis in HOL.
It's remarkable to consider that Mike focused on hardware verification during the 1970s because he thought that software verification was on the way to being solved. Four decades later, this still hasn't happened. Mike later explained that hardware designs are much cleaner than software, although they are extremely complex. Software designers are protected from their errors by warranty disclaimers and the ease of issuing patches over the Internet, while hardware must be right the first time. Hardware verification is now a reality; when will the software world catch up?
Prof. Hans Jürgen Ohlbach has acted as vice-president of the Association for Automated Reasoning for over 20 years. He is now retiring, and has asked the board to elect a replacement. The board elected Prof. Ulrich Furbach as his successor.
We thank Hans Jürgen Ohlbach for his many years of service, and welcome Ulrich Furbach on the board.
After seven years of excellent service, Martin Giese has resigned from the posts of AAR and CADE secretary. The AAR Board and the CADE Board of Trustees cannot express how valuable has been his service to the community. He will be missed in this capacity. Thank you, Martin, for everything; it was a pleasure to work with you.
Our new AAR secretary/treasurer and CADE secretary is Philipp Rümmer, starting May 1st. We welcome Philipp in his new role and look forward to working with him.
The affairs of CADE are managed by its Board of Trustees. This includes the selection of CADE (IJCAR) co-chairs, the selection of CADE venues, electing Herbrand award winners, instituting new awards, etc.
Nominations for three CADE trustee positions are being sought, in preparation for the elections to be held after IJCAR 2018.
The current members of the board of trustees are (in alphabetical order):
The terms of Christoph Benzmüller and Aart Middeldorp end. Both of these may be nominated for a second term.
The term of office of Stephan Schulz as IJCAR 2018 program chair also ends; he is replaced by CADE-27 program co-chair Pascal Fontaine. As outgoing ex-officio trustee, Stephan Schulz is eligible to be nominated as elected trustee.
In summary, we are seeking to elect two trustees.
Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at IJCAR 2018 in Oxford. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. Nominees must be AAR members. For further details please see the CADE Inc. bylaws at the CADE web site.
E-mail nominations can be provided up to the upcoming CADE business meeting, via email to
Christoph Weidenbach, President of CADE Inc.with copies to
Philipp Rümmer, new Secretary of CADE Inc.
The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to
A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at IJCAR 2018 is
14 May 2018Nominations 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 contributions (including the relationship to CADE), along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to
Christoph Weidenbach, President of CADE Inc.with copies to
Philipp Rümmer, new Secretary of CADE Inc. and AAR
FLoC has some funds to provide travel grants of up to $1000 (USD) for student attendees of FLoC'18. Funds can be requested to cover airfare and lodging (registration fees and meals will not be funded). We expect to award about 100 grants. The application deadline is May 18, 2018, and recipients will be notified by June 1.
Funds will be provided after the conference, upon submission of receipts and a short report detailing the student's experience at and benefit from FLoC'18 (these reports will be used to compile a final report to our sponsors). Awardees are expected to spend up to one day during the meeting helping with logistics.
Applicants' advisors should send a brief statement certifying their educational status and describing their financial need, and merits.
Special efforts will be made to bring to FLoC students from under-represented groups. Applications must be received by the deadline.
Applicants are required to apply using the linked web form.
Advisor letters (plain text only) should be sent to this email address by May 18, 2018.
If you have questions, please contact this (same) email address.
Call for Nominations
Nominations are now invited for the 2018 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.2016 and 31.12.2017
are eligible for nomination for the award. The deadline for submission
is 4 April 2018.
Submission details follow below.
Nominations can be submitted from 1 January 2018 and should be sent
to the chair of the Jury, Thomas Schwentick.
The Award
The 2018 Ackermann award will be presented to the recipient(s) at the
annual conference of the EACSL, 4-7 September 2018, in Birmingham
(UK).
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, Thomas Schwentick With the following subject line and text:
Since 2002, FoLLI (the Association for Logic, Language, and Information) has awarded the E.W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree awarded in 2017.
Who qualifies.
Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2017 and December 31st, 2017. Theses must be written in English; however, the Committee accepts submissions of English translations of theses originally written in other languages, and for which a PhD was awarded in the preceding two years (i.e. between January 1st, 2015 and December 31st, 2017). There is no restriction on the nationality of the candidate or on the university where the Ph.D. was granted.
Prize.
The prize consists of:
How to submit
Only electronic submissions are accepted. The following documents are required:
All documents must be submitted electronically (preferably as a zip file) to Ian Pratt-Hartmann. Hard copy submissions are not allowed. In case of any problems with the email submission or a lack of notification within three working days, nominators should write to Ian Pratt-Hartmann.
The prize will be awarded at the ESSLLI summer school in Sofia. The current (tentative) date for the presentation ceremony is August 17th, 2018.
More information is available on the FoLLI website. Queries: Ian Pratt-Hartmann
Important dates:
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 2019. TABLEAUX typically merges into IJCAR (the International Joint Conference on Automated Reasoning) in even years. Previous TABLEAUX/IJCAR conferences took place in Brasília/Brazil (TABLEAUX 2017), Coimbra/Portugal (IJCAR 2016), Wroclaw/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). 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 and 2015 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 2019. The TABLEAUX Steering Committee will decide if they also become the PC Chair or Co-Chairs. 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 May 5th, 2018.
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.
Celebrating 30 years of formal methods research at NASA Langley, the Tenth NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems.
Keynote speakers:
The program of the symposium is available.
Registration is now open for FLOPS 2018. Deadline for early registration is 20 April, 2018.
FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming.
The list of accepted papers is available here.
Invited Speakers
The conference is held in honor of Thomas C. Hales on the occasion of his 60th birthday.
The conference will feature talks on representation theory, discrete geometry, and formal verification, with 1.5 days dedicated to each of these topics and with broadly accessible public lectures at the interfaces.
Details are available on the conference website.
The Conference
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. CSL 2018 will be the 27th edition in the series. It will be organised by the School of Computer Science of the University of Birmingham.
Important Dates
Submission
Submissions will be through EasyChair.
Proceedings will be published in the Leibniz International Proceedings in Informatics. After the conference, selected papers will be invited to a special issue of the online open access journal Logical Methods in Computer Science.
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: 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:
iFM 2018 solicits high quality papers reporting research results and/or experience reports related to the overall theme of formal method integration.
Submissions should be made using the iFM 2018 Easychair site.
Important dates
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 2018 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to
CICM appreciates the varying nature of the relevant research in this area and invites submissions of very different forms:
Important Dates
Formal submissions
AISC is a forum for the exchange of ideas and the presentation of new tools and solutions at the intersection of Artificial Intelligence and Symbolic Computation. It aims to foster contacts and collaborations among researchers from different fields related to AI and Symbolic Computation. The conference is concerned with all aspects of research, including theory, implementations, and applications.
AISC 2018 takes a broad view of AI that includes non-traditional areas such as machine/deep learning and their interactions with logic and symbolic reasoning. It will also have a special track on Collective Intelligence.
Specific topics for AISC 2018 include, but are not limited to:
Topics for the special track on Collective Intelligence include, but are not limited to:
Electronic submission as PDF should be via EasyChair. More information on the submission is available on the conference website.
Important Dates
The PPDP 2018 symposium brings together researchers from the declarative programming communities, including those working in the functional, logic, answer-set, and constraint handling programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for analyzing, performing, specifying, and reasoning about computations, including mechanisms for concurrency, security, static analysis, and verification.
Submissions are invited on all topics related to declarative programming, from principles to practice, from foundations to applications. Topics of interest include, but are not limited to
PPDP will be co-located with the 28th Int'l Symp. on Logic-Based Program Synthesis and Transformation (LOPSTR 2018).
Submission Categories
Submissions can be made in three categories: regular Research Papers,
System Descriptions, and Experience Reports.
Important dates
RuleML+RR 2018 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 and other application areas. It will provide a forum for stimulating cooperation and cross-fertilization between the many different communities focused on the research, development and applications of rule-based systems.
RuleML+RR 2018 will take place in Luxembourg on September 18th-21th 2018 and will be part of the Luxembourg Logic for AI Summit (LuxlogAI), "Methods and Tools for Responsible AI", bringing together RuleML+RR 2018, DecisionCAMP 2018, the 14th Reasoning Web Summer School (RW 2018), and the 4th Global Conference on Artificial Intelligence (GCAI 2018).
RuleML+RR welcomes original research from all areas of Rules and Reasoning.
Important Dates:
For information about the submission process, see the conference website.
In the last few decades an impressive amount of foundational research in philosophical logic has been devoted to the development of semantical tools which provide sufficiently fine-grained semantics to deal with important topics of pure and applied modal logic, such as the representation of situations, states of affairs, structured contents, hyperintensional contexts, and agent-related attitudes, like epistemic and prohairetic attitudes. A number of different modal frameworks have emerged to tackle these themes such as:
The aim of this conference is to study the potential of these approaches and to explore new connections between them, by providing a forum to present new ideas and analytical methods. We welcome both logical contributions, providing novel solutions to crucial problems in the field, and foundational contributions, focusing on the conceptual frameworks underlying these approaches and the possibility of combining them.
Submission:
We invite submissions for 30 minute presentations, with 10 additional minutes for discussion. Please send a 1000-word abstract in PDF prepared for blind review. All abstracts should be submitted electronically using the EasyChair submission page.
Important dates:
More information is available on the conference website.
ISMIS is an established and prestigious conference for exchanging the latest research results in building intelligent systems. Held twice every three years, the conference provides a medium for exchanging scientific research and technological achievements accomplished by the international community.
Formal Methods for Intelligent Systems
This special session aims at bringing together academic and
industrial leaders who will present and discuss the results that
combine Formal Methods to solve problems in different areas related to
Intelligent Systems. The topics include, but not limited to:
Paper Submission
Authors are invited to submit their manuscripts (maximum 10 pages)
electronically in Springer's LNCS/LNAI style. For detailed
instructions see the conference homepage
; any necessary information
concerning typesetting can be obtained directly from Springer's
webpage. All submissions will be subject to review by the ISMIS 2018
program committee in consultation with the special session organizers.
Important Dates
The Logic Colloquium 2018 is the annual European summer meeting of the Association of Symbolic Logic (ASL). The Association for Symbolic Logic (ASL) is an international organization supporting research and critical studies in logic. Its primary function is to provide an effective forum for the presentation, publication, and discussion of scholarly work in this area of inquiry. The Association holds two major annual meetings to present current research in all aspects of logic in a way that is accessible to all logicians.
Special Sessions:
6 special sessions with topics:
Submissions:
Abstracts of contributed papers must be submitted as LaTeX source code, via EasyChair.
More information on the submission process is available on the conference website.
Applications For Student Grants:
The ASL, the NSF, and the local organizing committee will make available modest
awards to graduate students in logic and to recent PhDs to attend the meeting.
For more details, see the student grants webpage.
Important Dates:
ADG is a forum dedicated to the exchange of ideas and views, to the presentation of research results and progress, and to the demonstration of software tools on the intersection between geometry, computation, and automated reasoning.
Aim and Scope
ADG 2018 aims at gathering researchers, engineers, and others interested
in exploring methods for automated reasoning and symbolic computation in
geometry, to discuss theoretical and practical challenges, and to present
recent research progress and results dedicated (not exhausted) in
Important Dates
More Information about ADG 2018 can be found on the conference website.
The conference is devoted to non-classical logics: modal, many-valued, temporal, paraconsistent, epistemic, deontic, substructural, and nonmonotonic logic, and their applications in computer science, artificial intelligence, formal linguistics, cognitive studies, as well as the deeper analysis of traditional philosophical problems.
This is the ninth edition, under the title: "The origins of philosophical logic: 70 years of Jaskowski's and Los' contributions". We will also celebrate the 25th anniversary of the journal Logic and Logical Philosophy published by the Nicolaus Copernicus University in Torun and edited by the Department of Logic.
Important dates
Submissions to the conference should be made via easychair. More information is 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:
Information on the submission process are available on the conference website.
Related Events
The RV conference also includes an RV tool contest as well as an
exhibition of industrial-strength runtime verification tools and
approaches. Separate calls for contribution to these events will be
issued soon.
Important Dates
Papers as well as tutorial proposals will follow the following timeline
(Anywhere on Earth):
In conjunction with FLoC in Oxford, a total number of 79 workshops will be held, many of which will be of interest to readers of the newsletter.
NB: Check the workshop websites for up-to-date information about submission deadlines.
| Pre-FLoC workshops (Saturday 7 - Sunday 8 July) | |
|
32nd International Workshop on Unification (UNIF 2018) The International Workshop on Unification 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. UNIF welcomes submissions describing research on all aspects of unification and its applications. |
Deadline: 16 April Workshop: 7 July |
|
7th International Workshop on Confluence (IWC 2018) The goal of the workshop is to provide a forum for researchers interested in the topic of confluence to exchange and share new developments in the field. The workshop will enable discussion on theoretical results, new problems, applications, implementations and benchmarks, and share the current state-of-the-art on the development of confluence tools. |
Deadline: 15 April Workshop: 7 July |
|
7th International Workshop on Classical Logic and Computation (CL&C 2018) CL&C is focused on the exploration of the computational content of mathematical and logical principles. The scientific aim of this workshop is to bring together researchers from both fields and exchange ideas. This workshop aims to support a fruitful exchange of ideas between the various lines of research on Classical Logic and Computation. |
Deadline: 10 April Workshop: 7 July |
|
Higher-Dimensional Rewriting and Algebra Rewriting consists in orienting equalities. This seemingly simple point of view has given rise to a rich theory, which was first developed in computer science for handling strings and terms, and was then extended over the recent years to many other settings (operads, monoidal categories, higher categories, etc.), allowing it to have applications in algebra, homotopy theory and physics. All these generalizations fit into the general scope of higher-dimensional rewriting theory, which has emerged as a unifying algebraic framework. The aim of the workshop is to gather people interested in pushing further rewriting theory, using (higher) category theory as a common language. It is open to all topics concerning higher-dimensional generalizations and applications of rewriting theory. |
Deadline: 15 April Workshop: 7 July |
|
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. |
Deadline: 15 April Workshop: 7 July |
|
7th International Workshop on the Cross-Fertilization Between CSP and SAT (CSPSAT 2018) Constraint Satisfaction Problems (CSP) and Boolean Satisfiability Problems (SAT) have much in common. However, they also differ in many important aspects, leading to major differences in solution techniques. More importantly, the CSP and SAT communities, while to some extent interacting with each other, are mostly separate communities with separate conferences and meetings. This workshop is designed as a venue for bridging the gap and for cross-fertilization between the two communities, in terms of ideas, problems, techniques, and results. |
Deadline: 15 April Workshop: 7 July |
|
Pragmatics of SAT The aim of the Pragmatics of SAT (PoS) workshop series is to provide a venue for researchers working on designing and/or applying Boolean satisfiability (SAT) solvers and related solver technologies, including but not restricting to satisfiability modulo theories (SMT), Answer set programming (ASP), and constraint programming (CP) as well as their optimization counterparts, to meet, communicate, and discuss latest results. |
Deadline: 15 April Workshop: 7 July |
|
Twenty Years of Deep Inference Deep inference is paradigm for designing deductive proof systems. The inference rules in such systems can perform arbitrary rewriting inside formulas. This is very different from what one would expect from more traditional formalisms, like sequent calculus or natural deduction, where formulas are always decomposed along their main connective. The purpose of this workshop is to present this vast growing field in a coherent, easy accessible way to other communities in all areas of logic in computer science, and bring together researchers in the area of deep inference to exchange ideas and to discuss their current work. |
Deadline: 15 April Workshop: 7 July |
|
10th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2018) Graphs, and graph transformation systems, are used in many areas within Computer Science: to represent data structures and algorithms, to define computation models, as a general modelling tool to study complex systems, etc. Research in term and graph rewriting ranges from theoretical questions to practical implementation issues. The aim of this workshop is to bring together researchers working in these different domains and to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. |
Deadline: 22 April Workshop: 7 July |
|
Syntax and Semantics of Low-Level Languages (LOLA 2018) Since the late 1960s it has been known that tools and structures arising in mathematical logic and proof theory can usefully be applied to the design of high-level programming languages, and to the development of reasoning principles for such languages. Yet low-level languages, such as machine code, and the compilation of high-level languages into low-level ones have traditionally been seen as having little or no essential connection to logic. The LOLA workshop, affiliated with LICS at FLoC 2018, will bring together researchers interested in the relationships and connections between logic and low-level languages and programs. |
Deadline: 15 April Workshop: 7 July |
|
9th Workshop on Higher Order Rewriting (HOR 2018) HOR is a forum to present work concerning all aspects of higher-order rewriting. HOR aims to provide an informal and friendly setting to discuss recent work and work in progress concerning higher-order rewriting, broadly construed. This includes rewriting systems that have functional variables or bound variables, the lambda-calculus and combinatory logic being paradigmatic examples. |
Deadline: 15 April Workshop: 7 July |
|
2018 Joint Workshop on Linearity & TLLA (5th International Workshop on Linearity and 2nd Workshop on Trends in Linear Logic and Applications) Linearity has been a key feature in several lines of research in bot h theoretical and practical approaches to computer science. On the theoretical side there is much work stemming from linear logic dealing with proof technology, complexity classes and more recently quantum computation. On the practical side there is work on program analysis, expressive operational semantics for programming languages, linear programming languages, program transformation, update analysis and efficient implementation techniques. The aim of this Joint Linearity and TLLA workshop is to bring together researcher s who are currently working on linear logic and related fields, to foster their interaction and provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. |
Deadline: 1 May Workshop: 7-8 July |
|
Workshop on Homotopy Type Theory and Univalent Foundations 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/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. |
Deadline: 15 April Workshop: 7-8 July |
|
Game Semantics 25 2018 will mark the 25th anniversary of the work on fully abstract game semantics for PCF, which has recently been acknowledged by the Alonzo Church award. This work led on to a very active and flourishing field of game semantics for programming languages and type theories. This aim of this GaLoP-sponsored workshop is to provide an opportunity for reflection and elaboration of different perspectives on the field. The informal meeting also welcomes work in progress, overviews of more extensive work, programmatic or position papers, tutorials, and tool demos. |
Workshop: 7-8 July |
|
Workshop on Proof Complexity (PC 2018) Proof complexity focuses on the complexity of theorem proving procedures. The central question in proof complexity is: given a theorem F (e.g., a propositional tautology) and a proof system P (i.e., a formalism usually comprised of axioms and rules), what is the size of the smallest proof of F in the system P? Moreover, how difficult is it to construct a small proof? Many ingenious techniques have been developed to try to answer these questions; and they bare tight relations to intricate theoretical questions from computational complexity (such as the celebrated P vs. NP problem), first-order arithmetic theories (e.g. separating theories of bounded arithmetic) as well as to practical problems in SAT solving. |
Deadline: 15 April Workshop: 7-8 July |
|
Programming And Reasoning on Infinite Structures (PARIS) Developing formal methods to program and reason about infinite data types, whether they are inductive or coinductive, is challenging and subject to numerous recent research efforts. Often approached in rather ad hoc ways in the past decades, the understanding of the logical and computational principles underlying those programming phenomena is reaching a more mature stage as proved by the many advances published in the recent years. The workshop aims at gathering researchers working on those topics as well as colleagues interested in understanding those recent results and open problems of this line of research. For outsiders, the workshop will offer tutorial sessions and survey-like invited talks. For specialists of the topic, the workshop will permit to gather people working with syntactical or semantical methods, people focusing on proof systems or programming languages, foster exchanges and discussions benefiting from their various perspectives. |
Deadline: 15 April Workshop: 7-8 July |
|
6th Workshop on Strategic Reasoning (SR 2018) Strategic reasoning is one of the most active research area in multi-agent system domain. The literature in this field is extensive and provides a plethora of logics for modeling strategic ability. Theoretical results are now being used in many exciting domains, including software tools for information system security, robot teams with sophisticated adaptive strategies, and automatic players capable of beating expert human adversary, just to cite a few. All these examples share the challenge of developing novel theories and tools for agent-based reasoning that take into account the likely behavior of adversaries. The SR international workshop aims to bring together researchers working on different aspects of strategic reasoning in computer science, both from a theoretical and a practical point of view. |
Deadline: 15 April Workshop: 7-8 July |
|
Workshop in honour of Dana Scott’s 85th birthday and 50 years of domain theory Fifty years ago, Dana Scott introduced domain theory for the purposes of denotational semantics of programming languages when he was in Oxford, where he worked with Christopher Strachey. This work has had a vast and lasting impact on logic, computer science, and mathematics. As part of the Workshop DOMAINS'2018, which will take place in Oxford on 7-8 July 2018, we will celebrate 50 years of domain theory and Dana Scott's 85th birthday. We will also commemorate Klaus Keimel, the founder of the workshop series. |
Deadline: 18 March Workshop: 7-8 July |
|
5th Workshop on Natural Language and Computer Science Formal tools coming from logic and category theory are important in both natural language semantics and in computational semantics. Moreover, work on these tools borrows heavily from all areas of theoretical computer science. In the other direction, applications having to do with natural language has inspired developments on the formal side. The workshop invites papers on both topics. |
Deadline: 1 May Workshop: 7-8 July |
|
7th Workshop on Mathematically Structured Functional Programming (MSFP 2018) The seventh workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control. |
Deadline: 12 April Workshop: 8 July |
|
5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018) 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. |
Deadline: 15 April Workshop: 8 July |
|
The Coq Workshop 2018 The Coq Workshop series brings together Coq users, developers, and contributors. While conferences like ITP provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks. |
Deadline: 15 April Workshop: 8 July |
|
International Workshop on Quantified Boolean Formulas and Beyond Quantified Boolean formulas (QBF) are an extension of propositional logic which allows for explicit quantification over propositional variables. The decision problem of QBF is PSPACE-complete compared to NP-completeness of the decision problem of propositional logic (SAT). The goal of the International Workshop on Quantified Boolean Formulas (QBF Workshop) is to bring together researchers working on theoretical and practical aspects of QBF solving. In addition to that, it addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term research challenges. |
Deadline: 1 May Workshop: 8 July |
|
5th International Workshop on Graphical Models for Security (GraMSec 2018) Graphical security models provide an intuitive but systematic approach to analyze security weaknesses of systems and to evaluate potential protection measures. Cyber security researchers, as well as security professionals from industry and government, have proposed various graphical security modeling schemes. Such models are used to capture different security facets (digital, physical, and social) and address a range of challenges including vulnerability assessment, risk analysis, defense analysis, automated defensing, secure services composition, policy validation and verification. The objective of the GraMSec workshop is to contribute to the development of well-founded graphical security models, efficient algorithms for their analysis, as well as methodologies for their practical usage. |
Deadline: 15 April Workshop: 8 July |
|
Women in Logic 2018 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 comprising mostly women, replicating the experience that most men have at most LiCS meetings, and lowering the stress of the occasion; 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. |
Deadline: 15 April Workshop: 8 July |
|
9th Workshop on Intersection Types and Related Systems (ITRS 2018) Intersection types were introduced near the end of the 1970s to overcome the limitations of Curry's type assignment system and to provide a characterization of the strongly normalizing terms of the Lambda Calculus. The key idea is to introduce an intersection type constructor ∧ such that a term of type t ∧ s can be used at both type t and s within the same context. This provides a finite polymorphism where various, even unrelated, types of the term are listed explicitly, differently from the more widely used universally quantified types where the polymorphic type is the common schema which stands for its various type instances. As a consequence, more terms (all and only the normalizing terms) can be typed than with universal polymorphism. The ITRS 2018 workshop aims to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches. |
Deadline: 15 April Workshop: 8 July |
|
Coalgebra Now Coalgebra is a unifying theory of state-based systems. It has emerged in the last two decades as the right mathematical framework for reasoning about infinite objects and non-well-founded structures, encompassing and abstracting fundamental concepts such as bisimilarity, coinduction and modal logic. This area has now reached a level of maturity; the aim of the workshop is to provide an overview of the state-of-the art and perspectives for future research as well as to explore connections between coalgebra and other fields in theoretical computer science. The workshop will consist of invited talks by leading coalgebra researchers as well as prominent researchers whose work has often crossed paths with the coalgebra community. The workshop will also be a chance for a wider audience, such as the one attending FLOC, to be introduced to coalgebra theory by some of the founders of the field. |
Workshop: 8 July |
|
12th International Workshop on Developments in Computational Models (DCM 2018) The aim of this workshop is to bring together researchers who are currently developing new computation models or new features for traditional computation models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. |
Deadline: 8 April Workshop: 8 July |
|
IFIP Working Group 1.6: Rewriting IFIP Working Group 1.6 is one of the working groups of the Technical Committee 1 of the International Federation for Information Processing (IFIP). IFIP is the leading multinational, apolitical organization in Information & Communications Technologies and Sciences. It is recognized by United Nations and other world bodies, represents IT Societies from 56 countries or regions, covering all 5 continents with a total membership of over half a million. WG 1.6 Scope: Rewriting for computing and reasoning; Theoretical studies of the rewriting relation of different orders; Complexity issues of rewriting; Compilation techniques and applications; Theory and applications of rewriting logic and calculus; Application of rewriting to constraint solving, theorem proving and algebraic specifications; The design, promotion and teaching of rewrite based techniques and applications. |
Workshop: 8 July |
|
Workshop on Foundations of Computer Security (FCS 2018) Computer security is an established field of both theoretical and practical significance. In recent years, there has been sustained interest in the formal foundations of methods used in computer security. The aim of the FCS 2018 workshop is to provide a forum for the discussion of continued research in this area. FCS 2018 welcomes papers on all topics related to the formal underpinnings of security and privacy, and their applications. |
Deadline: 15 April Workshop: 8 July |
|
2nd Logic Mentoring Workshop The Logic Mentoring Workshop (LMW) will introduce young researchers to the technical and practical aspects of a career in logic research. It is targeted at students, from senior undergraduates to graduates, and will include talks and panel sessions from leaders in the subject. |
Workshop: 8 July |
| Mid-FLoC workshops (Wednesday 11 - Saturday 14 July) |
Satisfiability Checking and Symbolic Computation: Bridging Two Communities to Solve Real Problems (SC2 2018) Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems; more recent developments in the area of Satisfiability Checking are starting 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 of 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, along the SC-square H2020 FETOPEN Coordination and Support Activity project, is to provide a time to discuss, share knowledge and experience across both communities. |
Deadline: 30 April Workshop: 11 July |
|
IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2018) The IFAC Conference on Analysis and Design of Hybrid Systems brings together researchers and practitioners in the area of hybrid systems, with backgrounds in control, computer science, and operations research, to provide a forum for discussing and presenting recent results in the fields of hybrid and cyber-physical systems. We solicit theoretical as well as applied research papers in the area, both as regular papers, and as tools papers, and case studies. We welcome articles connecting the cognate fields of control theory and formal verification. |
Deadline: 6 January Workshop: 11-13 July |
|
16th International Workshop on Satisfiability Modulo Theories (SMT 2018) Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and combination methods that allow one to obtain more versatile SMT tools, usually leveraging Boolean satisfiability (SAT) solvers. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification efforts. The aim of the workshop is to bring together researchers and users of SMT tools and techniques. |
Deadline: 15 April Workshop: 12-13 July |
|
7th Workshop on Logic and Systems Biology Modern biology has made great advances in our knowledge of the workings of organisms at the molecular level. Although there is still much to be learned in this area, many biologists believe that the next major effort in their discipline will be to understand how these cellular components work together, in much the same way that the components of a computer are integrated. This system-level knowledge is essential to solving important problems like understanding the causes of diseases and discovering new drugs. As models of biological systems grow in complexity, researchers are experiencing some of the same problems that beset software designers and computer engineers. The topics of this workshop reflect the interdisciplinary approach needed to solve these problems. Some of the lecturers are biologists who use computer models to develop and test their hypotheses, and others are computer scientists who are applying formal methods to build and analyze models of biological systems. |
Workshop: 13 July |
|
Isabelle Workshop This informal workshop is intended to bring together Isabelle users and developers. Participants are invited to present their research and projects, including applications of Isabelle, internal developments, add-on tools, and reports on work in progress. |
Deadline: 15 April Workshop: 13 July |
|
25th RCRA International Workshop on Experimental evaluation of algorithms for solving problems with combinatorial explosion Many problems in Artificial Intelligence show an exponential explosion of the search space. Although stemming from different research areas in AI, such problems are often addressed with algorithms that have a common goal: the effective exploration of huge state spaces. Many algorithms developed in one research area are applicable to other problems, or can be hybridised with techniques in other areas. Artificial Intelligence tools often exploit or hybridise techniques developed by other research communities, such as Operations Research. Scope of the workshop is fostering the cross-fertilisation of ideas stemming from different areas, proposing benchmarks for new challenging problems, comparing models and algorithms from an experimental viewpoint, and, in general, comparing different approaches with respect to efficiency, problem modelling, and ease of development. |
Deadline: 15 April Workshop: 13 July |
|
5th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA 2018) Distributed algorithms is an active research field; their applications range from Internet applications over cloud computing to safety-critical control systems. Whereas many applications are of critical importance, the correctness of distributed algorithms is usually based on very subtle mathematical arguments. Consequently, one easily can make mistakes with hand-written proofs, which reduces the trust in the correctness of these systems. In the last decades, formal methods were proven to be useful for the verification of many hardware and software systems. For distributed algorithms, the application of formal methods was limited: formal methods have been used for finding bugs in distributed algorithms, and to a much smaller extent formal methods were used in computer-aided verification of simple distributed algorithms. However, to verify more involved distributed algorithms, one cannot easily apply existing verification tools. To be eventually able to do this, an interdisciplinary effort from the concerned fields of formal methods, logic in computer science, and distributed algorithm theory is required. |
Workshop: 13 July |
|
5th Vampire Workshop (Vampire 2018) The workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas. The workshop will also discuss the development and use of the first-order theorem prover Vampire. Workshop participants will include both Vampire developers and users, with discussions between tool developers and users. The users can learn more about Vampire and its recent developments. The users can learn more about the use of Vampire, its efficiency in various application areas and needs of the users. |
Deadline: 10 May Workshop: 13 July |
|
19th Workshop on Logic and Computational Complexity LCC meetings are aimed at the foundational interconnections between logic and computational complexity, as present, for example, in implicit computational complexity (descriptive and type-theoretic methods); deductive formalisms as they relate to complexity (e.g. ramification, weak comprehension, bounded arithmetic, linear logic and resource logics); complexity aspects of finite model theory and databases; complexity-mindful program derivation and verification; computational complexity at higher type; and proof complexity. |
Deadline: 15 April Workshop: 13 July |
|
5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018) Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. This series of workshops aims to bring together researchers working in the two communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis. |
Deadline: 15 April Workshop: 13 July |
|
Workshop on Learning and Automata (LearnAut 2018) Grammatical Inference (GI) studies machine learning algorithms for models defining recursive computations like automata and grammars. The expressive power of this kind of models and the complexity of associated computational problems are a major research topic within the LICS community. Historically, there has been very little interaction between the GI and LICS communities, though in recent years we have seen some important results starting to bridge the gap between both worlds, including applications of learning to formal verification and model checking, and (co-)algebraic formulations of automata and grammar learning algorithms. The goal of this workshop is to bring together experts on logic that could benefit from grammatical inference tools, and researchers in grammatical inference who could find in logic and verification new applications for their methods. |
Deadline: 31 March Workshop: 13 July |
|
1st International Workshop on Multi-objective Reasoning in Verification and Synthesis MoRe aims at bringing together researchers interested in multi-objective reasoning for verification and synthesis. Traditionally, verification and synthesis techniques focus on a single qualitative or quantitative objective for the reactive system. In practice, it is often desired that systems satisfy a functional requirement expressed as a qualitative property, while optimising some quantitative dimension (e.g., reach a target state while minimising the energy consumption). Furthermore, there are numerous application contexts in which reasoning simultaneously about multiple, heterogeneous quantitative and qualitative characteristics is important. In many cases, the analysis of such systems may be complicated by the fact that there are trade-offs between objectives. Such trade-offs may also arise between several interpretations of the same quantitative dimension: for example, between the average-case and the worst-case performance of a system. MoRe is a meeting place for researchers in the area of multi-objective reasoning for verification and synthesis, with topics of interest ranging from novel theoretical models to industrial challenges and practical applications. |
Deadline: 15 April Workshop: 13 July |
|
Workshop on Modular Knowledge (Tetrapod) Mathematics, logics, and computer science support a rich ecosystem of formal knowledge. This involves many interrelated human activities such as modeling phenomena and formulating conjectures, proofs, and computations, and organizing, interconnecting, visualizing, and applying this knowledge. To handle the ever increasing body of knowledge, practitioners employ a rapidly expanding set of representation languages and computer-based tools centered around the four fundamental paradigms of formal deduction, computation, datasets, and informal narration. Expanding on the Tetrapod workshop at the conference on intelligent computer mathematics (CICM) 2016, this workshop brings together researchers from a diverse set of research areas in order to create a universal understanding of the challenges and solutions regarding highly structured knowledge bases. |
Workshop: 13 July |
|
First Workshop on Automated Deduction for Separation Logics (ADSL 2018) In recent times, program verification, and particularly deductive program verification, has made significant progress. This progress is in part due to the incorporation of logical backends such as SMT solvers and other automated theorem-proving technologies. In parallel to these developments, the verification of heap manipulating programs, and static analyses in particular, has met with substantial successes, largely due to the development of Separation Logics. The goal of this workshop is to bring together academic researchers and industrial practitioners focused on improving the state of the art of automated deduction methods for Separation Logics. |
Deadline: 15 April Workshop: 13 July |
|
Runtime Verification for Rigorous Systems Engineering The RV4RISE workshop aims at bringing together researchers and practitioners interested in the problems of detecting, testing, measuring and extracting qualitative and quantitative properties from software, hardware and cyber-physical systems. |
Workshop: 13 July |
|
13th International Workshop on User Interfaces for Theorem Provers (UITP 2018) The User Interfaces for Theorem Provers workshop series (UITP) brings together researchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal method tools, and other tools manipulating and presenting mathematical formulas. While the reasoning capabilities of interactive proof systems have increased dramatically over the last years, the system interfaces have often not enjoyed the same attention as the proof engines themselves. In many cases, interfaces remain relatively basic and under-designed. The User Interfaces for Theorem Provers workshop series provides a forum for researchers interested in improving human interaction with proof systems. We welcome participation and contributions from the theorem proving, formal methods and tools, and HCI communities, both to report on experience with existing systems, and to discuss new directions. |
Deadline: 15 April Workshop: 13 July |
|
Verification and Deduction Mentoring Workshop The purpose of the Verification and Deduction Mentoring Workshop is to provide mentoring and career advice to early-stage graduate students, to attract them to pursue research careers in the area of computer-aided verification and deduction. The workshop will particularly encourage participation of women and underrepresented minorities. The workshop program will include a number of talks and interactive sessions. The talks will give an overview of the field along with brief introductions to the varied topics highlighted at CAV, IJCAR and other conferences at the Federated Logic Conference style=. Other talks will provide mentoring and career advice, from academia and industry. |
Deadline: 13 April Workshop: 13 July |
|
Summit on Machine Learning Meets Formal Methods, sponsored by the Alan Turing Institute Machine learning has revolutionised computer science and AI: deep neural networks have been shown to match human ability in various tasks and solutions based on machine learning are being deployed in real-world systems, from automation and self-driving cars to security and banking. Undoubtedly, the potential benefits of AI systems are immense and wide ranging. At the same time, recent accidents of machine learning systems have caught the public's attention, and as a result several researchers are beginning to question their safety. Traditionally, safety assurance methodologies are the realm of formal methods, understood broadly as the rigorous, mathematical underpinning of software and hardware systems. They are rooted in logic and reasoning, and aim to provide guarantees that the system is behaving correctly, which is necessary in safety-critical contexts. Such guarantees can be provided automatically for conventional software/hardware systems using verification technologies such as model checking or theorem proving. However, machine learning does not offer guarantees, and reasoning techniques necessary to justify safety of its autonomous decisions are in their infancy. The summit on machine learning meets formal methods will bring together academic and industrial leaders who will discuss the benefits and risks of machine learning solutions. |
Workshop: 13 July |
|
4th Workshop on Formal Integrated Development Environment (F-IDE 2018) High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application to ease the justification of design choices and the review of code and proofs. The workshop is open to contributions on all aspects of a system development process, including specification, design, implementation, analysis and documentation. It welcomes the presentation of tools, methods, techniques and experiments. |
Deadline: 23 April Workshop: 14 July |
|
16th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2018) The scope of the QAPL workshop is to discuss new developments on the quantitative evaluation of systems, with an emphasis on quantitative aspects of computation, broadly construed. We solicit papers on theory, engineering methodologies, tools, case studies, and experience reports where quantitative properties such as bandwidth, cost, energy, memory, performance, probability, reliability, security, and time are first-class citizens. |
Deadline: 15 April Workshop: 14 July |
|
16th Overture Workshop: New Capabilities and Applications for Mode-based Systems Engineering The 16th Overture Workshop is the latest in a series of workshops around the Vienna Development Method (VDM), the open-source project Overture, and related tools and formalisms. VDM is one of the best established formal methods for systems development. A lively community of researchers and practitioners in academia and industry has grown around the modelling languages (VDM-SL, VDM++, VDM-RT, CML) and tools (VDMTools, Overture, Crescendo, Symphony, and the INTO-CPS chain). Together, these provide a platform for work on modelling and analysis technology that includes static and dynamic analysis, test generation, execution support, and model checking. The workshop provides a forum for discussing and advancing the state of the art in formal modelling and analysis using VDM and its family of associated formalisms. |
Deadline: 15 April Workshop: 14 July |
| Post-FLoC workshops (Wednesday 18 - Thursday 19 July) | |
|
18th Refinement Workshop Refinement is one of the cornerstones of a formal approach to software engineering: the process of developing a more detailed design or implementation from an abstract specification through a sequence of steps that maintain correctness with respect to the original specification. Refinement forms the foundation for verification in a range of application areas, including distributed and concurrent systems, cyber-physical systems, autonomous systems, and other safety-critical applications. The aim of this BCS FACS Refinement Workshop is to bring together people who are interested in the development of more concrete designs or executable programs from abstract specifications using formal notations, tool support for formal software development, and practical experience with formal refinement methodologies. The purpose of the workshop is to provide a forum for the exchange of ideas, and discussion of common ground and key differences. |
Deadline: 16 April Workshop: 18 July |
|
1st International Workshop on Parallel Logical Reasoning The goal of the Parallel Logical Reasoning workshop (PLR) is to bring together researchers that actively work on the building of tools for logical reasoning that involve parallel computations, with a particular emphasis on model checking and SAT solving, but any other applications related to logics are also in the scope of the workshop. Modern parallel architectures such as multi-core CPUs and graphics processing units (GPUs) provide great opportunity to speed up demanding computations, but the algorithms involved in model checking and SAT solving are typically hard to parallelise. Nevertheless, this has not stopped the community from achieving ground-breaking results in the last few years, sometimes building on earlier results that have been achieved in the last few decades on distributed computing, in which a network of machines is employed for a single computation. |
Workshop: 18 July |
|
7th Workshop on Synthesis (SYNT 2018) Synthesis from formal specifications is a research field with a broad range of methods and applications. Recent years have seen an increased interest in synthesis methods in general, and their practical application in particular. The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. It fosters the development of frontier techniques in automating the development of computing systems and is inclusive in its interpretation of the term synthesis. |
Deadline: 1 May Workshop: 18 July |
|
Theorem Prover Components for Educational Software (ThEdu 2018) (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. |
Deadline: 15 April Workshop: 18 July |
|
TLA+ Community Event 2018 TLA+ is a formal language for specifying systems that is used in academia and industry. Tool support for TLA+ is provided through the TLA+ Toolbox, an Integrated Development Environment for writing TLA+ specifications and analyzing them using the TLA+ tools. The tools include the TLC model checker, the PlusCal algorithm language and translator, and the TLA+ Proof System. The TLA+ Community Meeting is intended as a forum where practitioners and researchers interested in the use and further development of the TLA+ specification language and its associated tools meet and discuss. It will consist of tutorials that present recent developments concerning the TLA+ language and tools, and of contributed talks. |
Deadline: 15 April Workshop: 18 July |
|
Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2018) Since its introduction in the late 1980s, Answer Set Programming (ASP) has been widely applied to various knowledge-intensive tasks and combinatorial search problems. ASP was found to be closely related to SAT, which led to a new method of computing answer sets using SAT solvers and techniques adapted from SAT. This has been a much studied relationship, and is currently extended towards satisfiability modulo theories (SMT). The relationship of ASP to other computing paradigms, such as constraint satisfaction, quantified Boolean formulas (QBF), Constraint Logic Programming (CLP), first-order logic (FOL), and FO(ID) is also the subject of active research. Consequently, new methods of computing answer sets are being developed based on relationships to these formalisms. Furthermore, the practical applications of ASP also foster work on multi-paradigm problem-solving, and in particular, language and solver integration. The most prominent examples in this area currently are the integration of ASP with description logics (in the realm of the Semantic Web) and constraint satisfaction (which recently led to the Constraint Answer Set Programming (CASP) research direction). |
Deadline: 15 April Workshop: 18 July |
|
ICLP DC 2018: 14th Doctoral Consortium (DC) on Logic Programming (ICLP – DC 2018) The DC is designed for students currently enrolled in a Ph.D. program, however Master's students who are actively involved in research (please see the list of topics below) can also participate in the DC program. Applicants are expected to conduct research in areas related to logic and constraint programming. |
Deadline: 15 April Workshop: 18 July |
|
16th International Colloquium on Implementation of Constraint and Logic Programming Systems (CICLOPS 2018) The workshop aims at discussing and exchanging experience on the design, implementation, and optimization of logic, constraint (logic) programming systems, and other systems based on logic as a means of expressing computations. Experience backed up by real implementations and their evaluation is given preference, as well as descriptions of work in progress in that direction. |
Deadline: 29 April Workshop: 18 July |
|
3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) The ARQNL workshop aims at fostering the development of proof calculi, automated theorem proving systems and model finders for all sorts of quantified non-classical logics. The workshop will provide a forum for researchers to present and discuss recent developments in this area. The 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. |
Deadline: 15 April Workshop: 18 July |
|
Workshop on Logic and Practice of Programming (LPoP 2018) The focus of the 2018 Logic and Practice of Programming workshop is logic and declarative languages for the practice of programming. Of particular interest are languages that have a clear semantic foundation, so that they can be used for concise modeling of complex application problems, facilitating formal proofs and automated analysis, and that are also implementable, so that the implementations can run as specified, as part of real applications. Also of interest are the design of declarative languages, libraries, and tools that facilitate the construction of complex systems and applications. The target audience for these languages are students who wish to model complex application problems, and practitioners who want to use them. The goal of the workshop is to bring together the best people and best languages, tools, and ideas to help improve logic languages for the practice of programming and improve the practice of programming with logic and declarative programming. |
Deadline: 4 May Workshop: 18 July |
|
13th International Workshop on Constraint Based Methods in Bioinformatics (WCB 2018) During the last years, Biology has become a source of challenging problems for the entire field of Computer Science in general, and for the areas of computational logic and constraint programming in particular.Successful approaches to these problems are likely to have significant applications in several fields of research, such as medicine, agriculture, industry, etc. Several successful applications of the Logic and Constraint Programming paradigms in Bioinformatics have been carried out in the last years, in the area of phylogenetic tree reconstruction, in haplotype inference, in proteins structure prediction, in RNA secondary structure prediction, and in system biology, just to cite a few. The workshop aims at exchanging ideas between researchers and collecting, if possible, new problems to be faced in the next future by our community. |
Deadline: 1 May Workshop: 18 July |
|
International Workshop on the Verification and Validation of Autonomous Systems (VaVAS) Autonomous systems are being increasingly developed and used in many areas of society, from driverless cars and unmanned air vehicles, to web-bots and companion robots. A defining characteristic of such systems is that they make decisions for themselves about what to do given their current state, the state of the environment, and the purpose of the system. A key aspect of ensuring that systems with such complex (and often safety-critical) behaviour can be safely deployed is verification and validation. The workshop aims to bring together researchers working on a range of techniques for verification and validation of autonomous systems, ranging from formal methods to simulation and testing, to present recent work in the area, discuss key difficulties, and stimulate collaboration. |
Deadline: 16 April Workshop: 18-19 July |
|
16th International Workshop on Termination (WST 2018) 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. |
Deadline: 15 April Workshop: 18-19 July |
|
MLP18: Machine Learning for Programming The two-day event will feature invited and contributed talks on improving software reliability and developer productivity by using machine learning, including deep learning. The techniques of interest include leveraging big code repositories (such as GitHub) to build models of code and using them for program analysis, synthesis, and repair techniques that advance the state of the art. |
Deadline: 15 April Workshop: 18-19 July |
|
The LaSh 2018 Workshop on Logic and Search The LaSh Workshops on Logic and Search are devoted to the study, from the point of view of logic, of declarative languages for defining o representing search and optimization problems and software that uses these languages. |
Deadline: 15 April Workshop: 18-19 July |
|
10th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2018) The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation. VSTTE will bring together users and practitioners (from industry and academia), tool developers, and researchers working on theoretic aspects of verification. We welcome submissions describing significant advances in the production of verified software, i.e., software that has been proved to meet its functional specifications. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We also welcome papers describing novel experiments and case studies evaluating verification techniques and technologies. |
Deadline: 22 April Workshop: 18-19 July |
|
11th International Workshop on Numerical Software Verification (NSV-XI) Numerical computations are ubiquitous in digital systems: supervision, prediction, simulation and signal processing rely heavily on numerical calculus to achieve desired goals. Design and verification of numerical algorithms has a unique set of challenges, which set it apart from rest of software verification. To achieve the verification and validation of global properties, numerical techniques need to precisely represent local behaviors of each component. The implementation of numerical techniques on modern hardware adds another layer of approximation because of the use of finite representations of infinite precision numbers that usually lack basic arithmetic properties such as commutativity and associativity. Finally, the development and analysis of cyber-physical systems (CPS) which involve the interacting continuous and discrete components pose a further challenge. It is hence imperative to develop logical and mathematical techniques for the reasoning about programmability and reliability. The NSV workshop is dedicated to the development of such techniques. |
Deadline: 15 April Workshop: 18-19 July |
|
18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018) The aim of the AVoCS workshop series is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. In particular, AVoCS 2018 aims to bring together scientists and engineers that are active in the area of formal methods, develop tools and techniques for the automated verification of critical systems, and are interested in exchanging their experiences in the industrial usage of these methods and tools. |
Deadline: 15 April Workshop: 18-19 July |
|
Logics for Reasoning about Preferences, Uncertainty, and Vagueness (PRUV 2018) Originally, managing preferences, uncertainty, and vagueness has in particular been explored in Artificial Intelligence. During the recent years, especially with the availability of massive amounts of data in different repositories and the possibility of integrating and exploiting these data, technologies for managing preferences, uncertainty, and vagueness have started to play a key role in other areas, such as databases and the (Social or Semantic) Web. These application areas have sparked another wave of strong interest into logics for dealing with preferences, uncertainty, and vagueness. Important examples are fuzzy and probabilistic approaches for description logics or rule systems for handling vagueness and uncertainty in the Semantic Web, or formalisms for handling user preferences in the context of ontological knowledge in the Social Semantic Web. The aim of PRUV is to bring together people from different communities (such as the Artificial Intelligence and the Semantic Web community, among others), including theorists and practitioners, working on logics for reasoning about preferences, uncertainty, and vagueness. |
Deadline: 15 April Workshop: 19 July |
|
Third Workshop on Fun With Formal Methods (FWFM 2018) The primary purpose of the workshop series on Fun With Formal Methods (FWFM) is to popularize and disseminate the best practice of popularization of Formal Methods. Not an exhaustive list of topics of FWFM follows: fascinating examples of use of FM in SE; simple but interesting educational examples of FM; FM for puzzles, games and entertainment; FM and programming contests; FM elsewhere (outside software and hardware); everything and anything related to popularization of FM. |
Deadline: 20 April Workshop: 19 July |
|
International Workshop on External and Internal Calculi for Non-Classical Logics The widespread application of logical methods in several areas of computer science, epistemology and artificial intelligence has resulted in an explosion of new logics. These logics are more expressive than classical logic, allowing finer distinctions and a direct representation of notions that cannot be well stated in classical logic. For instance they are used to express different modes of truth (modal logics) and to study different types of reasoning, like reasoning about knowledge (epistemic logics) or about obligations and prohibitions (deontic logics), hypothetical and plausible reasoning (conditional logics), and reasoning on separation and sharing of resources (bunched implications logics). Apart from formalizing reasoning, the logics are used also to model systems and to prove properties about them, leading for example to applications in software verification. The purpose of this workshop would be to discuss recent results on analytic (external or internal) calculi for non-classical logics like intuitionistic, modal, epistemic logics, conditional logics, substructural, resource logics, and other logical systems. |
Deadline: 23 April Workshop: 19 July |
|
Robots, Morality, and Trust through the Verification Lens Robots are becoming members of our society. Complex algorithms have rendered robots increasingly sophisticated machines with rising levels of autonomy, enabling them to leave behind their traditional work places in factories. They have begun to enter our society, which is consisted of convoluted social rules, relationships, and expectations. Driverless cars, home assistive robots, and unmanned aerial vehicles are just a few examples. As the level of involvement of such systems increases in our daily lives, their decisions affect us more directly. Therefore, we instinctively expect robots to behave morally and make ethical decisions. For instance, we expect a firefighter robot to follow ethical principles when it is faced with a choice of saving one's life over another's in a rescue mission, and we expect an eldercare robot to take a moral stance in following the instructions of its owner when they are in conflict with the interest of others (unlike the robot in the movie "Robot & Frank"). Such expectations give rise to the notion of trust in the context of human-robot relationship and to questions such as "how can I trust a driverless car to take my child to school?" and "how can I trust a robot to help my elderly parent?" The main goal of this workshop is to shed light on the little-understood notions of morality, ethics, and trust in autonomous robots from various perspectives. |
Deadline: 1 May Workshop: 19 July |
|
6th Workshop on the Practical Aspects of Automated Reasoning (PAAR 2018) PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop will bring together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It will allow researchers to present their work in progress, and to discuss new implementation techniques and applications. |
Deadline: 15 April Workshop: 19 July |
|
Verification of Engineered Molecular Devices and Programs (VEMDP 2018) Computer-aided design and verification of molecular devices and programs is increasingly relevant as the complexity of these engineered biological systems grow. We invite practitioners to describe and formalize existing methods to automatically verify the correct design, or behavior, of molecular devices and programs, and to communicate challenges in their field. Similarly we challenge experts in verification to learn about, and contribute to, the interesting problems and unique challenges that are found in the domain of biological systems. |
Deadline: 15 April Workshop: 19 July |
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.
Typical, but not exclusive topics of interest are:
More information, including submission process available on the conference website.
Important Dates
EPIT is a long series of Spring schools in theoretical computer science, initiated by Maurice Nivat in 1973 to bring together researchers in a friendly, intensive atmosphere.
The 2018 edition will take place on May 7-11 in Aussois, on the topic of software verification. The need for software verification in our information society has been recognized as early as in the ’70s and it is an ever-more-important concern today. Over the past decades, it has driven exciting research in various fields of theoretical computer science such as logic, automata, type systems, algorithms and complexity. Recently, verification techniques have seen rapid development and industrial adoptions, notably following the SMT revolution.
Speakers and courses:
Important Dates:
For information about application and registration, see the registration webpage.
Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the sixth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions.
Speakers and courses:
Important Dates: Applicants are urged to submit their applications before April 30, 2018, since there are only a limited number of spaces available. Non-US applicants requiring US visas are requested to apply early.
For information about application and registration, see the school webpage.
We are pleased to announce that the next edition of the SAT/SMT/AR Summer School will take place in Manchester, UK on 3-6th July 2018. Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR) continue to make rapid advances and find novel uses in a wide variety of applications, both in computer science and beyond.
The SAT/SMT/AR Summer School aims to bring a select group of students up to speed quickly in this exciting research area. The school continues the successful line of Summer Schools that ran from 2011 to 2015 as SAT/SMT Summer Schools and added AR in 2016. There will also be a special session on computer algebra to continue the activity of the SC2 summer school in 2017.
Lecturers for this year's summer school have been announced on the school's website and detailed programme of topics will appear soon.
Early registration (£100) has been extended to 20th April. After this the regular rate of £200 will apply. A small number of grants are still available to subsidise registration fees and accommodation costs. Applicants should indicate on the application form whether they wish to be considered for a grant. Grants will be awarded based on need but those applying earlier will be prioritised. Note that we have separate application and registration phases and deadlines apply to application rather than registration.
Applications can be made via this following form. For more information about application and registration, see the registration webpage.
The Logic & Learning School is an opportunity to learn from, and interact with, the world's experts leading recent progress in understanding the relationships between logic and learning. These experts come from both academia and some of the leading industrial research labs (Amazon Research and DeepMind).
In the last few decades, logic has emerged as a fundamental paradigm for understanding complex systems. It has turned out to be instrumental in formal methods such as program verification, reasoning about hardware, reasoning about real-time systems and, more recently, probabilistic systems. Machine learning has recently had spectacular successes in fields such as image recognition, game playing, and many areas that involve the extraction of information from large datasets. The use of statistical approaches yields practical solutions to problems that seemed out of reach just a few years ago. The understanding of why these approaches are so successful has lagged behind the empirical successes. Using logic as the foundation to understand machine learning to obtain the best of both worlds is a major challenge.
Complete list of speakers
Students and postdocs may also be interested in the FLOC Volunteer Programme.
For registration and further information about the Logic & Learning School (opens early February) see here.
The research areas of Semantic Web, Linked Data and Knowledge Graphs have received a lot of attention in academia and industry recently. Since its inception in 2001, the Semantic Web has aimed at enriching the existing Web with meta-data and processing methods, so as to provide Web-based systems with intelligent capabilities such as context-awareness and decision support. Over the years, the Semantic Web vision has been driving many community efforts which have invested a lot of resources in developing vocabularies and ontologies for annotating their resources semantically. Besides ontologies, rules have long been a central part of the Semantic Web framework and are available as one of its fundamental representation tools, with logic serving as a unifying foundation. Linked data is a related research area which studies how one can make RDF data available on the Web, and interconnect it with other data with the aim of increasing its value for everybody. Knowledge Graphs have been shown useful not only for Web search (as demonstrated by Google, Bing etc) but also in many application domains. Many advanced capabilities required by Semantic Web, Linked Data and Knowledge Graph application scenarios call for reasoning. Thus, a perspective centered on the reasoning techniques complementing other research efforts in this area is desirable. The Reasoning Web series of annual Summer Schools is devoted to this perspective, and gives insight into the Semantic Web, Linked Data, Knowledge Graph, Ontologies, Rules, and Logic. It was started in 2005 on behalf of the work package " Education and Training (ET) " of the Network of Excellence REWERSE, and since then it has been established as a major annual event in the above mentioned research areas. It is primarily intended for postgraduate (Ph.D. or M.Sc.) students, postdoctoral researchers, young researchers, and senior researchers wishing to learn about Reasoning on the Semantic Web and related issues.
Lecturers of the school:
For information about the schools, see the website.
If only there were a place where I could prove theorems for money, change the world, and have fun while doing it...
Sounds too good to exist?
In the Trustworthy Systems team at Data61 that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities.
We are looking for 3 motivated proof engineers who want to join our team in Sydney, move things forward, and have global impact.
To apply for this position, you should possess a significant subset of the following skills.
We are hiring at two levels, so if you are more qualified or experienced than the above would suggest, you can come in as a senior proof engineer.
If you additionally have experience
Apply online at the following links:
This round of applications closes 15 April 2018.
Still studying? We also have internship opportunities!
The Logic and Computation Group at the Research School of Computer Science, The Australian National University has a number of PhD scholarship available for bright, enthusiastic doctoral students in the following fields:
Potential applicants are encouraged to consult the group's web pages and make direct contact with potential supervisors.
Students will be based at the Research School of Computer Science within the Australian National University. The studentship is a tax-free allowance of A$ 27,082 (2018 rate) per year, tenable for a maximum of 3.5 years.
Applications are to be submitted electronically here before the closing date, April 20, 2018. Further information about graduate research within Computer Science at ANU, are available here.
The scholarships are open to individuals of any nationality. We are based in Canberra, Australia, the top-ranking region of the 2014 OECD quality of life survey.
The ANU actively seeks to promote diversity in the workplace.
A postdoctoral position is available with the Systems Software Research Group at Virginia Tech on a project that is investigating verification of x86 machine code. The project vision involves formalizing x86-64 semantics, decompiling program binaries, and investigating techniques to reason about program behaviors, all inside a theorem-prover.
Recent computer science or computer engineering PhD graduates with background and expertise in theorem provers such as Isabelle/HOL, Coq, or ACL2, and with an affinity for defining the formal semantics of languages is sought. We seek candidates with a solid background in at least one of the following topics:
Interested candidates should send a CV and cover letter to Dr. Freek Verbeek. Please indicate in your email that you are applying for a postdoc position. The position is for one year, with strong possibilities for additional years. The start date is flexible, but we aim to fill the position as soon as possible. Please also contact Dr. Verbeek for any questions.
The department of Computer Science of Technische Universität Darmstadt invites applications for an assistant professorship "Semantics and Verification of Parallel Programs".
Candidates should have a strong research and publication background in the area of semantics and verification of parallel software systems, and should strive to extend and deepen their research profile in this area. Examples for relevant topics are
Application deadline: April 22, 2018
More information and details on the application process are available here.
A post-doctoral position will be available in my group (starting October 2018) on the formal proof of the GNU MPFR library. Candidates should have experience with a least one formal proof assistant, for example Isabelle. (Experience with computer arithmetic and/or MPFR is welcome but not required.)
TU Wien, TU Graz, and JKU Linz are seeking exceptionally talented and motivated students for their joint doctoral program on Logical Methods in Computer Science (LogiCS). The doctoral positions are funded for a period of 4 years according to the funding scheme of the Austrian Science Fund.
The Program
LogiCS focuses on logic and its applications in computer science. Successful
applicants will work on interdisciplinary research topics covering
Faculty Members
Austria has a vibrant and highly active and successful logic in computer science community.
Positions and Funding
We are looking for 16 doctoral students, where 30% of the positions are
reserved for highly qualified female candidates. The doctoral positions are
funded for a period of 4 years according to the funding scheme of the Austrian Science Fund.
Additional positions will be available through other funding.
How to Apply
Detailed information about the application process is available on the LogiCS web-page.
The applicants are expected to have completed an excellent master's degree in computer science, mathematics, or a related field. Candidates with comparable achievements (e.g., bachelor of honors) may be considered on a case-by-case basis. Applications by the candidates need to be submitted electronically. The positions will be filled on continuous basis till October 2018. The evaluation of applications will start on 1st of March, 2018.
For further information please write to this address.
Uppsala University announces
The topic for the positions is to develop techniques for detecting and removing security vulnerabilities in software, and applying these techniques in software for IoT devices and for the Web. Techniques that the positions will focus on include program analysis, verification, symbolic execution, testing using fuzzing, taint analysis, model learning; supported by constraint solving and SMT. Among the goals is to significantly extend the power and scalability of such techniques to real-world code bases; in particular, to analyse the widely-used Contiki OS for IoT, and to efficiently and precisely analyse JavaScript code implementing client-side or server-side functionality.
The positions are funded by recent five-year grants from SSF (the Swedish Foundation for Strategic Research) that bring together several research groups at Uppsala University (Bengt Jonsson, Parosh Abdulla, Mohammed Faouzi Atig, Philipp Ruemmer, Kostis Sagonas, Wang Yi) that are world-renowned in the fields of automated verification, programming language implementation, and testing. The work is performed in collaboration with partners at RISE SICS (Simon Duquennoy, Luca Mottola, Shahid Raza, Thiemo Voigt) including developers of the Contiki OS, and the SICS Security lab, as well as the language-based security group at Chalmers (Andrei Sabelfeld).
Application deadline: April 23 2018
For more details and instructions on how to apply see
For more information on what support you can expect see here.The department of Information Technology, Uppsala University, announces
The subject of the post-doc position is to develop more powerful techniques for code optimization or code analysis, by applying machine learning techniques (e.g., deep learning) in new ways to extract features from program code. The project will use the result of learning in several possible ways, such as code optimisation that cannot be achieved by applying standard compile-time optimizations, or the automatic verification of correctness properties.
The goal of the PhD position is to find new ways of using machine learning (in particular, methods based on deep neural networks) to improve, extend or replace classical program analyses. Two focus areas are model checking (algorithms that can automatically prove the absence of bugs in programs) and defect prediction (methods that can predict the likelihood of defects in given code segments). The PhD work will be carried out in the context of a collaboration between Uppsala University and Microsoft Research Cambridge. The position is partly funded through a Microsoft Research PhD scholarship, and includes benefits such as summer schools organised by Microsoft Research Cambridge.
Application deadline: April 30 2018
For more details and instructions on how to apply see
For more information on what support you can expect see here.The Department of Computer Science of the Università degli Studi di Verona in beautiful Verona, Italy, EU, has an opening for a postdoctoral researcher position in automated reasoning. The position is for two years, it is full-time on research (no teaching duties), and it is flexible in terms of research topic. The candidate is expected to start in September 2018 the latest. Recent PhD graduates in Computer Science or related fields with a thesis in any topic in automated reasoning, broadly meant, are invited to get in touch by e-mail with Maria Paola Bonacina. Applications will be considered as soon as received.
CELTIQUE is looking for PhD candidates and postdocs!
The IRISA/Inria Celtique group in Rennes (France) has several open PhD and post-doctoral position. The positions are funded by David Pichardie's European ERC VESTA project (2018-2023). Postdoc applicants must have a PhD in Computer Science. PhD applicants must have a Master in Computer Science. We seek candidates with a solid theoretical background in Computer Science, in at least one of the following topics:
Postdoc positions are one year, with the possibility of extension to a second year. All position may start after September 1st 2018.
Candidate that are specially interested by compiler verification will also be considered for a postdoc in the national ANR project Discover, and can negotiate a starting time earlier than September.
The working language is English, knowledge of French is not required. The successful candidate will join the Celtique team at IRISA, INRIA Rennes.
Applicants should send their curriculum vitae, cover letter and names/contact information of two references to David Pichardie. Recommendation letters should be sent to David Pichardie directly.
Potential research projects
As a pillar of the French Cybersecurity Excellence Cluster based in Rennes, the University of Rennes is opening an Assistant Professor Position (tenured) in Software Security for its , with teaching in our newly open EIT Digital Cybersecurity Master.
Rennes is the Capital of Brittany, located close to the sea and 1 hour 25' West of Paris through a new dedicated High Speed Train line. Economically attractive, Rennes has a growing research and higher education activity (63000 students, 5000 researchers), a vibrant cultural life and a widely acknowledged quality of life.
The recruited person will join one of the IRISA teams working in cybersecurity, such as CAIRN, CELTIC, CIDER, DIVERSE, DRUID, EMSEC, MYRIADS or TAMIS. The main research topics addressed by the teams involved in this area are the security of information systems including intrusion detection, cryptographic protocols, privacy protection, security of embedded and communicating security policies, database security or the security of distributed systems such as cloud computing, computing grids or peer-to-peer networks, security of micro-architecture and compilation.
More information for applying can be obtained with the leaders of these teams.
The successful candidate will have a PhD in Software Security, a track record of international publications in leading conferences and journals, and motivation for and experience with teaching and student supervision.
Since teaching within the context of EIT Digital is fully in English, and the working language at IRISA is also English, it is not mandatory for the candidate to speak French. An excellent command of the English language is however required.
The University of Rennes is an equal opportunity employer and we value the diversity of our staff and students. We particularly welcome applications from female candidates who are currently under-represented in the academic staff.
Positions for formal verification engineers are available at Apple in the Austin FV team.
If you might be interested, you can check out our listings:
See in particular:
Also feel free to contact Jared C. Davis or Jim Grundy if you'd like to know more.
We are seeking postdoctoral researchers to work in a small, agile team at NASA Ames Research Park in Silicon Valley on the multi-year QUASAR project (Quantifiable Assurance Cases for Trusted Autonomy), part of the US Defense Advanced Research Projects Agency (DARPA) Assured Autonomy research program.
The successful candidates will undertake fundamental research into the foundations of 'Dynamic Assurance Cases' (DACs), which aim to provide quantified assurance of trustworthiness in the design and operation of learning-enabled autonomous systems.
Individual positions are available on foundations, quantification, and assurance aspects for DACs:
The foundations postdoc, in particular, is relevant to Isabelle proof engineers as we anticipate extensive formal verification of the mathematical characterization and operational semantics of DACs.
Please contact Iain Whiteside directly if you have any questions,
Professor Wen-Tsun Wu passed away on May 7, 2017, a few days ahead of his 98th birthday. Wu is one of the most influential Chinese mathematicians and computer scientists. In his early years, he made fundamental contributions to algebraic topology. In the late 1970s, Wu proposed the Wu's method of geometric theorem proving and founded the school of Mathematics Mechanization. His study on the ancient Chinese mathematics opened a new era in the field of history of Chinese mathematics. He also made contributions in the area of algebraic geometry, invariant theory, complex geometry, and game theory. Professor Wu was awarded the Herbrand Award for Distinguished Contributions to Automated Reasoning in 1997 for his work on automated geometry theorem proving. An eulogy for Professor Wen-Tsun Wu can be found here.
After a bit more than one year as co-editor of the newsletter (the first newsletter that Sophie and I edited together was the March 2017 edition, after taking over from Jasmin), it turns out that it is already time again for a change of organisation. I am grateful for the offer of the AAR Board and the CADE Board of Trustees to take over the role of AAR and CADE secretary from May 1st, and am happy to accept! Since my time is limited (and getting more and more scarce it feels) the immediate consequence is, however, that I will have to step down as co-editor and fully hand over those duties to Sophie, starting with the next newsletter.
Getting the five newsletters out was certainly a lot of fun, though sometimes quite a bit of work as well. After a while, everything might start to look like a call for papers. I would like to thank Sophie for the good collaboration, and wish her all the best for the next newsletters!
* * *
This brings me to a point that I experienced as frustrating during my time as editor: the second a newsletter is released, it is already outdated! This can be for several reasons: besides the many conferences and workshops listed, there were always a few that we managed to miss; dates and submission deadlines get extended all the time, and the newsletter is not updated; or there simply turn out to be mistakes in a newsletter. The moment we send out the mail with the newsletter, we usually start getting requests for changes, last-minute additions, etc.; unless factual errors are reported, we normally have to decline, and refer to the next newsletter.
As a result, I am wondering whether some sections of the newsletter (the ones listing calls for papers) should be turned into a "living" document to which new events can be added continuously, old events are removed automatically, and updates can be made at any point. I imagine a system similar to the confsearch web page, but maintained centrally and focusing on CADE and AAR events. Generating the corresponding sections of the newsletter would then boil down to extracting a snapshot at a particular point in time. Thoughts?