Course projects

Here is a list of possible subjects for the course projects. If you have other ideas, feel free to discuss them with lecturers.

- Projects can be done in pairs.

Send us an email by 1st October, to indicate which project you will do. - Each project should contain some code (OCaml or Prolog or Coq code unless another programming language is justified)
- You will present your project orally, possibly as early as the week of November, in 30 minutes.

The objective is for us to understand what you did; an effective way of achieving this is to use slides, although the slides themselves are not what will be evaluated.

On the other hand, a demo is expected. - You are requested to submit your code, significantly commented. You are free to improve your project after that submission.
- You should also send, by email, a document describing your project (pdf is preferred).

The document should give us all the keys to understand what you did/are doing, connecting the comments in your code to the "general picture".

The length of the document does not matter as long as the above objective is reached, but we reckon it would be difficult for us to understand what you did if the document is shorter than 2 or 3 pages. On the other hand, we cannot guarantee that pages beyond page 10 will be read thoroughly.

Below you will find proposals for projects.

Since the timeline for a project is rather short, and you will not start practicals on Prolog and Coq before 13/10 and 20/10, respectively, the proposals below all involve algorithms for Automated Deduction, and their potential implementations in OCaml. Other ideas are welcome, but if you want to do a project involving rather Prolog or Coq, we can discuss how to rearrange your practicals from Day 1 so as to start your project as early as possible.

- Making a SAT-solver produce proofs of UNSAT
The goal here is to improve the SAT-solver that you started writing in TD1 with

- better data-structures than lists
- the backjump rule instead of the backtrack rule, producing the backjump clause with a conflict analysis
- learning the backjump clauses as if they were input clauses
- derive from the above a proof of unsatisfiability, in case the answer is unsat.

- The theory of uninterpreted functions
This mathematical theory only says that, given a function symbol

`f`

of unknown interpretation,`f(x1,...,xn)=f(y1,...,yn)`

if`x1=y1`

...`xn=yn`

. It is well-known that satisfiability problems for that theory can be solved by an algorithm called congruence closure. Here, the project will explore how such problems can be solved in a more general context, called MCSAT, which organises an interaction between solvers for different theories. - Intuitionistic logic
This is the logic that rejects the idea of reasoning by contradiction, and which is widely used in Interactive Theorem Proving. However, there exist algorithms that can prove theorem of intuitionistic logic automatically, if they are in the propositional fragment. The best-performing algorithm for doing this uses a very unconventional approach, described in a LPAR'2015 paper. Two projects can be done regarding that algorithm:

First, compare it with earlier work, which it seems connected to: analyse the differences, and what could be the reason for a fundamental speed-up in the new approach.

Second, try to integrate that algorithm to a rather systematic approach for satisfiability-solving that is based on model constructing algorithms. - Forgetting what is learnt
Most algorithms for automated reasoning have a learning mechanism that allows them to learn new facts from old facts. The database of learnt facts is very useful, because what is learnt at some point can be re-used, to speed-up the reasoning mechanisms in the future. However, the database has a tendency to grow large, and despite clever techniques to scan it efficiently, its size increase eventually becomes problematic as too much CPU time is spent searching the database, and going over useless facts, or facts that are redundant with each other. State-of-the-art provers implement clever heuristics for pruning the database every now and then, removing the most useless facts, so as to keep the database size under control. The project consists in surveying these techniques, and implement them in a prover that does not yet have this feature.

- Linear Integer Arithmetic (LIA)
This theory has a sibling, Linear Rational Arithmetic (LRA), that is easier to automate. Universal statements in LRA can be proved or disproved by the use of (SAT-solving and) a simplex algorithm. For example, trying to prove that for all rationals x and y, either (2y < -2x + 1) or (2y > 2x + 1) or (2x > 1) is going to fail, because an obvious counter-example is x=y=1/2. However this would be provable if x and y were integers. Making sure that the counter-examples are actually integers, and not simply rationals, requires some extra work to be done on top of the simplex algorithm. Dejan Jovanovic invented for linear arithmetic a method that is rather different from the simplex algorithm, and we have implemented it for LRA. On the basis of his paper for LIA, the project would explore whether the adaptation from LRA to LIA is easier to do in his approach than in the simplex approach, and, if so, it would involve adapting our LRA implementation into an LIA implementation.

- Approaches for verifying neural nets
Formally verifying a neural net is asking the question of whether there is an input that can give a particular output (for instance if the neural net is used as a classifier, the question is whether there exists an input that gets mis-classified). We concentrate here on neural nets whose activation function is a max with 0. Technically, answering such a question for a given neural net requires solving linear arithmetic problem with case analyses for each max. Nothing theoretically difficult, but in practice the number of cases makes the question really difficult to answer. At CAV'2017, Guy Katz presented a clever technique to explore this huge search space efficiently. The question here is whether Dejan Jovanovic's model-constructing approach (or our own variant) can be used to express or capture this clever technique, or propose something similarly efficient.

- Bitvectors
Vectors of bits are what our computers manipulate at the lowest level. Establishing that hardware or software actually operate in the way we intend them to, often requires proving properties about bitvectors. The theory of bit vectors is not theoretically difficult, but usually, the properties we want to prove involve so many bits that proving them automatically is very long. At SMT'2017, Dejan Jovanovic and I proposed a novel approach for automatically proving these properties, trying to avoid going down to the bit-level as much as possible. Part of this proposal involves BDD (Binary Decision Diagrams). The project would involve turning these vague ideas into an actual implementation (warning: this is not just implementing something completely specified; it also involves quite a bit of design).