In a recent conversation with my colleague Ross Overbeek, author of the inference rule UR-resolution and the weighting strategy, a question arose whose answer is crucial to certain users of some automated reasoning programs. Specifically, has something vital been lost in the recent design and implementation of such programs? Arguably, the newer programs offer far more power today if measured in terms of the number of conclusions drawn per CPU-second. But, does that tell the whole story? Can such programs prove deep theorems and solve hard problems?
To begin to answer this question, I offer a set of three clauses that form an unsatisfiable set, meaning that the deduction of appropriate conclusions leads to a proof by contradiction.
P(e(x,e(e(e(x,y),e(z,y)),z))).
-P(e(x,y)) | -P(x) | P(y).
-P(e(e(a,b),e(b,a))) | -P(e(e(a,b),e(e(b,c),e(a,c)))).
The set of clauses is not merely a syntactic example; rather, the set corresponds to a deep theorem from logic.
Of course, you might prefer a problem relying on equality exclusively. To this end, I offer a second unsatisfiable set of three clauses corresponding to a deep theorem of mathematics.
(((y ∨ x) ∧ x) ∨ (((z ∧ (x ∨ x)) ∨ (u ∧ x)) ∧ x1)) ∧ (w ∨ ((x2 ∨ x) ∧ (x ∨ x3)))=x.
x = x.
b ∨ (a ∧ (b ∧ c))!=b | b ∧ (a ∨ (b ∨ c))!=b | ((a ∧ b) ∨ (b ∧ c)) ∨ b!=b | ((a ∨ b)∧ (b ∨ c))∧ b!=b.
Which, if any, of the newer programs, given this set that relies on equality, finds a proof of unsatisfiability? I would enjoy hearing about any results, positive or negative; e-mail: wos@mcs.anl.gov.
In his guest column for the AAR Newsletter No. 120, June 2017, Christoph Weidenbach makes a quest for automated reasoning procedures that can at the same time prove and disprove a conjecture. I could not agree more with that. While reasoning procedures for decidable (fragments of) logics are naturally strong in this respect, the community has generally a hard time to find effective methods that search for proofs AND disproofs in undecidable logics. This does not mean that we neglect the advances that have been made. There is a variety of work on showing non-consequence, in particular via model finding, but also via mapping non-consequence back to consequence, like in monomorphic (algebraic) logics. From 2004 to 2007, Peter Baumgartner, Hans de Nivelle, and myself gathered people interested in these topics in a series of DISPROVING workshops. Much has happened since then, but there is still not much of an understanding that this forms a field within automated reasoning. And certainly, there is too little co-construction of proof and disproof, which is really Christoph's point.
The point I want to make in this column is related, yet different. It is about the power of failed proofs. As we all know, much of the course of mathematical discovery was attributed to failed attempts of proving conjectures, which then led to refinements in the assumptions, and often to revised definitions of central concepts. (As a side note, this is sometimes overdone in computer science papers. Often, some result cannot be established for a class of problems the authors were aiming at originally. The subclass of problems where the approach still works gives rise to a definition, together with a nice name, of that subclass. That definition is then sold as a contribution to the field, which is justified in some cases, but less so in others.)
Failed proof attempts result in artefacts we may call, a bit sloppy, ‘partial proofs’. What that means precisely depends entirely on the proof format and procedure. Either way, partial proofs can be subjected to analysis, to retrieve useful information from them. And of course, in the context of automated reasoning, we like the analysis to be automated. It could not be otherwise.
Some of the earlier applications of failed proof analysis are the works on patching conjectures by Monroy, Bundy, Ireland and by Protzen, in the mid 90s. There, conjectures which are either untrue or just not provable with a given technique are patched, to obtain provable conjectures. Since then, many techniques involving failed proof analysis were invented and used, in application areas like the search for sufficiently strong induction hypotheses, or theory exploration, among others. In particular, we lately see a growing number of applications of partial proof analysis in verification and bug finding. For instance, several variants of verification based test case generation rely on unfinished proof construction, and the analysis of the resulting partial proofs, to extract the (pre)conditions under which the various program paths are executed. Other application areas may re-iterate failed proof attempts of refined variants of a conjecture, for instance to generate loop invariants.
For a more concrete illustration of how useful failed proofs can be in the context of verification, let me briefly mention the work Mauricio Chimento, Gordon Pace, Gerardo Schneider, and myself did lately on combined static and runtime verification of Java programs. The goal was to optimise, with results from static verification, runtime monitors which check compliance of observed runs with a specification. In that work, we do not limit ourselves to using the results of complete (static) proofs. Instead, we aggressively analyse partial proofs resulting from failed proof attempts. This is especially relevant as we aim, in that work, at fully automated, from the user perspective ‘low effort’ static verification, without any user interaction, and with no code annotations! Naturally, most attempts to prove method contracts fail in such a setting. But the automated analysis of the resulting partial proofs allows us to generate (pre)conditions under which the execution is ‘covered’ by the closed parts of the proof. Such conditions are later used in the generation of an optimised monitor, to not trigger runtime checks of cases which are already covered statically. This limits the runtime overhead of monitoring, in some cases dramatically. [Ahrendt,Chimento,Pace,Schneider; Verifying data- and control-oriented properties combining static and runtime verification: theory and tools; Formal Methods in System Design]
There are several parallel developments in the exploitation of failed proofs, and I am sure we will see more. But they are so far mostly seen as a particular ‘trick’ in their respective context. It would be great if we could conceive these developments as contributions to a common theme, and have cross-application discussions about this. Also, I would like to encourage everyone to consider whether and how one's own proof technology does — or could — allow for partial proof analysis.
An election was held from 28 September to 26 October 2017 to fill three positions on the board of trustees of CADE, Inc.
Four
candidates were nominated (in alphabetic order): Jürgen Giesl, Marijn Heule, Andrew Reynolds, Bruno Woltzenlogel Paleo.
Ballots were sent by electronic mail to all members of AAR on 28 September, for a total of 1172 ballots. 107 valid ballots were returned, which translates to a participation level of 9.1% (as compared to 11.2% in 2016, 11.0% in 2015, 10.0% in 2014, 11.8% in 2013, 13.0% in 2012, 16.2% in 2011).
The counting of the votes according to the single transferable vote algorithm described in the CADE Bylaws is detailed near the end of this newsletter.
The three candidates elected are Jürgen Giesl, Marijn Heule, and Andrew Reynolds.
After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:
On
behalf of the AAR and CADE Inc., I thank Pascal Fontaine and Geoff Sutcliffe for their service on the
board of trustees for the last three, resp. six years.
Geoff continues to take care of the AAR and CADE web presence even after his term of service, and we are very grateful for this service!
We also thank Leonardo de Moura for his service as ex-officio trustee for
CADE-26.
I would also like to thank Bruno Woltzenlogel Paleo for
running in the election.
Congratulations to Jürgen Giesl, Marijn Heule, and Andrew Reynolds on being elected!
After seven years of excellent service, AAR and CADE Secretary Martin Giese has informed the CADE Board of Trustees and the AAR Board of Directors that he wishes to step down. Martin deserves heartfelt thanks from all our field! Thus, the two corporations are seeking a new Secretary.
The role of Secretary is an important one, and most precious to our organizations. Former secretaries include Bill McCune, Bob Veroff, Maria Paola Bonacina, Amy Felty, and Wolfgang Ahrendt. The two roles of Secretary of AAR and Secretary of CADE have been filled by the same person since 1999, because AAR and CADE are strongly interconnected: CADE is a subcorporation of AAR, and the members of AAR elect the board of trustees of CADE. Thus, this call is for candidates to be the Secretary of both AAR and CADE.
The Secretary is a full-right member of both the AAR Board of Directors and the CADE Board of Trustees. The Secretary shares with the other members of these boards the responsibility, and opportunity, to influence and shape the core community work and decisions. In addition, the Secretary has the following distinguished duties:
Clearly, this is a very important job, which may give a lot of reward: the new Secretary will inherit all necessary documents and historical records from the outgoing Secretary and will be welcomed by the two boards. As CADE President I'll be happy to welcome the new Secretary and help towards a smooth transition.
Interested applicants should send an e-mail message with a brief statement, highlighting motivation and previous organizational experience, if any, and the url of their web page, to
no later than January 31st, 2018. The Secretary will be appointed by the two boards as soon as possible and all applicants will be informed of the outcome.We invite proposals for sites around the world to host the 10th International Joint Conference on Automated Reasoning (IJCAR) to be held in summer 2020. Previous IJCAR meetings include IJCAR 2001 in Siena, Italy; IJCAR 2004 in Cork, Ireland; IJCAR 2006 as part of FLoC in Seattle, Washington; IJCAR 2008 in Sydney, Australia; IJCAR 2010 as part of FLoC in Edinburgh, Scotland; IJCAR 2012 in Manchester, UK; IJCAR 2014 as part of the Vienna Summer of Logic in Vienna, Austria; IJCAR 2016 in Coimbra, Portugal; and IJCAR 2018 as part of FLoC in Oxford, UK.
IJCAR is a merger of CADE (Conference on Automated Deduction), TABLEAUX (Conference on Analytic Tableaux and Related Methods), and FroCoS (Symposium on Frontiers of Combining Systems) and possibly other meetings. Usually a considerable number of Workshops are also affiliated with the conference.
The deadline for proposals is February 15, 2018. Proposals should be sent to the IJCAR Steering Committee Chair. We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within one month after the proposal due date.
Proposals should address the following points that also represent criteria for evaluation:
Perspective organizers are encouraged to get in touch with the IJCAR Steering Committee Chair for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is strongly encouraged.
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.
For more information, see the conference website
Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that.
Topics:
Dates:
See the conference website for more information.
CiE 2018 is the fourteenth conference organized by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world.
Special Sessions:
Important Dates (tentative):
In 1996, as part of its Special Year on Logic and Algorithms, DIMACS hosted the first Federated Logic Conference (FLoC). It was modeled after the successful Federated Computer Research Conference (FCRC), and synergetically brought together conferences that apply logic to computer science.
The seventh Federated Logic Conference (FLoC'18) will be held in Oxford, UK, in July 2018, at the Mathematical Institute and the Blavatnik School of Government at the University of Oxford. FLoC 2018 brings together nine major international conferences related to mathematical logic and computer science:
In addition to conferences, FLoC 2018 will also feature 79 workshops (7-8 July, 13 July, and 18-19 July) and the School on Foundations of Programming and Software Systems (FoPSS, 30 June - 6 July).
The list of workshops can be found on the FLoC workshops web page.
Important Dates:
IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions, and invited talks.
IJCAR 2018 takes place as part of FLoC 2018 and is the merger of leading events in automated reasoning:
Topics include:
Important Dates:
For information about the submission process, see the conference website.
The ITP conference series is concerned with all topics related to interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009. The ninth ITP conference, ITP 2018, will be held in Oxford, July 9-12, 2018.
Scope of Conference:
ITP welcomes submissions describing original research on all aspects of
interactive theorem proving and its applications. Suggested topics include
but
are not limited to the following:
Important Dates:
For more information, visit the conference website.
SAT 2018 welcomes scientific contributions addressing different aspects of the satisfiability problem, interpreted in a broad sense. Domains include MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulae (QBF), Satisfiability Modulo Theories (SMT), as well as Constraint Satisfaction Problems (CSP). Topics include, but are not restricted to:
Important Dates:
All deadlines are 23.59 AoE (anywhere on earth)
The full CfP and more information are available on the conference website.
TAP's scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Its topics of interest center around the connection between proofs (and other static techniques) and testing (and other dynamic techniques). Papers are solicited on, but not limited to, the following topics:
Important Dates:
See the conference website for more information.
Since 1994, the RAMiCS conference series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond.
Topics:
We invite submissions in the general fields of algebras relevant to
computer science and applications of such algebras. Topics include but
are not limited to:
Important Dates:
See the conference website for more information.
The International Joint Conference on Rules and Reasoning (RuleML+RR), the leading international joint conference in the field of rule-based reasoning, calls for high-quality papers related to theoretical advances, novel technologies, and innovative applications concerning knowledge representation and reasoning with rules. Stemming from the synergy between the well-known RuleML and RR events, one of the main goals of this conference is to build bridges between academia and industry.
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 welcomes original research from all areas of Rules and Reasoning. Topics of particular interest include:
Important Dates:
See the conference website for more information.
KR 2018 is co-located with DL 2018 and NMR 2018.
Knowledge Representation and Reasoning (KRR) is an exciting, well-established field of research. In KRR a fundamental assumption is that an agent's knowledge is explicitly represented in a declarative form, suitable for processing by dedicated reasoning engines. This assumption, that much of what an agent deals with is knowledge-based, is common in many modern intelligent systems. Consequently, KRR has contributed to the theory and practice of various areas in AI, such as automated planning, natural language understanding, among others, as well as to fields beyond AI, including databases, verification, and software engineering. In recent years KRR has contributed to new and emerging fields including the semantic web, computational biology, and the development of software agents.
We solicit papers presenting novel results on the principles of KRR that clearly contribute to the formal foundations of relevant problems or show the applicability of results to implemented or implementable systems. We also welcome papers from other areas that show clear use of, or contributions to, the principles or practice of KRR. We also encourage “reports from the field” of applications, experiments, developments, and tests.
Topics of interest include, but are not limited to:
Important Dates:
See the conference website for more information.
The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to Software Science.
ETAPS, established in 1998, is a confederation of five main annual conferences (ESOP, FASE, FOSSACS, POST and TACAS) accompanied this year by 14 satellite workshops and other events.
The complete list of workshops affiliated with ETAPS 2018 can be found on this web page. Submission deadlines range from mid-January to February.
Substructural logics are non-classical logics lacking some of the structural rules of classical logic, and are motivated by philosophical, linguistic and computational considerations. Traditionally, substructural logics have been investigated using proof theoretic and algebraic methods. In recent years, combined approaches have started to emerge. The program of this SYSMICS workshop will be focused on the interactions between syntactic and semantic methods in substructural and related logics, as well as their applications.
Important Dates:
See the workshop website for more information.
SetVR 2018 will be the 6th meeting, with the first one held in 2004, previously called the Euler Diagrams Workshop. It aims to promote theoretical, empirical, applied research on visualization and diagrammatic reasoning, especially, about sets (set-theoretical and grouped data). SetVR 2018 welcomes submissions of types: full papers (16 pages) and short papers (8 pages; at least 5 pages). Accepted papers are expected to be published on-line by CEUR Workshop Proceedings (CEUR-WS.org). SetVR 2018 will run as part of the Diagrams 2018 conference, which will be held from June 18th to 22nd in 2018, and is expected to occupy one day during this period.
Topics include:
Important Dates:
For information about the submission process, see the conference website.
Matryoshka 2018 is co-located with WAIT 2018.
This workshop brings together researchers working on automated deductive techniques for higher-order logics (especially simple type theory and dependent type theory). There has been much progress in recent years with the higher-order automatic theorem provers Leo-III and Satallax, the Lean proof assistant, and metaprovers such as HOLyHammer and Sledgehammer.
With the Matryoshka project, we aim at designing a new generation of higher-order automatic theorem provers based on state-of-the-art first-order provers, including E, VeriT, and CVC4, and to integrate them in popular proof assistants. We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. We encourage researchers motivated by the same goals to get in touch with us, subscribe to the matryoshka-devel mailing list, and join forces.
The workshop succeeds to the LPAR-05 workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), held in Montego Bay, Jamaica. The Matryoshka workshop series is conceived to be a meeting point for the Matryoshka team and colleagues working on the same challenge. It is an informal event. We expect to hold it at least once a year until the project's completion in 2023.
Please send an email to the organizers (Alexander Bentkamp and Jasmin Christian Blanchette) if you would like to give a talk, demonstrate a tool, or otherwise participate.
See the workshop website for more information.
WAIT 2018 is co-located with Matryoshka 2018.
Inductive and coinductive theorem proving is a topic of growing interest in the automated reasoning community. The Fourth International Workshop on Automated (Co)inductive Theorem Proving (WAIT 2018) focuses on all relevant aspects of (co)inductive reasoning.
The workshop is an informal event and aims to give researchers interested in the topic a chance to meet, exchange ideas, and have a platform for discussions.
We invite talks featuring demonstrations and tutorials of (co)inductive theorem provers, challenge problems, new directions of research, or anything else of interest to the (co)inductive theorem proving community.
The previous events in the series were hosted in London, Gothenburg, and Vienna. This fourth installment explicitly generalizes the scope to include coinductive methods.
Please send an email to the organizers (Johannes Hölzl and Jasmin Christian Blanchette) if you would like to give a talk, demonstrate a tool, or otherwise participate.
See the workshop website for more information.
“PhDs in Logic” is an annual graduate conference organized by local graduate students. This interdisciplinary conference welcomes contributions to various topics in mathematical logic, philosophical logic, and logic in computer science. It involves tutorials by established researchers as well as short (20 minute) presentations by PhD students, master students and first-year postdocs on their research.
PhD students, master students, and first-year postdocs in logic from disciplines that include but are not limited to philosophy, mathematics, and computer science are invited to submit an extended abstract on their research. Submitted abstracts should be about 2 pages long (not including references). Each abstract will be anonymously reviewed by the scientific committee. The accepted abstracts will be presented by their authors in a 20 minute presentation during the conference. The deadline for abstract submission is 19th January 2018.
For more information please see this web page.
The seventh Federated Logic Conference (FLoC'18) will be held in Oxford, UK, in July 2018, at the Mathematical Institute and the Blavatnik School of Government at the University of Oxford.
In addition to nine major international conferences related to mathematical logic and computer science (CAV, CSF, FM, FSCD, ICLP, IJCAR, ITP, LICS and SAT), FLoC 2018 will feature as many as 79 workshops and the School on Foundations of Programming and Software Systems (FoPSS, 30 June - 6 July).
The selection process for workshops is now over and the complete list can be found on the FLoC workshops web page.
Individual CfPs of the workshops related to automated reasoning are or will be also included in this or the following newsletter.
This year, CL&C will be held as satellite workshop of FSCD 2018 (former TLCA + rRTA). CL&C is focused on the interplay between, on one side, the exploration of the computational content of classical mathematical proofs, and on the other side, the languages and the semantic models proposed in computer science for this task: continuations, game models, denotational models, learning models and so forth. the scientific aim of this workshop is to bring together researchers from both proof theory and computer science and to exchange ideas.
The following paper categories are welcome:
Important Dates:
Affiliated with the Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 9-12 July 2018 and held as part of the Federated Logic Conference 2018 (FLoC), 6-19 July 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 comprised of 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. These are:
Important Dates:
Several new models of computation have emerged in the last years, and many developments of traditional computation models have been proposed with the aim of taking into account the new demands of users of computer systems and the new capabilities of computation engines.
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. The proceedings are produced after the meeting, so that authors can incorporate the workshop feedback in the published papers.
DCM 2018 will take place in Oxford on July 8, as a one-day satellite event of FLoC 2018, associated to LICS'18.
Topics of interest include all abstract models of computation and their applications to the development of programming languages and systems. This includes (but is not limited to):
Important Dates:
LFMTP is affiliated with FSCD 2018 (part of FLoC)
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.
LFMTP 2018 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
Important Dates:
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 back ends 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. We will consider technical submissions presenting work on the following topics (the list is not exclusive):
The workshop is affiliated with the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018) and part of the Federated Logic Conference 2018 (FLOC 2018).
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.
Important Dates:
See the LC 2018 web site for more information.
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. We will also include a special session on computer algebra to continue the activity of the SC2 summer school in 2017.
Further details (including a list of talks, application details, and grants for students) will be circulated and added to the website in January. The early application deadline is currently planned for May 1st.
As described on its Springer web page, this book, written by Mauricio Ayala-Rincon and Flavio de Moura,
This book, written by Patrick Schultz and David I. Spivak, is available on arXiv. The abstract follows.
This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be formalized in a proof assistant such as Coq or Lean by adding a number of axioms. Well-known temporal logics—such as Linear and Metric Temporal Logic (LTL and MTL)—embed within the logic of temporal type theory. The types in this theory represent “behavior types”. The language is rich enough to allow one to define arbitrary hybrid dynamical systems, which are mixtures of continuous dynamics—e.g. as described by a differential equation—and discrete jumps. In particular, the derivative of a continuous real-valued function is internally defined. We construct a semantics for the temporal type theory in the topos of sheaves on a translation-invariant quotient of the standard interval domain. In fact, domain theory plays a recurring role in both the semantics and the type theory.
Floating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and potentially lead to numerous failures. One way to greatly increase confidence in floating-point software is by computer-assisted verification of its correctness proofs.
This book provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation.
The authors of this book are Sylvie Boldo and Guillaume Melquiond. Full references are available on the publisher web page.
The Project:
You will be working on the LOEWE project “Software-Factory 4.0” (SF4.0),
funded by the German State of Hesse.
The goal of “Software-Factory 4.0” is to enable legacy software systems (as used for high performance computing and cyber-physical production systems) to keep up with the rapid technological advances made in the development of new hardware and middleware platforms. Existing software must be retrofitted to fully exploit the potential provided by technological progress. Complete re-development of the existing stock of production software is unfeasible. At the same time, superficially adapted legacy software prevents optimal hardware usage. This is known as the “software gap”.
SF4.0 aims to create methods and tools that enable continuous and largely automated re-engineering of software to meet changed requirements and technological constraints. Re-engineering keeps software development costs manageable and allows one to preserve expert domain knowledge inherent to legacy software. In SF4.0, special emphasis will be put on the reliability of the resulting software. Formal methods and semantics will be applied for this purpose.
The two main application areas to be explored in SF4.0 are “High Performance Computing” (HPC) and “Industrie 4.0”. In the former, parallelization of existing software is the main driving force, while the latter focuses on the variability aspects of cyber-physical production systems and the development of digital twins.
SF4.0 consists of eight part projects, each of which offers 1-2 Ph.D. positions in the areas of computer science and mechanical engineering. A selection of the specific areas includes: concurrency semantics, cyber-physical production systems, formal methods, parallel and distributed computing, software-aided construction, software engineering, and static program analysis.
Your Profile:
You are enthusiastic about applied and/or theoretical research and you
have a strong background and demonstrable interest in one or more of the areas
mentioned above.
We are looking for researchers with an independent mind who are willing to cooperate in our international team. We expect good communicative and social skills. Candidates should be prepared to prove their English language skills.
As a research outcome we expect publications, software tools, and a Ph.D. thesis.
What We Offer:
Further Information and How to Apply:
Applications should arrive before December 6, 2017. The application
process will be available until all positions are filled.
An electronic application form and a description of the different part projects is available at the SF4.0 application portal
Further information on the project, open positions and the application process can be found at the coordinator web page and project web page.
The Swansea Railway Verification Group has two studentship available on Formal Modelling, Analysing and Testing of Real Time Systems:
The Computational Logic research group at the University of Innsbruck has two open positions funded by the FWF (Austrian science fund) via the START project “Certifying Termination and Complexity Proofs of Programs”.
The project aims at increasing the reliability in current complexity and termination provers by independently checking the generated proofs. To this end, several analysis techniques will be formalized in the theorem prover Isabelle/HOL, with a focus on LLVM and integer transition systems.
For this project, we are looking for two enthusiastic researchers with a background in computational logic. Knowledge of automated termination analysis, complexity analysis, or theorem proving would be an asset. Candidates with a strong theoretical background in related areas are also encouraged to apply. The PhD-student candidate must have a Master's or equivalent degree. Knowledge of German is not essential.
The salary is determined by the FWF-funding scheme (3,627 EUR monthly gross salary for postdocs, and 2,071 EUR for PhD-students, cf. this web page).
Applications (including a CV, a publication list (only for postdocs), and a letter of recommendation) may be emailed to the project leader René Thiemann no later than December 18, 2017.
We plan to make decisions on these positions in December 2017. The preferred starting date is within the first three months of 2018. Informal inquiries are also welcome via email.
The city of Innsbruck is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of the Alpine environment and urban life in this historic town provides a high quality of living.
Further information is available from the following links:
The Homotopy Type Theory research group at CMU Philosophy has positions open in the coming academic year 2018-19 for incoming PhD students interested in doing research in type theory, homotopy theory, (higher) category theory, and related areas. For more information about our very active research group, see the info page.
The department also has a research group focused on interactive theorem proving, formal verification, and formalization of mathematics, centered on the Lean Theorem Prover.
For information about the Pure and Applied Logic PhD program at CMU, see the info page.
Admitted students receive full tuition, a generous living stipend, health insurance, and other benefits. Students are typically assigned limited teaching duties as graders or teaching assistants, or, when available, are supported by a research grant. Upon completion of the program, students receive the degree of PhD in Pure and Applied Logic. For further information, please contact Steve Awodey or Jeremy Avigad.
Deadline: January 2, 2018
An election was held to fill 3 positions. Juergen Giesl, Marijn Heule, Andrew Reynolds, and Bruno Woltzenlogel Paleo were nominated. 107 valid ballots were returned. Therefore, in each iteration of the single transferable vote algorithm described in the CADE Bylaws, a candidate is elected if she or he gets at least 54 first preference votes. Otherwise, the votes of the candidate with the least first preference votes are redistributed.
The following table reports the initial distribution of preferences among the candidates:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | no supp. |
| Juergen Giesl | 42 | 16 | 26 | 13 | 10 |
| Marijn Heule | 20 | 28 | 25 | 19 | 15 |
| Andrew Reynolds | 20 | 32 | 19 | 19 | 17 |
| Bruno Woltzenlogel Paleo | 25 | 20 | 21 | 21 | 20 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Marijn Heule, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Juergen Giesl | 46 | 29 | 22 | 10 |
| Andrew Reynolds | 34 | 29 | 27 | 17 |
| Bruno Woltzenlogel Paleo | 27 | 35 | 25 | 20 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Bruno Woltzenlogel Paleo, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Juergen Giesl | 56 | 41 | 10 |
| Andrew Reynolds | 43 | 47 | 17 |
Now, Juergen Giesl reaches at least 54 first preference votes, and is elected.
To find the next elected candidate, we redistribute the votes of Juergen Giesl and get the following table:
| Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
| Marijn Heule | 37 | 30 | 25 | 15 |
| Andrew Reynolds | 31 | 38 | 21 | 17 |
| Bruno Woltzenlogel Paleo | 35 | 24 | 28 | 20 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Andrew Reynolds, one gets the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Marijn Heule | 55 | 37 | 15 |
| Bruno Woltzenlogel Paleo | 47 | 40 | 20 |
Now, Marijn Heule reaches at least 54 first preference votes, and is elected.
To find the next elected candidate, we redistribute the votes of Marijn Heule and get the following table:
| Candidate | 1st pref. | 2nd pref. | no supp. |
| Andrew Reynolds | 54 | 36 | 17 |
| Bruno Woltzenlogel Paleo | 47 | 40 | 20 |
Now, Andrew Reynolds reaches at least 54 first preference votes, and is elected.
To summarize, the 3 candidates elected are Juergen Giesl, Marijn Heule, and Andrew Reynolds.
Obituaries
* * *
An OCaml library for first-order logic worth knowing
Less than a year before officially completing my PhD (Sophie writing), I was faced with a dilemma: either implement my most recent results or pursue the theoretical work without the backing of experiments. Given the short amount of time I had left, I was tempted to just forget the implementation, even knowing that this would degrade the worth of my results. Indeed, on top of my own calculus and data-structures, I also needed to implement from scratch well-founded orderings and congruence closure on ground first-order terms, among other things. Fortunately, at that time I became aware of LogTK, an OCaml library for first-order logic. LogTK is not too hard to handle when you have prior experience in OCaml, especially thanks to this tutorial, that really helped me a lot to get started. Thanks to it, I had experimental results in time for the following CADE deadline.
What I really want to say with this story is that LogTK is a cool piece of software that allowed me to go further than I expected during my PhD. If you have experience in OCaml and need to implement something in first-order logic that can't just be hacked from an existing solver, you may want to give it a try!
By the way, if you know of some other cool and not well-known library related to automated reasoning, feel free to write something about it and send it to us.
* * *
We wish happy end-of-the-year festivities and holidays to all the members of the AAR.