Here are some project suggestions, but you are of course welcome to suggest your own.

• Lazy Annotation [Duc]
• Integration with the Scala compiler [Nada]
• Integration with LLVM [Jonas]
• Integration of polyhedral library into Scala
• Verification case studies using Leon [Marc & Diggory]
• Implementation of Cooper's algorithm [Cristian]
• Synthesis of all solutions
• BigInts as a Main Data Type [Diana]
• Integration of arbitrary precision into Scala [Damien and Roman]
• Testing of floating-point codes for precision

By a “student verifier” we mean the verifier you obtain at the end of Spring break, after completing the inference of conjunctions of predicates.

Implement lazy annotation on top of your verifier. For more details, please see:
Kenneth L. McMillan: Lazy Annotation for Program Testing and Verification. CAV 2010: 104-118.

Extend the official Scala compiler by building a plugin that acts as interface between Scala and the student's verifier. This project will replace the current verifier front-end of your running project with the official Scala front-end, allowing any Scala program written in the subset in consideration to be checked using the verifier. The plugin will consist of traversing Scala ASTs provided by the compiler and generate the appropriate CFGs.

Analogously to the previous case, establish integration of your verifier with the http://llvm.org/ compiler infrastructure.

Reuse and incorporate into the Scala compiler an analyzer such as the Parma polyhedra library (PPL): http://bugseng.com/products/ppl, which already has a Java interface.
Alternatively, explore the combination of PPL with the student verifier.

Working with Regis Blanc, explore the use of Leon in verification case studies of Scala programs that belong to a particular subset.

Implement a version of Cooper's algorithm for quantifier elimination in Scala. For more details, please see the Calculus of Computation textbook.

Starting from the implementation of Comfusy (see STTT 2012 journal paper version), make it create procedures that enumerate *all* solutions and not just return one.

Design analysis that estimates the ranges of variables, with the goal of supporting arbitrary-precision integers. The goal would be to use the analysis to transform a program in the language such as the one we use in the project, into one that executes efficiently and is guaranteed to give the same result. Namely, to have correct semantics, the language should use BigInt implementation, which can be slow. The goal is to compute that certain unbounded integers remain within smaller ranges and emit code that corresponds to operations on bounded types such as Int, Byte, Boolean. The code should also contain appropriate conversion operators and ensure that the overall code gives the same result as if it used BigInts.

Scala currently does not have an arbitrary numerical precision data type that supports transcendental functions (e.g. sin, cos, etc.). The algorithms and implementations in other languages do exist, however. The idea of this project is to identify a suitable library and to integrate it into Scala in an easy to use way (for instance like here). One possible such library is the ARPREC package, but there are several more.

Most testing techniques are targeted towards detecting run-time errors or for checking user-defined assertions, but precision of floating-point computations is usually not taken into account. The idea of this project is to investigate the usefulness of a SmartFloat data type that estimates floating-point roundoff errors for generating test inputs. The test inputs should uncover paths through the program that are less precise than needed. We suggest to conduct this project as a case study on some scientific computing code(s) and to use interval subdivision to narrow down interesting input ranges and obtain precise estimates. The SmartFloat data type can also give feedback on which inputs contribute significantly to output errors; this information can be used for an adaptive interval subdivision procedure.