• You are, of course, free to suggest your own project and discuss it with us.

• To ensure that everyone knows what they should do and we know what you are actually doing, you will submit a short (about 1-2 pages) proposal for the project you decide on. This should include e.g. deliverables in terms of code or algorithms, a plan of attack for your problem, more background references, examples, etc. Deadline is 10 April.

• Projects from our list of suggestions will be assigned on a first-come-first-served basis, so don't wait until the last minute to have a look. If you picked a project, send an announcement over Moodle so that everyone knows.

• You can keep working in the same groups or regroup or work individually, as you wish (but please let us know if you change something).

The name after each project title indicate the contact person for the project.

1. Extend Leon with Higher-Order Functions [Etienne] (Nicolas V.)
2. Extend Leon with Parametric Polymorphism [Etienne]
3. Templates in Function Postconditions [Filip Konecny] (Ravi)
4. Inference of Regular Tree Constraints [Regis]
5. Proof Carrying Code [Eva] (Bruno and Romain)
6. Add Global Variables to Leon extension [Etienne]
7. Translate Leon programs into Horn clauses [Regis Blanc and Hossein Hojjat]
8. Bounded Universal Quantifiers [Regis]
9. Comparison of Leon, Why3, and Dafny [Eva] (Denys)
10. BAPA Logic in Leon [Philippe Suter and Viktor]
11. Verifying Security Properties [Hossein Hojjat]
12. Strings and Lists in Leon [Regis] (Dinis and Vera)
13. SMT-Based Synthesis [Pierre-Emmanuel]
14. Improve the Web IDE for Leon [Etienne]
15. Leon front ends [Eva] (Igor)
16. Quick and Dirty Scala Verifier [Regis] (CANCELLED)
17. Proving Correctness of Scala Data Structures [Regis] (Nicolas S. and Johann)
18. Automated Discovery of Algebraic Specifications [Philippe and Viktor]
19. Approximating nonlinear functions [Eva]
20. Scala as a Proof Language [Pierre-Emmanuel]
21. Online Machine Learning in InSynth [Tihomir and Ivan] (Tong)

This extension will allow Leon to support higher-order functions such as map and fold. We can therefore prove interesting lemmas about them, such as:

(map(f) andThen map(g))(x) == map(f compose g)(x)

and do reasoning at a higher level of abstraction.

Ideally, the project will support the

(x => E) 

notation for anonymous functions, functions as parameters, representation of function parameters as uninterpreted functions/maps, and, during reasoning, replacement of function parameters with concrete anonymous or non-anonymous functions.

Add a simple form of type parameters to Leon. This will enable defining generic lists and similarly reusable algebraic data types.

This requires enhancing the front end, the formula trees, and connection to Z3.

For some theoretical implications, please see:

• ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/KrsGGT-TACAS-07.pdf

but soundness for proofs should be achievable by mostly considering unknown type parameters to denote (countably) infinite sets.

Allow postconditions to use unknown parameters and develop techniques to synthesize them.

This can be used in conjunction with specifying running times of functions. Instead of saying that the running time of a method is 10*x+2, we can write, e.g. 'a*x+'b.

See, for example, this paper:

• http://www-step.stanford.edu/papers/sas04.html

Design and implement an inference engine that will compute regular tree grammars that describe subsets of algebraic data types that functions manipulate.

For example, for a recursive function that removes certain types of nodes from an abstract syntax tree, the result will be a grammar describing a subset of trees that it returns (omitting the removed node types).

The idea of proof carrying code is that, just as we compile code, we can also compile Hoare logic proofs for this code to assembly level. The advantage of doing that is that we can go much further than Java bytecode verifiers. We can have lower-level code (like binaries) and prove higher-level properties (like assertions or postconditions), if we ship binaries with additional annotations.

The proof carrying code model is that a high-level language is verified, and then compiled together with the information about the result of the verification. When the client downloads the code, a low-level code verifier examines the binary and the associated proof. Without trusting whoever produced the binary or the proof, it checks whether the binary satisfies the shipped properties. The properties are required to be detailed enough, so that checking this is fast. In that way, we do not need to trust the high-level language compiler or verifier, as long as the low-level code verifier is correct. A broken verifier or compiler will generate binaries that will be refused by low-level verifier.

In this project, you will explore building a basic form of proof carrying code for Leon. You can choose either to work with the existing compiler to bytecodes in Leon, or compile to a concrete or abstract assembly language.

For more information, please see:

• http://www.cs.berkeley.edu/~necula/pcc.html

Leon has an extension that supports imperative programs, but it currently only supports local mutable variables. Add support for global variables declared in an object. Translate them by introducing them as function parameters and results.

To help with modularity of the transformed programs, introduce a non-recursive algebraic data type storing all global variables.

Global variables should support any of the existing types, such as integers, algebraic data types, sets, maps.

Time permitting, consider allowing mutable fields in classes and transforming them into global maps.

Currently Leon mostly requires precise postconditions to verify recursive functions. The goal of this project is to improve the automation in Leon. Leon will therefore automatically infer some of the postconditions using static analysis.

The approach explored here is to develop a translation from Leon into Horn clauses and then run one of the tools that work on Horn clauses.

One such tool is Eldarica. See Eldarica page and this paper,

Another tool is HSF.

Leon uses only quantifier-free constraints so far, which allows it to predictably find counterexamples. Bounded universal quantifiers can in some cases be expanded into recursive functions, but can be handled more efficiently in many cases. To improve the efficiency of reasoning and the convenience, the goal of this project is to add bounded universal quantifiers to Leon.

One example approach is to allow

 e.forAll 
 e.exists

where e is of type Set[A].

This will be useful for especially for stating properties of maps and arrays. Existing Leon benchmarks provide a good example where several Boolean functions can be expressed using quantifiers.

Compare three related verification tools:

• Leon, developed in LARA group
• Dafny, developed by Rustan Leino, http://rise4fun.com/Dafny/
• Why3, http://why3.lri.fr/

Translate benchmarks from one tool to another when this is natural, and understand reasons in verification technology that contribute to differences in the success for verification.

Optionally, you may choose to transfer some of the important advantages of Why3 or Dafny to Leon.

Contact: http://www.irisa.fr/celtique/cornilleau/

Extend Leon's support for sets using size constraints.

Build on the works such as this one:

• Deciding Boolean Algebra with Presburger Arithmetic
• Sets with Cardinality Constraints in Satisfiability Modulo Theories

Background: Spi-calculus is a formalism designed to represent cryptographic protocols. In a spi-calculus model there is a set of processes running in parallel. The processes can send and receive messages through channels. There is an automatic verification tool called ProVerif for verification of models in spi-calculus. The input language of ProVerif is based on spi-calculus. ProVerif translates the spi-calculus description into a set of Horn clauses for internal representation. It can also directly analyze Horn clause description of security protocols.

Problem description: There are some predicate abstraction tools (HSF, Eldarica) that can handle Horn clauses. The goal of this project is to verify some of the security benchmarks using the the predicate engines. Second (optional), we would like to find some completeness grantees for security protocols. This means to find some basic classes of protocols for which we ensure that the predicate abstraction engine can finally decide if the program is correct or not.

Extend Leon to support theory of strings and list concatentations.

Introduce a built in notion of Lists or Sequences into Leon, with a nice and clean set of operations on them. Compare to sequence operations in Python.

Study the existential word problem and context unification problems and examine verification conditions that arise in practice.

See these papers:

• Word Equations With Two Variables
• Bounded Second-Order Unification is NP-Complete
• Satisfiability of Word Equations with Constants Is in PSPACE
• Wojciech Plandowski. An efficient algorithm for solving word equations. In Jon M. Kleinberg, editor, STOC, pages 467–476. ACM, 2006

Implement synthesis based on capturing quantifier instantiations.

To solve the problem

choose(x => P(x,a))

generate a statement:

FORALL x. !P(x,a)

Prove that the statement is unsatisfiable and capture the instantiated quantifiers. Use the instaitiations to construct the program that realizes the specification P(x,a).

Add features such as sharing and exchanging programs, continuous error reporting, counterexample visualisation, specification debugging. Consider comparison to: http://alloy.mit.edu/alloy/

This project is essential to user interfaces and therefore to usability of verification tools.

Interesting aspects involve detecting changes in the program and verifying only those parts that need to be re-verified, and enable continuous verification, much like current continuous compilation.

Add a front-end for Leon for one of the following weakly languages

• PHP subset, possibly leveraging http://lara.epfl.ch/w/phantm, consult with Etienne Kneuss
• Python subset
• LISP subset as in ACL2, see http://www.cs.utexas.edu/~moore/acl2/

This will greatly increase the reach of Leon and the set of benchmarks, as well as help understand the impact of different programming models on the ability to verify properties, and help us compare different tools.

Adding an interface to an untyped language requires developing technique for Leon to handle untyped programs. See, for example:

• http://docs.scala-lang.org/sips/pending/type-dynamic.html

Thus, a possible starting point may be addition of Type Dynamic into Leon.

Extend the Leon verifier by defining a robust interface that approximates any Scala code with some Leon code.

Use this approximation feature to apply Leon to substantial Scala code base.

The approximation need not be complete or faithful to Scala, but simply a best effort.

Understand some data structures from Scala library, or their simpler counterparts.

Model them in Leon by translating them manually into functional code, manually where needed. Prove their correctness or report experience in finding bugs and specifications.

Automatically generate candidate specifications of functions (for example, associativity of a binary operation, monotonicity, etc.). Then test candidate hypothesis and introduce them as Leon lemmas.

Consult Philippe Suter and Viktor Kuncak

Evaluating nonlinear functions can be expensive, especially if done repeatedly, as functions like sin, cos, log, etc. are evaluated correct up to the last digit. However, such precision is not always necessary, e.g. if the rest of the computation is imprecise anyway, or only a small number of decimal digits is needed to make a decision. This project will explore ways of automatically approximating such nonlinear functions with guaranteed error bounds by using linear approximations. The identification of realistic examples and evaluation of the precision and efficiency of the method is part of the project. This project complements approaches that determine suitable combinations of approximations to achieve an overall precision, but require the user to provide the initial approximations manually, e.g.:
Z.A. Zhu, S. Misailovic, J.A. Kelner, M. Rinard, Randomized accuracy-aware program transformations for efficient approximate computations. POPL 2012

Explore the effectiveness of Scala as a language for writing down formal proofs, such as the proofs used in Isabelle or Coq systems.

• http://www.cl.cam.ac.uk/research/hvg/Isabelle/

Consult Giuliano Losa, Pierre-Emmanuel

Machine learning can be done online, while InSynth is used. Here, a student will implement an engine that will learn directly from the InSynth user and his/her code. This includes collecting and reasoning about recently used snippets and similar statistics, plus, data we can derive from the user's code.

Again, if there is any subset of this project that interests you, we encourage you to contact us.