LARA is a research group led by Viktor Kunčak. We develop precise automated reasoning techniques: tools, algorithms and languages. The goal of these techniques to help construction of verified computer systems. We develop several open-source projects, notably:

• Stainless is a tool for constructing formally verified software that is guaranteed to meet specifications for all inputs (see the ASPLOS tutorial). The primary input format to Stainless is a subset of Scala. furthermore, Bolts shows several case studies carried out using Stainless.
• LISA is a project to develop proof assistant based on first-order logic and set theory.
• Scallion is a Scala library for provably correct parsing and pretty printing.

For more information on software, see the organization’s GitHub.

Research and Development

Viktor Kunčak	Mario Bucev	Dragana Milovancevic
Simon Guilloud	Samuel Chassot	Sankalp Gambhir

Support

System Manager Fabien Salvi

Administrative Assistant Sylvie Buchard

More information

See the EPFL page of LARA as well as the video channel for the Formal Verification course.