-
Notifications
You must be signed in to change notification settings - Fork 0
Stainless
drganam edited this page Oct 3, 2023
·
1 revision
Stainless is a program verifier for Scala programs.
Scala programs.
Stainless supports programs written in an expressive subset of Scala, called PureScala. For remarks on the supported Scala features see: https://epfl-lara.github.io/stainless/purescala.html.
Stainless supports verifying:
- Assertions which should hold at the place where they are stated, but are checked statically
- Postconditions using ensuring function: assertions for return values of functions
- Preconditions using require function: assertions on function parameters
- Loop invariants: inductive assertions that hold in each loop iteration after the while condition check passes
- Algebraic data type class invariants: assertions on immutable parameters of constructors (which remain true for all constructed values)
- Automatic checks done for the absence of runtime failures: completeness of pattern matching, division by zero, array bounds checks, map domain checks
Stainless ensures that the input program belongs to a subset of Scala. This subset syntactically prevents:
- the creation of null values or unininitalized local variables or fields (therefore, dereferencing fields in Stainless programs cannot lead to null dereference error)
- explicitly throwing an exception.
Stainless performs non-trivial termination checks for its functions and supports specifying decreasing measure functions.
Stainless can also prove equivalence of recursive programs using automated functional induction.
The system is split into two main components:
- Inox, a backend verification condition solver based on model finding procedures. Inox relies on function unfolding to perform both counterexample and proof search. Inox relies on SMT solvers to solve the constraints it generates.
- Stainless, a Scala frontend that supports contract-checking and termination proving. Stainless encodes and type checks Scala programs and relies on Inox to handle verification conditions.
- External SMT Solvers: Z3, CVC4
- Repository: https://github.com/epfl-lara/stainless
- Website: https://stainless.epfl.ch/
- Warm-up Examples: https://epfl-lara.github.io/stainless/tutorial.html
- Bolts (Stainless Verified Scala): https://github.com/epfl-lara/bolts
- Benchmarks: https://github.com/epfl-lara/stainless/tree/main/frontends/benchmarks
- ASPLOS'22 Tutorial: https://epfl-lara.github.io/asplos2022tutorial/
- EPFL's Formal Verification Course: https://tube.switch.ch/channels/f2d4e01d
- Jad Hamza, Nicolas Voirol, and Viktor Kunčak. 2019. System FR: Formalized Foundations for the Stainless Verifier. Proc. ACM Program. Lang OOPSLA (November 2019). https://doi.org/10.1145/3360592
- Nicolas Charles Yves Voirol. 2019. Verified Functional Programming. (2019), 229. https://doi.org/10.5075/epfl-thesis-9479
- Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak. 2015. Counter-Example Complete Verification for Higher-Order Functions. In Scala Symposium. Association for Computing Machinery, New York, NY, USA.