I have derived much satisfaction and joy from finding new results in mathematics and logic. And I expect that many of you find equal delight in your research, whether looking for a new proof or even trying to duplicate a result in a particularly daunting area. Many of the challenges I have presented in this column in past AAR newsletters have fallen into both categories. Here I return to logic, specifically to an area called the BCSK logic and one of its extensions.
Matthew Spinks and Robert Veroff spent some time and research in that area before I was introduced to it by them. Two 3-literal clauses are needed, the following, which you will recognize as old friends if you have spent some time with condensed detachment.
-P(i(x,y)) | -P(x) | P(y). % Modus -P(j(x,y)) | -P(x) | P(y). % ModusThe function i denotes implication, and the function j denotes implication.
As noted, condensed detachment is in focus here. I shall offer several challenges in this area. The solutions may have been presented in the literature already, but my intention is twofold: to provide you the opportunity to do the research on your own and to, I hope, have you go beyond the known solutions and find new ways to attack the problems.
The following nine formulas in clause notation axiomatize the BCSK logic.
P(i(x,i(y,x))). % (A1) P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). % (A2) P(i(i(i(x,y),x),x)). % (A3) P(i(x,j(y,x))). % (A4) P(i(j(x,j(y,z)),j(j(x,y),j(x,z)))). % (A5) P(i(j(x,j(y,z)),j(y,j(x,z)))). % (A6) P(i(j(j(x,y),x),x)). % (A7) P(i(j(i(x,y),y),j(i(y,x),x))). % (A8) P(j(i(x,y),j(x,y))). % (A9)
Your first challenge is to prove each of the following theorems, called theses by various logicians. Each theorem is given in its negated form.
-P(i(i(A,B),j(A,B))). -P(j(i(A,B),i(j(B,C),j(A,C)))). -P(j(i(B,C),i(j(A,B),j(A,C)))).
Your second challenge involves BCSK+, which is created by adding the following extension to BCSK:
P(i(j(j(x,y),y),j(j(y,x),x))). % (A10)You are asked to prove in BCSK+ the following, given in negated form; but your proof should not use A6 as an axiom or as a deduced clause.
-P(i(a1,i(j(a2,j(a3,a4)),j(a3,j(a2,a4))))).You might find that various proofs in BCSK+ are longer than in BCSK. This may be unexpected in that BCSK+ has access to one additional axiom, which intuitively might suggest proofs that are found will be shorter. For more possible understanding, consider the case in which some lemma is proved on the way to finding the desired proof. That part of the larger proof might be moderately long. However, if the lemma is instead included as part of the s-called axiom set, then the sought-after proof will be clearly shorter.
One reason is that you might, if successful, invent or formulate a general approach to solve such problems. Another reason is that sometimes a logician or mathematician knows of a proof of a theorem but wishes to avoid the use of some lemma or lemmas and, possibly, avoid the use of some axiom and still find a proof of the theorem.
For your third challenge, you are asked to find a proof of the preceding, stated in its negated form; however, rather than in BCSK+, you are asked to obtain a proof in BCSK. In other words, A10 cannot be used as an axiom.
For your fourth challenge, you are asked to prove the following, in negated form, in BCSK+, and then in BCSK+ replace A10 with the positive form of the following and prove it from this new set of axioms.
-P(i(j(A,B),i(A,B))). %(A10a)
In other words, A10 and A10a are equivalent in the presence of A1 through A9. In addition, you are asked to find the proofs in both directions but without using A3, A6, and A7 as axioms.
I now come to the aspect that is to me most exciting. You are asked to find which, if any, of the nine axioms for BCSK are dependent. Then you are asked to find which of the ten axioms for BCSK+ are dependent. Similar investigations can lead to the discovery of theorems that are new to the field in focus. Or, you may find new axiom dependencies or discover that certain axioms previously believed to be needed to prove particular theorems are, in fact, not needed.
If you wish to wander deeper into research, you can try to determine which simple formulas (undefined) adjoined to BCSK+, all ten axioms, have the property that, from the larger set, you can prove the three axioms for Lukasiewicz, the following in negated form.
-P(i(i(p,q),i(i(q,r),i(p,r)))). -P(i(i(n(p),p),p)). -P(i(p,i(n(p),q))).
If you begin with just the ten axioms, A1 through A10, can you prove any of the three Lukasiewicz axioms just given? If you return to BCSK, removing A10, can you prove any of the Lukasiewicz axioms?
Experiments of this type might encourage you to formulate new strategies or to incorporate into the program you use new parameters to choose from.
To close this column, I now offer a formidable challenge.
Thanks to John Halleck, a single axiom can be studied, the following.
P(i(xp,i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(i(j(xq,j(xr,xq)), xs),xs),i(j(j(xt,j(u,v)),j(j(xt,u),j(xt,v))),w)),w), i(j(j(j(x,y),x),x),z)),z),i(j(xp1,i(xq1,xp1)),xr1)),xr1),i(j(i(xs1,i(xt1, u1)), i(i(xs1,xt1),i(xs1,u1))),v1)),v1), i(j(i(w1,i(x1,y1)),i(x1,i(w1,y1))),z1)) z1),i(j(i(i(xp2,xq2),xp2),xp2),xr2)),xr2),i(i(j(xs2,xt2),i(xs2,xt2)), u2)),u2),i(j(i(j(v2,w2),w2),i(j(w2,v2),v2)),x2)),x2),i(j(i(i(y2,z2), z2),i(i(z2,y2),y2)),xp3)),xp3),i(i(xq3, i(xr3,i(xs3,xr3))),xt3)),xt3))).
The challenge, in two parts, first asks you to prove from this formula the ten axioms A1 through A10 for BCSK+.
The second half asks for a proof that the cited single axiom is a theorem, provable from the ten axioms of BCSK+. The length of the given single axiom may indeed prove to be a substantial obstacle, for either of the two parts of the challenge. And, as a bit of a puzzle to solve, of the two given 3-literal clauses for implication, only one is needed to meet the various challenges.
The Herbrand Award is given by CADE Inc. to honour a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to
A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at CADE-27 is
13 May 2019Nominations 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, Secretary of AAR and CADE Inc.
Nominations are now invited for the 2019 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.2017 and 31.12.2018 are eligible for nomination for the award. The deadline for submission is 1 April 2019. Submission details follow below.
Nominations can be submitted from 1 January 2019 and should be sent to the chair of the Jury, Thomas Schwentick.
The Award
The 2019 Ackermann award will be presented to the recipient(s) at CSL
2020, the annual conference of the EACSL, 13-16 January 2020, in Barcelona.
The award consists of
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:
Submission can be sent via several e-mail messages. If this is the case, please indicate it in the text.
Jasmin Christian Blanchette
Cătălin Hriţcu
Co-chairs of CPP 2020
The CPP (Certified Programs and Proofs) conference series, initiated in 2011, targets any research promoting formal development of certified software and proofs. We would like to bring this conference to the attention of AR researchers.
CPP is often perceived as a close relative of the ITP (Interactive Theorem Proving) conference, but as explained in its manifesto, it has a substantially broader scope, including
CPP welcomes any research promoting formal development of certified software and proofs. Beyond papers that have a mechanized implementation, it also welcomes papers that present new foundational theory, semantic models, program logics, and type systems even if they have only pen-and-paper proofs.
Historically, CPP has received few submissions from the AR community (beyond its ITP subcommunity), but these have usually been well received. The authors of the following accepted papers, from the last five years, can attest to this:
Why not join them? The next edition of CPP will be held in New Orleans, USA, on 20 and 21 January 2020. It will be co-located with the POPL (Principles of Programming Languages) conference. See the forthcoming call for paper for details. We hope you will consider submitting your best AR-related work at CPP.
Topics of Interest
FM 2019 encourages submissions on formal methods in a wide range of
domains including software, computer-based systems,
systems-of-systems, cyber-physical systems, human-computer
interaction, manufacturing, sustainability, energy, transport, smart
cities, and healthcare. We particularly welcome papers on techniques,
tools and experiences in interdisciplinary settings. We also welcome
papers on experiences of formal methods in industry, and on the design
and validation of formal methods tools. The broad topics of interest
for FM 2019 include, but are not limited to:
Important Dates
For more information, see the symposium web page.
The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability.
The TAP conference aims to promote research in the intersection of testing and proving by bringing together researchers and practitioners from both areas of verification.
Topics of Interest
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
For more information, see the conference web page.
The ITP conference series is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics. This will be the 10th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988.
Paper Submission
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, see the conference web page.
MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.
Topics include, but are not limited to, the following:
Important Dates
More information is available on the homepage of the conference.
MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.
Topics include, but are not limited to, the following:
Important Dates
More information is available on the homepage of the conference.
The conference brings together researchers working on mathematical foundations of quantum physics, quantum computing, and related areas, with a focus on structural perspectives and the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods, and other computer science techniques applied to the study of physical behaviour in general. Work that applies structures and methods inspired by quantum theory to other fields (including computer science) is also welcome.
Important Dates
For more information see the conference web page.
The Programme Committee invites submissions for contributions on all aspects of logic, language, and computation. Work of an interdisciplinary nature is particularly welcome. Areas of interest include, but are not limited to:
Important Dates
Programme and submission details can be found here.
MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged.
Topics include, but are not limited to, the following:
Important Dates
More information is available on the homepage of the conference.
CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science. CALCO 2019 is co-located with MFPS XXXV.
Topics of Interest
Typical, but not exclusive topics of interest are:
Important Dates
More information is available on the homepage of the conference.
The 26th edition of the SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software, but does not exclude analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, and empirical evaluation.
Topics of interest include, but are not limited to:
Important Dates
Please keep in mind the following dates for submission:
For more information, see the symposium web page.
The purpose of the CONCUR conferences is to bring together researchers, developers, and students in order to advance the theory of concurrency, and promote its applications.
Topics
Submissions are solicited in semantics, logics, verification and analysis of concurrent systems. The principal topics include (but are not limited to):
Important Dates
All dates are AoE.
More information is available on the homepage of the conference.
Static analysis is widely recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of Static Analysis Symposia has served as the primary venue for the presentation of theoretical, practical, and application advances in the area.
Topics
The technical program for SAS 2019 will consist of invited lectures and
presentations of refereed papers. Contributions are welcomed on all aspects of
static analysis, including, but not limited to:
Important Dates
More information can be found on the symposium web page
The aim of the FMICS conference series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.
Topics
Topics of interest include (but are not limited to):
Important Dates
More information is available on the homepage of the conference.
TABLEAUX is the main international conference at which research on all aspects — theoretical foundations, implementation techniques, systems development and applications — of the mechanization of tableaux-based reasoning and related methods is presented. TABLEAUX has been held every year since 1992. Starting in 1995, the proceedings have been published in Springer's LNCS/LNAI series. TABLEAUX 2019 will be co-located with the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019). The two conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions
Scope of Conference
Tableau methods offer a convenient and flexible set of tools for automated
reasoning in classical logic, extensions of classical logic, and non-classical
logics. Areas
of application include verification of software and computer systems,
deductive databases, knowledge representation and its required inference engines, teaching,
and system diagnosis.
Topics of interest include but are not limited to:
We also welcome papers describing applications of tableau procedures to real world examples. Such papers should be tailored to the tableau community, and should focus on the role of reasoning and on logical aspects of the solution.
Important Dates
For more information, please visit the conference website.
FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis. Starting in 2000, the conference proceedings have been published in Springer's LNCS/LNAI series. FroCoS 2019 will be co-located with the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019). The two conferences will provide a rich programme of workshops, tutorials, invited talks, paper presentations and system descriptions.
Scope of Conference
In various areas of computer science, such as logic,
computation, program development and verification, artificial intelligence, knowledge representation,
and automated reasoning, there is an obvious need for using specialized formalisms and
inference systems for selected tasks. To be usable in practice, these specialized systems must
be combined with each other and integrated into general purpose systems. This has led to the
development of techniques and methods for the combination and integration of dedicated formal
systems, as well as for their modularization and analysis. FroCoS traditionally focuses on these types
of research questions and activities.
Like its predecessors, FroCoS 2019 offers a
forum for research in the general area of combination, modularization, and integration of systems,
with emphasis on logic-based methods.
Topics of interest
Important Dates
For more information, please visit the conference website.
The PPDP 2019 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.
Scope
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
Important Dates
For more information, see the symposium web page
The International Conference on Mathematics of Program Construction (MPC) aims to promote the development of mathematical principles and techniques that are demonstrably practical and effective in the process of constructing computer programs.
Scope:
MPC seeks original papers on mathematical methods and tools put to use
in program construction. Topics of interest range from algorithmics to
support for program construction in programming languages and systems.
Typical areas include type systems, program analysis and transformation,
programming language semantics, security, and program logics. The notion
of a 'program' is interpreted broadly, ranging from algorithms to hardware.
Theoretical contributions are welcome, provided that their relevance to program construction is clear. Reports on applications are welcome, provided that their mathematical basis is evident. We also encourage the submission of 'programming pearls' that present elegant and instructive examples of the mathematics of program construction.
Timeline:
More information is available on the conference web page.
SEFM aims to bring together leading researchers and practitioners from academia, industry, and government, to advance the state of the art in formal methods, to facilitate their uptake in the software industry, and to encourage their integration within practical software engineering methods and tools.
Topics of interest include, but are not limited to, the following aspects of software engineering and formal methods:
Important Dates
More information is available on the homepage of the conference.
The aim of the colloquium is to bring together practitioners and researchers from academia, industry and government to present research results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing. ICTAC also aims to promote research cooperation between developing and industrial countries. The proceedings will be published as a volume of Springer's LNCS series.
Topics of interest include, but are not limited to, the following:
The important dates are:
More information is available on the colloquium web page.
FMCAD 2019 is the nineteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.
Topics of Interest
FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods and their applications to computer-aided design.
Topics of interest include (but are not limited to):
Important Dates
For more information, see the conference web page.
Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science.
List of topics:
Dates:
For more information, see the conference web page.
ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of five main annual conferences, accompanied by satellite workshops. ETAPS 2019 is the twenty-second event in the series.
Main Conferences (8-11 April)
TACAS '19 hosts the 8th Competition on Software Verification (SV-COMP) and TOOLympics, an event to celebrate the achievements of the various competitions or comparative evaluations.
Satellite Events (6-7 April)
18 satellite workshops and other events will take place before
ETAPS 2019: DICE-FOPARA, GaLoP, HSB, QAPL, SynCoP, VerifyThis,
TOOLympics (6-7 April) BEHAPI, InterAVT, LiVe, MeTRiD, PERR (6 April)
CREST, HCVS, PLACES, SPIoT, SYNTCOMP Camp,
Mentoring Workshop (7 April)
See the full program here.
For more information, see the joint conferences web page.
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry require advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The 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.
New developments and emerging applications like autonomous software for uncrewed deep space human habitats, caretaker robotics, Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), and the need for system-wide fault detection, diagnosis, and prognostics provide new challenges for system specification, development, and verification approaches. The focus of these symposiums are on formal techniques and other approaches for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle.
The NASA Formal Methods Symposium is an annual event organized by the NASA Formal Methods (NFM) Steering Committee, comprised of researchers spanning several NASA centers. NFM 2019 is being co-organized by Rice University and NASA- Johnson Space Center in Houston, TX.
Location & Cost:
The symposium will take place in the McMurtry Auditorium, Rice University, Houston, Texas, USA, May 7--9, 2019. Travel information and discounted hotel reservations can be found here. Houston hotel space is scarce for these dates and the hotel block expires March 20.
There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to attend, to listen to the talks, and to participate in discussions; however, all attendees must register.
For more information, see the symposium's web page.
iFM 2019 is concerned with how the application of formal methods may involve modelling different aspects of a system which are best expressed using different formalisms. Correspondingly, different analysis techniques may be used to examine different system views, different kinds of properties, or simply in order to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modelling and analysis; i.e., the combination of (formal and semi-formal) methods for system development, regarding modelling and analysis, and covering all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.
Besides the standard conference track and the Doctoral Symposium, iFM will host a number of workshops and tutorials related to the theme of the conference. The purpose of the workshops is to provide participants with a friendly, interactive atmosphere for presenting novel ideas and discussing their application. The goal of the tutorials is to enable the participants to familiarise themselves with theoretical aspects and application of formal methods.
Proposals must be written in English, not exceed 5 pages with a reasonable font and margins, and be submitted in PDF format via email to the iFM workshop chairs, Martin Leucker and Violet Ka I Pun.
Workshop proposals should include:
Important Dates
More information is available on the homepage of the conference.
The FSCD conference covers all aspects of Formal Structures for Computation and Deduction from theoretical foundations to applications. The annual FSCD conference comprises the main conference and a considerable number of affiliated workshops (expectedly, more than ten).
We invite proposals for locations to host the 6th FSCD International Conference to be held during the summer of 2021. Previous (and upcoming) FSCD meetings include:
The deadline for proposals is 31st March 2019. Proposals should be sent to the FSCD Steering Committee Chair (see contact information above). We encourage proposers to register their intention informally as soon as possible. Selected proposals are to be presented at the business meeting of FSCD 2019 taking place at Dortmund in June 2019. The final decision about hosting and organising of FSCD 2021 will be taken by the SC after an advisory vote of the members of the community in attendance at the business meeting.
Proposals should address the following points:
Learning models defining recursive computations, like automata and formal grammars, are the core of the field called Grammatical Inference (GI). The expressive power of these models and the complexity of the associated computational problems are major research topics within mathematical logic and computer science, spanning the communities that the Logic in Computer Science (LICS) conference brings together. Historically, there has been little interaction between the GI and LICS communities, though recently some important results started 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 who could benefit from grammatical inference tools, and researchers in grammatical inference who could find in logic and verification new fruitful applications for their methods.
Topics of interest include (but are not limited to):
Important dates
More information is available on the workshop web page.
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems.
Topics of interest include:
Important Dates
More information is available on the homepage of the workshop.
Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and programming languages, supporting tool development and reasoning. LSFA 2019 will be a satellite event of CADE-27.
Topics of interest include, but are not limited to:
Important Dates:
More information is available on the LSFA web page.
The PxTP workshop brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms. PxTP 2019 is affiliated with the 27th International Conference on Automated Deduction (CADE-27).
The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation of such tools in larger verification environments has demonstrated the potential to reduce the amount of manual intervention. Examples include the Sledgehammer tool providing an interface between Isabelle and (untrusted) automated provers, and also collaboration between HOL Light and Isabelle in the formal proof of the Kepler conjecture.
Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop strives to encourage such cooperation by inviting contributions on suitable integration, translation and communication methods, standards, protocols, and programming interfaces. The workshop welcomes the interested developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and interfaces, and producers of standards and protocols. We are also interested both in success stories and in descriptions of the current bottlenecks and proposals for improvement.
Topics
Topics of interest for this workshop include all aspects of cooperation between reasoning tools, whether automatic or interactive. More specifically, some suggested topics are:
Important Dates
More information is available on the homepage of the workshop.
The main goal of this workshop is to bring together key people from various sub-communities of automated reasoning—such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving—to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community.
The structure of the workshop will be informal. We invite extended abstracts in the form of non-technical position statements aimed at prompting lively discussion. The title of the workshop is indicative of the kind of discussions we would like to encourage:
Important dates are not yet known. Check the ARCADE homepage for more information.
Unification is concerned with the problem of making two terms equal, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc.
Traditionally, the scope of the UNIF workshops has covered the topic of unification in a broad sense. Topics of interest to this forum include, but are not limited to:
The workshop is proposed to be hosted by the 4th International Conference on Formal Structures for Computation and Deduction (FSCD, Dortmund, 24-29 June 2019).
Important Dates
For more information, see the homepage of the workshop.
Interaction and Concurrency Experiences (ICEs) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools, and programming primitives for complex interactions. ICE 2019 is a satellite workshop of DisCoTec 2019.
The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models. We solicit contributions relevant to Intereaction and Concurrency, including but not limited to:
Important dates
More information is available on the workshop web page.
The Coq workshop is part of ITP 2019.
While conferences usually 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.
We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop.
Relevant subject matter includes but is not limited to:
Important dates:
For more information, go to the workshop web page.
Interaction and Concurrency Experiences (ICEs) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools, and programming primitives for complex interactions. ICE 2019 is a satellite workshop of DisCoTec 2019.
The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models. We solicit contributions relevant to Intereaction and Concurrency, including but not limited to:
Important dates
More information is available on the workshop web page.
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. NSV 2019 is co-located with CAV.
Topics of interest:
The scope of the workshop includes, but is not restricted to, the following topics:
Important Dates:
More information is available on the workshop web page.
The Coq workshop is part of ITP 2019.
While conferences usually 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.
We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop.
Relevant subject matter includes but is not limited to:
Important dates:
For more information, go to the workshop web page.
Confluence provides a general notion of determinism and has always been conceived as one of the central properties of rewriting. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certification as well as new applications. The workshop aims at promoting further research in confluence and related properties. It is collocated with FSCD.
Confluence relates to many topics of rewriting (completion, modularity, termination, commutation, etc.) and has been investigated in many formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting, conditional rewriting, etc. Recently there is a renewed interest in confluence research, resulting in new techniques, tool supports, certification as well as new applications.
Topics:
Important Dates
More information about the workshop can be found in the home page of IWC.
A core goal of Bridging-the-gap-Workshops is to make results from psychology, cognitive science, and AI accessible to each other. The goal is to develop systems that can adapt themselves to an individuals' reasoning process and that such systems follow the principle of explainable AI to ensure trustfulness and to support the integration of results from other fields. We propose a human syllogistic reasoning challenge to predict future inferences of an individual reasoner based on some previous observations. Hence, participants can develop cognitive AI models (written in Python) that predict the next inference. These predictions are then evaluated in the CCobra framework.
Despite a common research interest -- reasoning -- there are still several milestones necessary to foster a better inter-disciplinary research. First, to develop a better understanding of methods, techniques, and approaches applied in both research fields. Second, to have a synopsis of the relevant state-of-the-art in both research directions. Third, to combine methods and techniques from both fields and find synergies. E.g., techniques and methods from computational logic have never been directly applied to model adequately human reasoning. They have always been adapted and changed. Fourth, we need more and better experimental data that can be used as a benchmark system. Fifth, cognitive theories can benefit from a computational modeling. Hence, both fields -- human and automated reasoning -- can both contribute to these milestones and are in fact a conditio sine qua non. Achievements in both fields can inform the others. Deviations between fields can inspire to seek a new and profound understanding of the nature of reasoning. Additionally to predict human inferences is a major step that can help to foster the integration of digital companions and cognitive assistance systems into our everyday life. An important condition is that such systems can adapt themselves to an individual's reasoning process and that such systems follow the principle of explainable AI to ensure trustfulness and to support the integration of results from other fields. Symbolic approaches do provide an easier access to it.
Topics of interest include, but are not limited to the following:
The workshop will be located at the 28th International Joint Conference on Artificial Intelligence (IJCAI 2019) at Macao, China. The Bridging workshop is supported by IFIP TC12.
Important Dates
More information is available on the workshop's web page.
Building on the pioneer intuitions of Floyd-Hoare logic, dynamic logic was introduced in the 70's as a suitable logic to reason about, and verify, classic imperative programs. Since then, the original intuitions grew to an entire family of logics, which became increasingly popular for assertional reasoning about a wide range of computational systems. Simultaneously, their object (i.e. the very notion of a program) evolved in unexpected ways. This lead to dynamic logics tailored to specific programming paradigms and extended to new computing domains, including probabilistic, continuous and quantum computation. Both its theoretical relevance and practical potential make dynamic logic a topic of interest in a number of scientific venues, from wide-scope software engineering conferences to modal logic specific events. However, no specific event is exclusively dedicated to it. This workshop aims at filling fill such a gap, joining an heterogeneous community of colleagues, from Academia to Industry, from Mathematics to Computer Science.
Topics
Submissions are invited on the general field of dynamic logic, its
variants and applications, including, but not restricted to
Important Dates
More information is available on the workshop's web page.
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.
Ideally, an F-IDE dedicated to such developments should comply with several requirements. The first one is to associate a logical theory with a programming language, in a way that facilitates the tightly coupled handling of specification properties and program constructs. The second is to offer a language/environment simple enough to be usable by most developers, even if they are not fully acquainted with higher-order logics or set theory, in particular by making development of proofs as easy as possible. The third is to offer automated management of application documentation. It may also be expected that developments done with such an F-IDE are reusable and modular. Tools for testing and static analysis may be embedded within F-IDEs to support the assessment process.
List of Topics
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. Topics of interest include, but are
not limited to, the following:
The F-IDE workshop is part of FM Week 2019.
Important Dates
More information is available on the workshop's web page.
HOR is a forum to present work concerning all aspects of higher-order rewriting. HOR 2019 is affiliated with FSCD 2019.
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.
Topics
The following is a non-exhaustive list of topics for the workshop:
Important Dates
More information can be found on the workshop's web page.
The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally-based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area.
Topics of interest in the scope of this workshop include:
Important Dates
More information is available on the homepage of WPTE 2019.
SD’19 is the fifth in a series of workshops aiming to gather various communities of structural proof theorists. As well as theoretical work in the form of regular papers, we encourage submission of implementations, tools and system descriptions. SD'19 is affiliated with FSCD 2019
Topics of interest
Important Dates
More information is available on the homepage of the workshop.
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. The program will consist of invited lectures as well as contributed talks selected by the Program Committee. LCC 2019 is collocated with ICALP 2019.
Important Dates:
More information is available on the homepage of the workshop.
Women are chronically underrepresented in the LiCS community. 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. WiL 2019 is affiliated with the Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
Previous versions of Women in Logic (Reykjavik, Iceland 2017 and Oxford, UK 2018) were very successful in showcasing women's work and as catalysts for recognition of the need for change in the community. Our extended program committee tries to cover most areas of Logic in Computer Science. These include but are not limited to the usual Logic in Computer Science (LICS) topics. These are:
Important Dates
More information is available on the homepage of the workshop.
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 2019 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
Important Dates
More information is available on the homepage of the workshop.
Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses, and many recent advances in the Constraint/Logic Programming, Verification, and Automated Deduction communities have centered around efficiently solving problems presented as Horn clauses.
This workshop aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE), on the topic of Horn clause based analysis, verification and synthesis.
Horn clauses have been advocated by these communities at different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.
Aims and Scope
Topics of interest include but are not limited to the use of Horn
clauses, constraints, and related formalisms in the following areas:
CHC-COMP
HCVS 2019 will host the 2nd CHC competition (CHC-COMP), which will
compare state-of-the-art tools for CHC solving for performance and
effectiveness on a set of publicly available benchmarks.
More information can be found on the competition's web page.
All participants of CHC-COMP are invited (but not obliged) to submit
a tool description for publishing either online or at the proceedings
through the EasyChair system for HCVS (the HCVS deadlines apply).
Important dates
More information is available on the homepage of the workshop.
The Computational Logic and Applications (CLA) workshops are a series of annual meetings, whose main purpose is to provide a free and open forum for research on combinatorial and quantitative aspects of mathematical logic and their applications in computer science.
Scope
Topics within the scope of CLA include:
Special Issue
Following the meeting, a special issue of DMTCS is planned for early 2020 with full papers on the topics of CLA. These papers can be either results presented at the 2019 CLA meeting, or at a former meeting but not published elsewhere, or results not presented at CLA, as long as they fall within the scope of the workshop. The submitted papers should present original research, including survey papers, which is not already published or submitted to publication to another journal.
More information is available on the homepage of the workshop.
This is the first call for participation for a one-day meeting in memory of Martin Hofmann in Munich on Saturday, 13 July 2019.
We will meet to remember and celebrate Martin's life and work. There will be invited talks from friends and colleagues as well as ample time for discussions and exchange of memories during the breaks. The talks will be about various topics in Computer Science and Mathematics that Martin would have enjoyed. The talks will combine scientific content with personal stories about Martin.
If you are planning to attend then please register on the website of the meeting.
There may be a small registration fee to help cover refreshments; more information later.
If you would like to propose a contribution to the program then contact Jan Hoffmann or Don Sannella.
Important Dates:
Computational complexity theory was born more than 50 years ago when researchers started asking themselves what could be computed efficiently. Classifying problems/functions with respect to the amount of resources (e.g. time and/or space) needed to solve/compute them turned out to be an extremely difficult question. This has led researchers to develop a remarkable variety of approaches, employing different mathematical methods and theories.
The future development of complexity theory will require a subtle understanding of the similarities, differences and limitations of the many current approaches. In fact, even though these study the same phenomenon, they are developed today within disjoint communities, with little or no communication between them (algorithms, logic, programming theory, algebra...). This dispersion is unfortunate since it hinders the development of hybrid methods and more generally the advancement of computational complexity as a whole.
The goal (and peculiarity) of the Caleidoscope school is to reunite in a single event as many different takes on computational complexity as can reasonably be fit in one week. It is intended for graduate students as well as established researchers who wish to learn more about neighbouring areas.
Lectures
More information is available on the school's web page.
Rewriting is a simple yet powerful model of computation with numerous applications in computer science and many other fields: logic, mathematics, programming languages, model checking, quantum computing, biology, music...
ISR'19 is hosted in the center of Paris and proposes to master students, PhD students and researchers, two parallel tracks:
Registration is open until May 17!
More information is available on the school's web page.
The Midlands Graduate School (MGS) in the Foundations of Computing Science provides an intensive course of lectures on the mathematical foundations of computing. The MGS has been running since 1999, and is aimed at PhD students in their first or second year of study, but the school is open to everyone, and has increasingly seen participation from industry. We welcome participants from all over the world!
Courses:
Eight courses will be given. Participants usually take all
the introductory courses and choose additional options from
the advanced courses depending on their interests.
The registration deadline is Sunday, 31 March. Spaces are limited, so please register early to secure your place.
For more information, see the school's web page.
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 ninth 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.
The lecturers at the school include:
Applicants are urged to submit their applications before April 30, 2019, since there are only a limited number of spaces available. Non-US applicants requiring US visas are requested to apply early. We strongly encourage the participation of women and under-represented minorities in the summer school.
For more information and to apply go to the summer school web page.
The 40th edition of the International Summer School Marktoberdorf 2019 based on the excellent networking in the Summer School Marktoberdorf series on Safety and Security of Software Systems: Logics, Proofs, Applications is now ready for application. Deadline is: April 7, 2019.
The "Marktoberdorf Summer School" is a ten days' course for young computer scientists and mathematicians working in the field of formal software and systems development. It takes place at the little town of Marktoberdorf, this year from July 31 to August 9, 2019.
Our challenge is to give in-depth presentations of state-of-the-art topics in verification for safety and security of software systems and to promote international contacts and collaborations between leading researchers and young scientists.
Further information including lecturers, topics and the application form are available on the web page of the summer school.
If you have further questions, please do not hesitate to contact us via email.
The fourth international autumn school "Proof and Computation" will be held from 20th to 26th September 2019 in Herrsching near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy.
Scope
Deadline for applications: 31st May 2019. Applicants will be notified by 28th June 2019.
More information such as financial support and application procedure are available on the school's web page.
In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-27 will be held during the 27th International Conference on Automated Deduction (CADE-27).
CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of:
Deadlines and Important Dates
Go to the CASC homepage for more information.
This is a call for participation for the 6th Syntax-Guided Synthesis Competition to be organized as a satellite event of SYNT & CAV 2019 in New York City.
The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementation. The motivation is twofold. First, narrowing the space of implementations makes the synthesis problem more tractable. Second, providing a specific syntax can potentially lead to better optimizations.
The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions that satisfies the specification in the given theory. The formulation of the problem builds on SMT-LIB.
There has been a lot of recent interest in both using SyGuS solvers for various synthesis applications and developing different solving algorithms. Despite significant progress in solution strategies in the last few years, synthesis remains a challenging problem. Last year, in the general track, more than 25% of the problems were unsolved, and we welcome solvers that can advance the state of the art.
Important Dates:
For more information see the sygus webpage. For questions regarding the competition please contact the organizers.
We are seeking to appoint a PhD student in UCL’s Programming Principles, Logic, and Verification (PPLV) group,to work alongside the EPSRC-funded project “A coalgebraic framework for reductive logic and proof-search (ReLiC)”.
The project is led by David Pym (PI), Alexandra Silva, and Simon Docherty (Co-Is). Facebook (Peter O’Hearn) is a partner in the project.
The position is available from 23 September 2019 for 4 years. The starting stipend will be approximately £17,280, with an approximate annual uplift of 3%.
We are looking for a talented, highly motivated student interested in working on some aspects of the project. Here is a description of the project.
The traditional treatment of logic is that of a deductive science: from axioms, conclusions are deduced according to formal proof rules. However, in practice many applications of logic and mathematical reasoning proceed in the opposite direction: from a putative conclusion, one finds sufficient axioms from which it may be concluded. This proceeds not by a step-by-step application of proof rules, but instead by the systematic reduction of the space of possible (deductive) proofs. We call this the reductive approach to logic. Archetypal examples of reductive reasoning in computer science include automated theorem proving, logic programming languages such as PROLOG, and precondition inference in program verification.
The ReLiC project aims to produce a uniform mathematical foundation for reductive logic via the framework of coalgebra and coinduction. Coalgebra can fruitfully be seen as a unifying formalism for stateful systems, while coinduction is a closely connected proof principle based on the reduction of goals into subgoals. In doing so we aim to
We are looking for a student with an excellent first degree in mathematics, computer science, philosophy, or another mathematical discipline, who has a strong background and interest in logic. Ideally, candidates will also have an excellent, relevant Master’s degree and strong programming skills.
For an informal discussion of the position, please contact David, Alexandra, or Simon.
To apply, please follow the instructions here and indicate clearly on your application that you are applying for this Scholarship ("A Coalgebraic framework for reductive logic and proof-search") under the scholarships section, or in your personal statement.
We are advertising both fixed term and tenure track positions in computer sciences from level B (assistant professor), level C (associate professor) and level D (associate professor plus plus :)
See here.
Canberra is a great place to live! See here.
We are also into proof-theory, formal verification using HOL4, Isabelle/HOL and Coq, type-theory and other topics which should be music to your ears, see here.
Please feel free to contact me if you wish to discuss applying.
And I promise that there are no crocodiles, jellyfish or sharks in our lake! See here.
A PostDoc position is available in my group at Inria Paris on Formally Secure Compilation in Coq. I am seeking outstanding candidates with a strong, internationally competitive research track record. Particularly interesting for us is research expertise in:
Candidates are expected to work collaboratively on project-relevant topics and help advise students, but can also dedicate some of their time to their own independent projects. For exceptional candidates with enough experience we can also discuss about Starting Researcher positions, who can propose and follow their own research agenda and be fairly independent. Our team can also support such exceptional candidates for permanent Researcher positions funded and awarded competitively by Inria. Further details about these various positions are available here.
Do not hesitate to contact me if you are interested!
There is a vacancy for either a PhD student (up to 4 years) or a Postdoc (2 years) in the Software Engineering group at TU Darmstadt, Germany. We perform cutting-edge research in the intersection between software engineering and formal methods, being a co-developer of the leading static verification tool KeY. You will work in a DFG-funded project that looks at one of the most intriguing questions in software analysis: how can information from static verification be combined with information obtained at runtime? We will investigate methodologies and data structures suitable to represent information from hybrid sources. To this end we team up with the group of Bernhard Steffen at TU Dortmund who develop LearnLib , a leading tool for automated learning of automata-based models from execution traces.
The salary follows the E13 scale . You will work in an international research group with a friendly and supportive climate. TU Darmstadt offers excellent training and development opportunities for young researchers.
Prerequisites:
For a PhD position we expect a very good MSc degree in Computer
Science or a closely related field, as well as documented research
exposure in an area relevant to the position, for example, a first
publication or an excellent, research-oriented MSc thesis. For a
postdoc position we expect a PhD in a relevant area, such as software
engineering, formal methods, static analysis, or programming languages
as well as several international, peer-reviewed publications.
The position is available immediately.
For further questions about the position, please contact Prof Dr Reiner Hähnle.
Please send your application consisting of the usual material (cover letter, CV, papers, thesis, grade record, name of one or two references) as a zip file to this email address.
Lean Forward is an ambitious research project that aims at formally proving theorems in research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles, by collaborating with number theorists. The project is funded by an NWO Vidi grant from January 2019 to December 2023 and is hosted by the Vrije Universiteit Amsterdam.
As part of this project, we will develop formal libraries of fundamental number theory in Lean and explore how to automate proof search in these. Moreover, we will develop techniques and tools that help mathematicians perform accurate computations and reasoning using proof assistants, integrating procedures from computer algebra systems in a foundational, verified fashion. The ultimate aim is to contribute to the development of a proof assistant that actually helps mathematicians by making them more productive and more confident in their results.
We are looking for outstanding candidates for several fully funded, four-year PhD positions, due to start in 2019 or early 2020. Candidates should ideally have some experience with (automatic or interactive) theorem proving or mathematics and be at ease with both theory and engineering. Please contact me for more information.
Applications are invited for multiple positions (PhD/Postdoc/Scientific Programmer) at the IMDEA Software Institute, Madrid, Spain.
Selected candidates will work under the supervision of Aleks Nanevski. The topic of the research, to be determined based on the common interests of the candidate and the supervisor, will be in the areas of software verification, logics for concurrent programs, and language-based security. The research will be funded by Aleks' ERC Consolidator award "MATHADOR: Type and Proof Structures for Concurrent Software Verification", which aims to investigate the type-theoretic foundations for verification of concurrent software.
PhD candidates should have an excellent MSc or BSc degree in computer science or a related subject, with an interest in the above areas, and a strong commitment to research.
Postdoc candidates should have, or expect shortly to obtain, a PhD in computer science. The ideal candidate will have expertise in program semantics and program logics, concurrent or distributed computing, type theory or interactive theorem proving, as they apply to the above areas.
Scientific programmer candidates should hold a BSc or MSc degree in computer science, with experience in and passion for functional programming and interactive theorem proving (eg., Coq).
All positions require good teamwork and communication skills, including excellent spoken and written English. Salaries at IMDEA Software Institute are internationally competitive.
For any questions about these positions, please contact Aleks directly.
Deadline for applications is March 31st, 2019. Review of applications will begin immediately.
Applications should be submitted online here.
The UK Research Institute in Verified Trustworthy Software Systems and the UK's National Cyber Security Centre have provided a fully funded 3.5-year PhD scholarship (for UK/EU students) to work on concurrency, programming languages and formal methods in Mark Batty's group at the University of Kent in Canterbury, UK. Applications are due by the 26th April 2019.
The post is suited to a wide range of applicants with formal or practical skills: you will join a team that spans theory (formal semantics, verification, proof) and practice (tool building, concurrent programming, compilation).
The project will focus on concurrency in mainstream programming languages where our work has found fundamental problems and made changes to the C and C++ standards through the International Standards Organisation (ISO). The specifications of Languages like C/C++ and Java do not adequately describe when the programmer can rely on the compiler to leave program dependencies in place, or when the optimiser is free to remove them. Removing dependencies can lead to unexpected concurrency behaviour as it enables speculative execution on the processor. Industry bodies like the ISO know that their specifications are broken and keenly await a fix. We have a fix, and we are building tools and verification techniques around it. The PhD project focusses on this area of research.
This research is part of PLAS, one of the largest programming languages research groups in Europe. It is currently ranked 17th worldwide by the independent CSrankings website. We provide a supportive environment for research and we have a vibrant postgraduate population. We encourage our students to engage with the wider research community through attending conferences and taking internships with leading industrial companies. We are located in Canterbury, a lively and cosmopolitan historic town with convenient travel links to London and Europe.
Application process:
Mark Batty's web page.
Programming Languages and Systems Group's web page.
Applications process web page.
The studentship covers UK/EU fees, a travel budget and a stipend for 3.5 years. There is an option to teach, but no requirement. Non-EU students are welcome to apply but are subject to higher fees and would need to find funding for the difference.
Laboratory
The Laboratory of Fundamental Computer Science of Orleans (LIFO, EA 4022) is a laboratory of the University of Orleans and INSA Center-Val de Loire. Research conducted at LIFO ranges from algorithmics to natural language processing, from automatic learning to massive parallel computing, from verification and certification to system security.
Team
The aim of the LMV team is to improve the understanding of safety and security of computer systems. From "partial order" logic to usual programming languages, the team members work on these questions at different levels of abstraction.
Funding : Fully-funded 3-years scholarship from the French Ministry for Education and Research
Subject : The reactive synchronous programming model [9] is a relaxation of the ESTEREL model [6]. In the latter, a collection of processes progress by successive phases of global synchronization (“ clock ticks ”) and communicate by events. At each instant (a phase between two ticks) each component reacts to the presence / absence of events. While the ESTEREL model solves the problem of causality posed by the instantaneous reaction to absence by restricting the expressivity of the language, the synchronous reactive model delays reaction to absence (the absence of a signal can not be decided before the end of an instant). Several works have focused on the semantic study of languages derived from this model [2, 5, 3] and on the analysis of the properties of such programs [4, 12]. Other works have successfully studied the possibility of using this programming model in the context of mobility [7]. Implementations of this programming model have been proposed for several languages like C, Scheme, Ocaml and Java [8, 13, 10, 11]. In [9], the authors propose a version of this model supporting strong security properties.
In this thesis, we will focus on a purely functional approach of the synchronous reactive model (existing languages have imperative features). As a first step, the selected candidate will have to carry out the semantic study of a programming language based on this model. An obvious starting point will be the article [1]. In a second step, the definition of desirable properties for the programs of this language will lead to the implementation of verification tools dedicated to these properties. The different developments will have to be formalized using the Coq proof assistant. Depending on the results obtained, the automatic extraction of code from the latter may be considered.
From an applied point of view the objective of this thesis is to propose a high-level programming language for the Internet Of Objects. In particular, such a language should make it possible to deploy a program, conceived in a global manner, on the different actors of a communicating scenario.
Application
We are happy to provide more details to potential applicants. Requests for additional information regarding the project’s content/motivation, other informal enquiries, and formal applications can be sent to Frédéric Dabrowski. Formal applications must include:
Deadline for applications: May 15th 2019.
References
We are looking for a PhD student to work in the BioComputing group (University of Lille, France) on formal methods (especially inspired by logic and semantics of programming languages) for modeling and static analysis of biological systems. More precisely, the thesis entitled “Computational Models of Intestinal Glucose Absorption for Diabetes Prediction”, aims at developing new computational methods for the prediction of glucose intestinal absorption at the physiological and cellular level in order to improve the understanding of diabetes pathology. In addition of having a background in formal methods, we expect candidates interested in health sciences and biology. For more details, see here.
The thesis will be co-supervised by Cédric Lhoussaine and François Pattou (Professor of Surgery). The starting date will be September or October 2019. Potential candidates are encouraged to contact Cedric Lhoussaine as early as possible. The deadline for application is 1st of May.
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 one year, full-time on research (no teaching duties), flexible in terms of research topic, and with a competitive salary. Recent PhD graduates in Computer Science or related fields, scientists at the postdoc level who wish further experience towards a tenure-track position, or who need a bridge between positions, faculty on paid leave of absence for six months who wish to extend it to twelve, and active in any topic in automated reasoning, are invited to get in touch by e-mail with Maria Paola Bonacina. Applications will be considered as soon as received. An official application with the University will have to be filed in the window between April 26 - May 16.
If only there were a place where I could prove theorems, change the world, and have fun while doing it...
Sounds too good to exist?
In the Trustworthy Systems team at UNSW and 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 offering scholarships to multiple motivated PhD students who want to join us in Sydney, move things forward, and have a global impact.
Cogent is a language we designed that co-generates code and proofs in order to ease the verification of systems components around seL4. Potential PhD topics include designing and implementing new domain-specific programming languages extending Cogent, writing formal specifications and proofs in Isabelle/HOL, developing formally verified infrastructure for building secure systems on top of seL4, contributing to improved proof automation and reasoning techniques, and applying formal proof to real-world systems and tools.
To apply you should have (or be about to obtain) a bachelor degree (minimum 4 years) or a bachelor and a masters degree in Computer Science, Mathematics, or similar.
You should also possess a significant subset of the following skills:
If you additionally have experience
You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages.
Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements.
We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See here for more information.
For applying, email us a copy of your CV, cover letter, transcripts, and contact information for two referees.
This round of applications closes on the 19th of April 2019.
For any questions on these positions, please contact Christine Rizkallah.
The seL4 code and proof, and the Cogent project, are open source.
More information about the Trustworthy Systems team is available here.
Still studying? We also have internship opportunities!
The Department of Information Technology, Uppsala University, opens a fully paid PhD student position in Computer Science, on SMT Reasoning for Security Analysis. The main advisor of the PhD student will be Philipp Rümmer. The topic of the PhD position is (i) to develop and extend SMT technology tailored to security analysis, in particular methods and tools for relevant theories such as strings, fragments of word equations, and regular expression constraints, and to (ii) investigate and improve SMT-based methods for security analysis, possibly including approaches like whitebox fuzzing, model checking, symbolic execution, and variants of taint tracking.
About the project: The funding for the PhD position is part of the ambitious framework project WebSec: Securing Web-driven Systems, funded by the Swedish Foundation for Strategic Research (SSF) and dedicated to principled security and privacy for the web. The project is a collaboration between Chalmers in Gothenburg (project leader: Andrei Sabelfeld) and Uppsala University (PI: Philipp Rümmer), and the PhD student will have the opportunity to work together with several world-leading groups at both universities: the Embedded Systems, Algorithmic Program Verification, and Optimization group in Uppsala, and the Information Security group at Chalmers. Information about WebSec is given here.
Requirements: The candidate should have a Master of Science in computer science, computer engineering, or equivalent, with a solid grasp in SMT or constraint solving, security, formal methods, and language technology such as compiler construction. Good programming skills and communication skills are required in this project. We expect the student to have demonstrated ability to do research, as seen through his/her MS thesis. Excellent skills in spoken and written English are an absolute requirement.
For more details and instructions on how to apply see the position description. More information on what support you can expect is given on this web page.
As part of the ERC Consolidator Grant "Certified Quantum Security" and the US Airforce project "Verification of Quantum Cryptography", we are looking for postdocs to work on verification of quantum cryptography (or more generally on quantum cryptography).
We will develop methods for the verification of proofs in quantum cryptography. Similar to what the EasyCrypt tool does in classical cryptography. The scope of the project covers everything from the logical foundations, through the development of tools, to the verification of real quantum protocols.
The ideal candidate would have experience in:
Please contact Dominique Unruh if you have more questions about the project, the required background, Estonia, the position itself, or the application process. I can also provide a detailed description of the overall research project.
The salary range is 30000-36000 Euro per year (depending on experience), which is highly competitive in Estonia due to low costs of living and low income tax rate (20%), pension contributions and health insurance are covered by the employer.
Applications are accepted at any time (until all positions are filled), and positions can start as soon as possible. Positions are for 2-3 years (up to negotiation).
To apply, please send the following documents to Dominique Unruh:
A post-doctoral position is available in the Caramba team at Inria Nancy - Grand Est.
The goal of this project is to formally prove algorithms and code used by the GNU MPFR library.
Candidates should have a strong background in formal proof and in the C programming language.
Applications should be submitted before June 6 here.
As I wrote in the last issue of the newsletter, I believe it would be useful to some people to know the schedule of the AAR newsletter publication. This is now possible: I have put this information on my web page and it can also be accessed from the AAR Newsletters page.
* * *