- Matryoshka: https://matryoshka-project.github.io
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. The situation has improved with the integration of first-order automatic theorem provers—superposition provers and SMT (satisfiability modulo theories) solvers—through middleware such as Sledgehammer for Isabelle/HOL and HOLyHammer for HOL Light and HOL4; but this research has now reached the point of diminishing returns. Only so much can be done when viewing automatic provers as black boxes.
To make interactive verification more cost-effective, we propose to deliver very high levels of automation to users of proof assistants by fusing and extending two lines of research: automatic and interactive theorem proving. This is our grand challenge. Our starting point is that first-order (FO) automatic provers are the best tools available for performing most of the logical work. Our approach will be to enrich superposition and SMT with higher-order (HO) reasoning in a careful manner, to preserve their desirable properties. We will design proof rules and strategies, guided by representative benchmarks from interactive verification.
With higher-order superposition and higher-order SMT in place, we will develop highly automatic provers building on modern superposition provers and SMT solvers, following a novel stratified architecture. To reach end users, these new provers will be integrated in proof assistants and will be available as backends to more specialized verification tools. The users of proof assistants and similar tools stand to experience substantial productivity gains: From 2010 to 2016, the success rate of automatic provers on interactive proof obligations from a representative benchmark suite called Judgment Day has risen from 47% to 77%; with this project, we aim at 90%–95% proof automation.
- Lean Forward: https://lean-forward.github.io
Proof assistants (also called interactive theorem provers) are increasingly used in academia and industry to verify the correctness of hardware, software, and protocols. However, despite the trustworthiness guarantees they offer, most mathematicians find them too laborious to use.
The goal of the Lean Forward project is to collaborate with number theorists to formally prove theorems about research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles. The theorems will be selected together with our collaborators to guide the development of formal libraries and verified tools.
Our vehicle will be Lean, a disruptive proof assistant developed at Microsoft Research and Carnegie Mellon University. Lean draws on decades of experience in interactive and automatic theorem provers (e.g., Coq, Isabelle/HOL, and Z3). Its logic is very expressive, and emphasis is placed on strong proof automation. The system is easy to extend via metaprograms that rely on the same logical language that is used to express specifications and proofs.
- Automata Transforming Streams
DASDiP: Design and Analysis of Secure Distributed Protocols
Distributed protocols, e.g. consensus, leader election, atomic commit, are the building blocks of all network applications, from everyday file-sharing systems to complex grid applications for solving grand challenges like protein folding, financial modeling etc. They have been widely studied and well understood. Traditionally, the studies mostly regard computation-intensive tasks and the main concerns are correctness, fault-tolerance and efficiency.
Since the growth of internet and mobile communication infrastructures, the scope of network applications has extended towards service-oriented tasks: e-commerce, electronic voting, auctions, content-exchange systems, mobile ad-hoc applications etc. Here new concerns, like guaranteeing privacy, fairness, or authenticity, play an essential role. These issues are generated by possible malicious behaviour in the network and they do not replace, but come in addition to the old correctness, fault-tolerance and efficiency problems.
This project aims at a systematic study of both theoretical and practical aspects of designing and analyzing such secure distributed protocols, taking as starting point the well-developed theory and practice of distributed protocols. We wish to redefine existing theoretical failure models to accommodate malicious behaviour and thus obtain new attack models. These models will then be used as setting for deriving theoretical impossibility and complexity results that will clarify the borders of what is achievable by security protocols. Furthermore, these models will be also used as framework for formally analyzing existing security protocols and designing new ones.
Formal Verification of Epidemic Protocols
As the world's computing systems become more numerous and highly connected, new behaviors appear. When large numbers of programs interact in a connected environment, various phenomena occur which are not explicable in terms of the programming or behavior of any single agent. It is necessary to understand these phenomena in order to keep the overall systems both secure and efficient.
A peer-to-peer network relies on the computing power and bandwidth of its participants rather than on a relatively low number of servers. Peer-to-peer networks typically use ad hoc connections. The group of Maarten van Steen works on peer-to-peer technology to build large-scale distributed systems.
In this project we will concentrate on epidemic protocols, which multicast data similar to the way a disease spreads. A participating peer can randomly select another peer to exchange information. Epidemic protocols are generally robust, but they tend to be message intensive. A key challenge is to design epidemic protocols that maintain their robustness without sending as many messages.
These protocols will be formally specified and verified, using both model checking and theorem proving. The aims are to detect possible bugs, to obtain information about the performance of such protocols (e.g. what is the chance that a piece of information is shared with all processes within a given time), and to gain further confidence in these protocols. Last but not least, the aim is to develop a systematic approach for analyzing epidemic protocols.
HOT: Higher-Order Termination
The project HOT is concerned with the question `Does my program eventually halt?'. We study this question in the setting of higher-order term rewriting. The aim of HOT is to develop, extend, and improve methods to prove termination of higher-order rewriting systems. In addition, we aim to develop a higher-order termination tool.
In higher-order rewriting, one needs to deal with both substitution, as in the lambda calculus, and algebraic combinatorics, as in first-order term rewriting. Termination methods for higher-order rewriting are therefore expected to combine ideas of both typed lambda calculi (such as candidates of reducibility) and first-order term rewriting (such as path orderings and dependency pairs).
We focus on two termination methods. The first is the higher-order recursive path ordering. A main issue here is an extension to more complex typing systems as used in proof assistants. The second is the method of dependency pairs. A main issue here is the extension to the higher-order case. In both cases we aim at a presentation that is user-friendly and suitable for implementation in a termination tool for higher-order rewriting. Moreover, we aim at an integrated approach that is suitable both in the case that beta-reduction is explicit and in the case that beta-reduction is implicit, and one works with beta-equivalence classes.
The development of termination methods for higher-order rewriting is essential for the project of adding rewriting to type theory, which will significantly increase the power of proof assistants such as Coq.
The Art of the State: Distributed Model Checking
Model checking is an important automated approach to verify properties of distributed systems and protocols. First the state space is generated of the (software or hardware) system under consideration, or of a formal specification of this system. Requirements of the system, formulated in some temporal logic, can then be checked against the state space.
The main bottleneck is that the state space of a distributed system grows exponentially with its number of distributed components. Therefore currently a lot of effort is spent on developing methods for distributed model checking, where the state space is stored on a cluster of computers. So far these effort were mainly by researchers from the model checking community, that has only limited experience in large-scale distributed computing.
Distributed model checking has the potential to become an important application for the DAS-4 cluster. It requires large amounts of memory as well as intensive communication between nodes. Moreover, it is directly applicable to study the correctness of real-life software and hardware systems. Notably, it can be used in the design of protocols for DAS-4 itself.
This research focuses on developing algorithms, methods and efficient implementations for distributed model checking.
A Term Rewriting Perspective on Program Termination
With the increasing complexity of computer systems, program verification has become central in computer science. A program is considered `correct' if it `terminates' and produces a valid output with respect to a given specification. Even control programs, such as Windows, that are not supposed to be terminating, consist to more than 99% of terminating function calls. Termination of these functions (e.g. rendering the desktop) is important since they must return to the main control loop.
We aim to integrate automated termination analysis in the software development cycle to increase software correctness and quality. Termination is a central aspect of program verification, and in contrast to other aspects, termination analysis does not require additional work from the developer (like writing a formal specification). Therefore, it is especially suitable for automation.
We analyse program termination via a translation to term rewriting systems (TRSs). The TRSs then act as unifying formalism for all programming languages. For TRSs, over the past ten years an impressive arsenal of termination methods and automated termination provers has been developed. Via the translation, these powerful tools become applicable for proving program termination.
Besides this general focus, we aim at the development of novel termination methods, tailor-made for program termination. In particular we plan to investigate `modular termination proofs' and `local termination'. Both are hardly developed in state-of-the-art TRS termination analysis. Modular termination proofs are of importance, since the size of real-life programs requires modular reasoning, where parts of the program are analysed separately. Then the proofs for the parts are combined into a termination proof for the whole program. Moreover, in program verification one is interested in termination of a program started on a valid input. This is a local termination problem, in contrast to global termination of all expressions, which includes also undesired (e.g. unreachable, ill-formed) expressions.