In contrast to the focus in many of the columns I have written, a focus on proving one or more theorems, I suspect at least some of you would like a challenge that is of a more general nature.
I have in mind a challenge that would, if met, have a possibly dramatic effect on the performance of automated reasoning programs.
If you glance at an experiment with such a program, an experiment that did reach the goal but took considerable CPU time to reach the goal, you might discover that many, many conclusions were drawn and then discarded because of being identical to or an instance of a conclusion already retained.
In other words, both forward and back subsumption (so-to-speak) wasted much time, perhaps a rather large fraction of the time the program took to return the desired answer to the question under consideration.
Information that is subsumed is (in effect) redundant information.
In the presence of reflexivity, x = x, almost never is it of use to learn that a = a and b = b, for example.
In a problem in group theory, instances of the axiom of left identity are seldom edifying, instances of (where e denotes the identity) e+x = x.
In general, the challenge offered here asks for a way to avoid deducing most or all of the so-called redundant information. Since I am often preoccupied with various types of strategy, the challenge here asks for the formulation of a strategy to be employed to save the CPU time spent on deducing and discarding redundant information. I have no idea how to address the challenge, and I suspect an understandable immediate reaction is that no appropriate strategy can be formulated. But, especially for those who might enjoy history, and also to show how apparently formidable obstacles were overcome, I turn to the early 1960s.
Let us look at a different aspect of time that can be wasted.
Generally speaking, if a program spends huge amounts of time deducing conclusions that have no relevance to the theorem to be proved, that time is wasted.
Such was the case in the early 1960s; indeed, a simple theorem in group theory was in focus with the obvious objective of finding a proof.
The theorem asserted that commutativity holds (is provable) for groups in which the square of every element x is the identity e.
The proof eluded us, even when using a fine program designed and implemented by Dan Carson at Argonne National Laboratory.
The attempt ran out of memory -- specifically because too many clauses were deduced before a proof was found.
That simple exercise in group theory was the wellspring for the formulation of the set of support strategy.
In the set of support strategy, the program is prevented from applying the inference rule(s) in use to a set of clauses none of which are in a list designated as the set of support list.
The recommendation for the use of the strategy, in general, is to place all of the axioms of the area under study outside of the set of support list, list(sos) for Bill McCune's OTTER.
Typically, one places in the set of support list the so-called special hypothesis, if such exists, and possibly the denial of the conclusion of the theorem.
For example, in the context of the cited simple exercise from group theory, you would place xx = e and, possibly, ab != ba in the set of support list.
With such a placement, the program would not be able, while using the set of support strategy, to apply an inference rule to a set, say, consisting of left identity and associativity.
In other words, the program would not be exploring group theory as a whole.
For McCune's OTTER, the axioms of a group would be placed on list(usable) and used only to complete the application of an inference rule.
Among conclusions not drawn would be various lemmas about group theory, most or all would not be useful if, for example, trying to prove commutativity for groups in which the square of x, for all x, is the identity e.
But, you might well argue, isn't such a lemma essential? And the surprising answer is no. Intuition might suggest the need for such a lemma, but such is not the case -- provided, in general, that the complement of the chosen set of support is itself satisfiable. Indeed, without this lemma, a proof is guaranteed to be found when the complement of the chosen set of support is satisfiable -- quite intriguing! No wonder, then, that McCune considered this strategy to be very deep.
And with the use of the strategy, which restricts the actions of an automated reasoning program, the simple exercise was crushed. For one aspect, many conclusions were not drawn that otherwise would have been drawn, using up too much time. The use of the set of support strategy requires no CPU time (except in rather bizarre cases). This characteristic of the strategy is critical especially for much, much harder theorems.
As for the approach or strategy I have challenged you to develop, one that avoids generating redundant conclusions, some CPU time most likely will be required for its use. The aim is, of course, to minimize that time.
To further set the stage for the challenge I am issuing, I return to a study I made with my colleague D. Ulrich in 2006.
The area of logic concerned the formulas known, respectively, as B, C, and I.
The goal was to deduce from the following proposed single axiom the axiom system consisting of B, C, and I, but to find a very short proof, if such existed; the function i denotes implication.
P(i(i(i(x,x),i(y,z)),i(i(i(i(z,u),u),v),i(y,v)))).
The theorem to prove is the following in negated form.
% negation of the join of B, C, and I.
-P(i(i(a1,i(b,a2)),i(b,i(a1,a2)))) | -P(i(a1,a1)) | -P(i(i(a1,b),i(i(a2,a1),i(a2,b)))).
The only inference rule in use was hyperresolution, coupled with the following clause for condensed detachment.
-P(i(x,y)) | -P(x) | P(y).
Although a proof of length 20 was found in less than 2 CPU-seconds, far more CPU time was used to find a marvelous 16-step proof. More piquant, the 16-step proof happens to be level 10, not so deep a proof.
-----> EMPTY CLAUSE at 65197.30 sec ----> 1324675 [hyper,2,1321737,9972,1322447].
But what took so much time? Well, the following statistic sheds some light.
clauses forward subsumed 880401
Since the number of clauses forward subsumed is more than half of the number retained when a 16-step proof was found, this data suggests that much CPU time was consumed in the generation and then discarding of redundant information. Additional clauses were back subsumed, more than 200,000. The computer time it takes to deduce and retain a clause is not much more than the time it takes to deduce and discard a clause. Can you formulate a strategy that enables a program to avoid the generation of such a huge amount of useless information, useless because of being redundant, as established by being subsumed?
Similarly, at least for OTTER, clauses are discarded if one of their properties yields a value larger than assigned in the input, such as assigned with max_weight or with max_distinct_vars.
What about finding a strategy to quickly predict such occurrences and avoid deducing such clauses?
I have proofs found after five days in real time.
If that time could be reduced to three, what an improvement!
Perhaps for a beginning, if you study the clauses discarded by, say, subsumption during a long experiment and if you view those discarded clauses in relation to the retained item that enabled the discarding, can you identify properties of the retained clause that can be used ahead of time to save most of the time used in discarding redundant information?
Note that I say "save most of the time": recall that employing the set of support strategy costs no time -- yours or the program's.
The 2018 Herbrand Award for distinguished contributions to automated reasoning will be presented to Bruno Buchberger for the invention, implementation, and analysis of the Gröbner-basis method, resulting in the reshaping of symbolic computation towards comprehensive and widely applicable tools.
We welcome all participants of IJCAR 2018 to join the CADE business meeting on Tuesday, July 17th at 4pm. The agenda includes the following topics:
During the past forty years there has been extensive, continuous, and growing interaction between logic and computer science. In many respects, logic provides computer science with both a unifying foundational framework and a tool for modeling. In fact, logic has been called "the calculus of computer science", playing a crucial role in diverse areas such as artificial intelligence, computational complexity, distributed computing, database systems, hardware design, programming languages, and software engineering.
The Federated Logic Conference brings together several international conferences related to mathematical logic and computer science.
You are warmly invited to participate in FLoC 2018. Registration is now open and we remind speakers and participants to book accommodation as soon as possible, as Oxford is popular in the summer.
Conferences
FLoC 2018 brings together nine major international conferences related
to mathematical logic and computer science:
Workshops
In addition to conferences, FLoC 2018 will also feature 70+ workshops (7-8 July, 13 July, and 18-19 July).
Events
Other events are also planned, such as a public lecture or a public debate.
Late registration is open until June 25th, 2018. On site registration will be possible during the conference.
The theme for this year's event is "Intelligent World". The main objective of the conference is to present the latest research and results of scientists related to AI topics. MIWAI 2018 provides opportunities for the delegates to exchange new ideas and establish future collaborations. This year the conference is organized by Mahasarakham University, with association of Vietnam Academy of Science and Technology and University of Science and Technology of Hanoi, Vietnam.
MIWAI aims to promote AI research in both theoretical and applied research addressing real-world applications. We encourage researchers to submit their unpublished papers in the following areas, but not limited to:
Important Dates:
For information about the submission process, see the conference website.
The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices.
Topics of interest include, but are not limited to:
Important Dates:
Information about the submission process are available on the conference web page.
The Luxembourg Logic for AI Summit (LuxLogAI 2018) brings together the 2nd International Joint Conference on Rule and Reasoning (RuleML+RR 2018), the Reasoning Web Summer School (RW 2018), the Global Conference on Artificial Intelligence (GCAI 2018), DecisionCAMP 2018 and the annual meeting of the Deduction Systems group (Deduktionstreffen 2018) of the German Gesellschaft für Informatik (GI).
With its special focus theme on methods and tools for responsible AI, a core objective of LuxLogAI is to present the latest developments and progress made on the crucial question of how to make AI more transparent, responsible and accountable.
First Call For Posters
RuleML+RR 2018 calls for additional short poster papers related to theoretical advances, novel technologies, and innovative applications concerning knowledge representation and reasoning with rules. A Best Poster Award will be given to the best poster presentation.
The full Call for Posters, including submission details, is available here.
Important dates:
First Call For Abstracts
The annual meeting Deduktionstreffen (Deduktionstreffen 2018) is the prime activity of the Interest Group for Deduction Systems (FGDedSys) of the German Informatics Society (Gesellschaft für Informatik). It is a meeting with a familiar, friendly atmosphere, where everyone (not only the German community) interested in deduction can report on their work in an informal setting. The Deduktionstreffen will also host the annual general meeting of the members of FGDedSys. Contributions on all theoretical, experimental and application aspects of deduction are welcome.
Important dates:
First Call For Applications
In order to give PhD students and Postdocs (with limited funding) the opportunity to attend LuxLogAI, the organizers are awarding a number of grants to motivated applicants. In return, successful applicants are asked to assist the local organization team during the conference.
For further details, including how to submit your application, visit this web page.
Important dates:
The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2 and the other theorem provers in the Boyer-Moore family.
Topics include:
Important Dates (extended):
For more information see the workshop website.
CCC is a workshop series bringing together researchers from exact real number computation, computable analysis, effective descriptive set theory, constructive analysis, and related areas. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correct algorithms for computations with real numbers and related analytical data, which are of increasing importance in safety critical applications and scientific computation.
Scope: The workshop specifically invites contributions in the areas of
Deadline: 15 July 2018
Information about the submission process is available on the workshop web page.
The summer school on verification technology, systems & applications focuses on fundamental aspects of verification techniques, their implementation, and their use for concrete applications. It is organized by Inria Nancy, the Max-Planck-Institut für Informatik in Saarbrücken, and the Universities of Liège and of Luxembourg, and will take place at the research center Inria Nancy - Grand Est in Nancy, France, from August 27 to 31, 2018.
The following speakers have agreed to lecture at the school:
Participation to the school is free to anybody holding at least a bachelor degree or equivalent; it includes the lectures, coffee and lunch breaks, and a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending an email to Stephan Merz including
Full details can be found on the school Web page.
There is an increasing need for Software Security and Protection due to the growing sensitivity of user data coupled with the ubiquitous nature of computing systems ranging from tiny embedded devices to powerful data centres.
The International Summer School on Information Security and Protection (ISSISP) highlights this need by bringing internationally renowned speakers from diverse fields in Computer Science such as Software Engineering, Formal Methods, Computer Architecture, Operating Systems, and Programming Languages.
In particular, topics to be covered include vulnerability detection and analysis, software forensics, and information flow control. The summer school caters towards students and professionals from academia, government, and industry. Courses will include both lectures and hands-on sessions.
ISSISP is open to students, academics, and professionals from academia, government, and industry. The number of attendee places is strictly limited. Prospective attendees should submit an expression of interest here. Expressions of interest will continue to be reviewed until the first day of the School (9th July). Please contact this address with any specific questions regarding registration.
More information is available on the web page of the school.
The aim of the summer school is to cover basic and advanced topics in proof theory. The focus of the first edition will be on structural proof theory, ordinal analysis, provability logic, automated theorem proving, and philosophical aspects of proof. Other areas like reverse mathematics, proof mining, and proof complexity will be covered at the co-located workshop, and in follow up summer schools. The intended audience is advanced master students, PhD students, postdocs and experienced researchers in mathematics, computer science and philosophy.
More information is available on the web page of the school.
The Automation of Logic group, led by Dr. Christoph Weidenbach, is looking for a PhD student to work on the formalization, in the Isabelle proof assistant, of the metatheory of automated reasoning.
Researchers in automated reasoning spend a substantial portion of their work time developing logical calculi (e.g., DPLL, resolution, and superposition) and proving metatheorems about them. These proofs are typically carried out with pen and paper, which is error-prone and can be tedious. As part of the IsaFoL (Isabelle Formalization of Logic) project, we are interested in formalizing results concerning existing logical calculi. The motivation is manifold:
The PhD project is about verifying a functional implementation of a superposition prover: a minimalistic version of E, SPASS, or Vampire, based on the superposition calculus, a saturation loop, simplification, and subsumption. The project would be executed in close collaboration with Jasmin Blanchette at Vrije Universiteit Amsterdam and members of the Automation of Logic group in Saarbrücken, including Mathias Fleury, Sophie Tourret, and Uwe Waldmann.
The candidate should ideally have some experience with automated or interactive theorem proving, or with some closely related area of theoretical computer science (e.g., term rewriting). To apply, please send your personal record (including CV, grade transcripts, and contact information for two references) by email to Jennifer Müller.
The Information Security Group carries out research on methods and tools for the analysis and construction of safe and secure systems. This includes methods for specifying systems, developing systems in correctness-preserving ways, and verifying or testing existing systems and infrastructures. Our goal is not only to build and analyze novel systems and security solutions, but also to develop better methods and tools for system engineering and quality assurance activities.
We have an open Ph.D. research position on "Big Data Monitoring". The project's main objective is to develop and implement efficient, parallelized algorithms capable of checking whether a high-volume and high-velocity stream of events comply with given rules. The rules are formulated in an input language that allows users to express temporal and data dependencies between different events in the data feed in a simple and intuitive manner. If any of the rules are violated, a compact output of the data that caused the violation should be produced.
The ideal candidate for this position is an enthusiastic, outstanding researcher with a strong background and interest in one or more of the following areas:
Candidates with a strong theoretical background in related areas are also encouraged to apply. ETH Zürich regulations require PhD candidates to hold a Master's or equivalent degree (e.g. Diplom). The project is funded by the Swiss National Science Foundation and will be supervised by Prof. David Basin and Dr. Dmitriy Traytel.
The Ph.D. student will be a paid employee of ETH Zürich. Salary and employment conditions are attractive. ETH Zürich regulations require doctoral students to hold a Master's or equivalent degree (e.g. Diplom).
Zürich is a diverse and multicultural city, which is consistently rated among the best cities in the world in which to live. We favor the same sort of diversity that defines Zurich's cultural makeup and encourage anyone matching the profile above to apply, regardless of where you are from.
Applications should include a curriculum vitae, a brief description of research interests, transcripts of grades, 2-3 letters of recommendation from teachers or employers, and, if possible, the Master's or Bachelor's thesis and publications. Applications and informal inquiries should be sent to Dmitriy Traytel
ETH Zürich specifically encourages women to apply with a view towards increasing the proportion of female researchers.
We have open Ph.D. research positions in the area of Privacy, Data Protection, and Access Control. We seek to hire one or more doctoral students who will carry out research on the development of novel control and auditing mechanisms that enhance data protection, e.g., by ensuring that data is only used for the purposes it is collected. This will involve developing and prototyping new access control mechanisms as well as using code analysis and machine learning methods to extract and determine "purpose" from code and other system artifacts. In addition and independent of foundational research on these topics, there will be the opportunity to work with our industrial partners to evaluate the developed techniques on realistic large-scale systems.
The ideal candidate for this position is an enthusiastic, outstanding student with a strong background and interest in one or more of the following areas:
Candidates with a strong theoretical background in related areas are also encouraged to apply. ETH Zürich regulations require PhD candidates to hold a Master's or equivalent degree (e.g. Diplom). The Ph.D. student will be a paid employee of ETH Zurich. Salary and employment conditions are very attractive.
Applications should include a curriculum vitae, a brief description of research interests, transcripts of grades, 2-3 letters of recommendation from teachers or employers, and, if possible, the Master's or Bachelor's thesis and publications. Applications and informal inquiries should be sent to Esfandiar Mohammadi.
ETH Zürich specifically encourages women to apply with a view towards increasing the proportion of female researchers.
The position is for 2.5 years, with a possible extension. Closing date for applications: 1 July 2018.
We are looking to hire a motivated Research Associate to join IRIS: Interface Reasoning for Interacting Systems - an exciting new EPSRC-funded Programme Grant led by University College London, Imperial College London, Queen Mary University of London and the London School of Economics. The goal of the IRIS project is to study and devise novel approaches for analysing large systems in a scalable manner via reasoning at the level of inter-component interfaces. The current post at Imperial College London will be jointly supervised by Dr Alastair Donaldson (Department of Computing) and Dr John Wickerson (Department of Electrical and Electronic Engineering, EEE), and will focus on reasoning about software designed to run on many-core architectures and other highly parallel accelerators. There will be a special focus on high-assurance software that needs to leverage many-core technology due to performance constraints, and yet which needs to be highly reliable.
Imperial's Computing and EEE departments are both leading departments in their respective subjects among UK Universities, and have consistently been awarded the highest research rating from the Higher Education Funding Council. The 2014 REF assessment ranked the Department of Computing third (first in the Research Intensity table published by The Times Higher), and the EEE department first for research in the country's EEE sector.
Reasoning about many-core software is challenging for various reasons, including the state-space explosion that arises due to interleaving of concurrent components, the subtle relaxed memory semantics of modern architectures and programming languages, and the difficulty of automated testing in the face of the nondeterminism that arises from both of these concerns. As part of the IRIS project we will focus on making both theoretical and practical advances in reasoning capabilities for many-core software, following various lines of inquiry including (but not limited to):
Duties and responsibilities
The successful candidate will work with the investigators at Imperial to conduct original research in areas relevant to the IRIS project (including for example some of the research areas outlined above), and will collaborate with the investigators and researchers involved in the IRIS project more broadly to amplify the technical depth and potential impact of the work. In addition to frequent research meetings at Imperial, the candidate will attend regular IRIS project meetings to engage with the other academic and industrial partners, and will present work arising from the project at international meetings.
Essential requirements
The breadth of the project allows for flexibility in the profile of applicants, ranging from applicants with backgrounds in formal methods or programming languages theory who are interested in applying fundamental theory to challenging engineering problems, to applicants with a background in system-building who are interested in how to reason about systems. All applicants require the following:
For more information see the job advertisement web page.
Please get in touch with Alastair Donaldson or John Wickerson for informal enquiries.
The chair MAIS at TU Darmstadt, led by Prof. Dr. Heiko Mantel, is offering three positions for Ph.D. candidates and Postdocs in the following areas:
The positions are available immediately and applications will be considered until the positions are taken. For more information and how to apply, see this web page.
The UK Research Institute in Verified Trustworthy Software Systems and the UK's National Cyber Security Centre have provided a PhD studentship to work with Mark Batty at the University of Kent in Canterbury, UK. The position is part of the "Specification and verification of C++ data structure libraries" project.
Details and how to apply on this 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. The position starts in September 2018. Applicants must have, or be about to complete a degree in Computer Science or Mathematics at the BSc or MSc level.
Please do contact Mark Batty if you are interested.
Two postdoctoral research positions are available at Stanford University under Professor Clark Barrett. Applications are being accepted now with a target start date for both positions of Fall 2018. Starting salary is $80,000 per year and includes benefits. Any updates will be posted on this website.
Verification of Neural Networks
The first position will focus on tools and techniques for applying formal verification to deep neural networks. The project aims to extend and apply the highly-successful Reluplex tool. Applications include safety-critical systems such as self-driving cars and drone aircraft.
The ideal applicant must have:
Hardware Verification
The second position will focus on building a new generation of open-source tools for hardware verification and model checking. This person will work closely with the Stanford Agile Hardware Center and the CVC4 SMT Solver team.
The ideal applicant must have:
Stanford University
Stanford University is among the top universities in the world in computer science research. Located in the heart of silicon valley, it is known for an exciting and fast-paced research environment combining exceptional academic talent with abundant opportunities to collaborate with top high-tech companies. The weather is also really nice.
Application details
Questions and applications can be sent to Prof. Clark Barrett. Applicants should include their CV, including a list of publications, together with a brief statement outlining their suitability for the project and the names of at least two references.
This project offers an exciting opportunity to combine theory and practice in the verification of real time systems, based on research questions posed by Siemens Rail Automation UK. We are looking for an ambitious candidate, keen to undertake challenging collaborative research with industrial impact.
More information can be found on the scholarship web page.
A PhD studentship in the area of logic and verification is available at UCL's PPLV group.
Details are available on the scholarship web page under the title "PhD Studentship in Logic and Verification at UCL".
Closing date is 17 July 2018.
Applications are invited for a PhD studentship at University College London, under the supervision of Prof. Alexandra Silva and Dr. Matteo Sammartino.
The start date is flexible. It should be in September 2018 at the latest.
The studentship is funded by the UK Research Institute in Verified Trustworthy Software Systems, and will be carried out within the Programming Principles, Logic and Verification (PPLV) group. The PPLV group offers an exciting research environment, with outstanding connections with cutting-edge industry.
Potential applicants are encouraged to contact Prof. Silva and Dr. Sammartino for further information and expressions of interest. Applications should be made via the UCL evision system.
The department of Computer Science has a new opening for a Research Associate in Verification of Linear Dynamical Systems, working with Professor James Worrell, and funded by an Established Career Fellowship from EPSRC. The overall goal of this proposal is to develop techniques to solve fundamental computational problems arising in the verification of discrete and continuous linear dynamical systems, including Markov chains, linear recurrence sequences, linear while loops, and linear differential equations.
The closing date for applications is 12 noon on Friday 13th July 2018.
More information can be found on the application web page.
Deadline: 31 Jul 2018
At Faculty 3 - Mathematics/Computer Science the following open position is available. The vacancy will be filled - conditional to the release of budgetary funds - as soon as possible:
Professorshipin the discipline
Salary Group W2
Theoretical Computer Science
Reference number: P559/18
as a civil servant, permanent position
The future professor will represent Theoretical Computer Science in research and teaching and should have an outstanding scientific qualification in a relevant area such as Algorithms and Complexity Automata Theory Finite Model Theory Algorithmic Graph Theory.
He/she will teach introductory lectures to undergraduate students as well as specialized courses to graduate students; teaching in the form of student projects is a welcome addition. Commitment and innovativeness in teaching are expected, and so is the willingness for didactical self-improvement and contribution to the internationalization of the University of Bremen.
It is further expected that the future professor contribute to science funding by acquiring third party funds. Cooperation with research institutions associated with the University of Bremen and contributions to the high-profile research area Minds, Media, Machines are highly welcome. Prerequisites for an appointment are a completed university degree in a field relevant to the position, a very good doctoral degree as well as further scientific achievements (equivalent to a habilitation postdoctoral thesis) which may have also been acquired outside of a university, teaching experience at a university, and pedagogical proficiency. Experience in considering the gender perspective in research and teaching is desirable. Non-German speaking candidates are expected to be able to teach in German within two to three years.
The recruitment is based on §18 BremHG.
As a winner of the Total-E-Quality Science Award, the University of Bremen strives to increase the number of female professors and therefore explicitly requests applications from female scientists. Applications from international scientists as well as applications of scientists with a migration background are explicitly welcome. Disabled candidates will be given preference in case of almost identical professional and personal qualifications.
Applications including a cover letter, CV, publication list, copies of degree certificates, should be submitted by July 31st, 2018 to:
Universität Bremenor electronically in a single PDF file.
Fachbereich 3 - Mathematik und Informatik
Fachbereichsverwaltung
Bibliothekstr. 5
28359 Bremen
For inquiries, please contact the dean of Faculty 3 Mathematics/Computer Science, Prof. Dr. Kerstin Schill.
Comprehensive information on all aspects of the hiring process can be obtained here.
Matryoshka is an ambitious research project that aims at developing efficient deduction techniques and integrating them in proof assistants. The project is funded by a European Research Council Starting Grant from March 2017 to February 2022. It is co-located between Vrije Universiteit Amsterdam (Jasmin Blanchette) in the Netherlands and Loria, Inria Nancy - Grand Est (Stephan Merz, Pascal Fontaine) in France.
Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. To make interactive verification more cost-effective, we propose to deliver powerful automation to users of proof assistants by fusing and extending two lines of research: automatic and interactive theorem proving. To reach end users, these new provers will be integrated in proof assistants, including Coq, Isabelle/HOL, and the TLA+ Proof System. The subject of the position advertised here is this last aspect, i.e. integrating automatic deduction techniques in the TLA+ Proof System, the proof assistant for Lamport's Temporal Logic of Actions. To provide more automation for the non-temporal aspects of TLA+, which make up perhaps 90% or more of typical proofs, the PhD student will design efficient translations of set theory to higher-order logic. In order to filter the few useful lemmas out of the large TLA+ context, we suggest the design and use of a system of soft types.
We are looking for one outstanding candidate for a Ph.D. due to start before the end of 2018. Candidates should ideally have some experience with automatic or interactive theorem proving and be at ease with both theory and engineering. The student will work in a motivating environment in close collaboration with the Matryoshka and TLA teams. Please contact as soon as possible Jasmin Blanchette, Pascal Fontaine and Stephan Merz for more information.
To know more:
Applications are invited for a Research Associate to carry out research on application of formal verification technology to safety assurance of autonomous robots. This position will be funded by the EPSRC for three years in the context of the recently awarded CyPhyAssure project.
You will assist in the development of a computerised platform for arguing the safety of autonomous robots by application of multi-model based assurance cases. We will build this platform within the Isabelle/HOL proof assistant, and utilise the Structured Assurance Case Metamodel (SACM). The platform, as conceived, will support formal modelling of individual modular components of a robot and its environment, the combination of these models to describe the overall system's behaviour, the description of formal requirements of the overall system, and decomposition and apportionment of these requirements to the constituent models.
You will liaise with academic and the industrial partners and participate in the writing of research papers. You will have a PhD in the area of formal methods, experience in modelling and formal refinement, and understanding of hybrid and/or probabilistic systems. You will have substantial experience in the application of the Isabelle/HOL theorem prover. Experience in the areas of assurance cases, safety processes, and robotics are all highly desirable.
For more information on this position, please visit this web page.
Funding research into scalable testing and verification.
Facebook is pleased to invite university faculty to respond to a call for research proposals on Testing and Verification (TAV). This is Phase One of Facebook's funding initiative to support research in Testing and Verification.
We're particularly interested in:
This is my first newsletter without Philipp as a co-editor. I wish to thank him for his collaboration till now and in the future as secretary of the AAR.
* * *
Now I would like to talk a little about one of the projects I am involved with.
During the last week of June, I attended the Matryoshka workshop. It was packed with interesting talks, mostly about first- and higher-order automatic and interactive theorem proving. One thing I found particularly interesting was the discussion session that concluded the workshop. At some point in this discussion, Martin Riener said something in the spirit of:
I would be very interested if someone could give a list of things that are difficult to do when going from first- to higher-order automated reasoning.Alexander Steen (a PhD student working on the higher-order automated prover Leo III) immediately replied that he could and started doing so. The rest of the discussion was centered on this issue of when and where things get ugly in higher-order, what that means and how it has been overcome (or not) in different tools.
Among this list, two points particularly struck home:
In short, as someone that is stumbling upon these issues today, I look forward to this discussion turning into a paper that could be used as a guide, warning people about the pitfalls in the road to higher-order automated reasoning.