Salto: Static Analyses for Trustworthy OCaml

This site is under construction. Stay tuned!

The expressive type system of OCaml brings strong static safety guarantees by ensuring data is used in a consistent way by a program. The Salto project aims at providing OCaml programs with additional guarantees, by answering questions such as:

• Can a program raise an exception?
• Can arithmetic operations overflow?
• Are all the array accesses performed within the array bounds?
• Can a program break some user-defined invariant or assertion?
• Which data might be modified by a program?

Those questions are beyond the scope of the OCaml type system, but are within reach of abstract interpretation-based static analyses.

The goal of the Salto project is to define sound static analyses that help answer the above questions as automatically as possible. The analysis will help a programmer have better confidence in her programs, by bringing increased safety and security guarantees.

News

• November 2022: official start of the project

Contributors

• Thomas Jensen, senior researcher at Inria, team Épicure
• Thomas Genet, full professor at Université Rennes 1, team Épicure
• Pierre Lermusiaux, research engineer at Inria, team Épicure
• Benoît Montagu (lead), researcher at Inria, team Épicure

Funding

The Salto project is a partnership between Nomadic Labs and Inria, and is funded by the Tezos Foundation.