In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language.
Our system is based on a dependently-typed language and an algorithmic type checking procedure
which ensures total correctness. We rely on SMT solvers to automate the
verification process and to provide us with useful counterexamples when considered
properties are invalid. We then enable verification in the presence of high-level Scala language features
by encoding them into the dependently-typed language.

We introduce an SMT-backed counterexample finding procedure which can also prove that no
counterexample exists. The procedure incrementally unfolds function calls and applications in order
to progressively explore the space of counterexamples. We present increasingly expressive fragments of our
dependently-typed language and establish soundness and completeness properties of the procedure for each fragment.
We then describe an extension which introduces support
for quantifier reasoning. We discuss syntactic and semantic conditions under which the
extended procedure can produce valid counterexamples in the presence of universal quantification.

We present a bidirectional type checking algorithm for our dependent type system.
The algorithm relies on our counterexample finding procedure to discharge verification conditions
which enables predictable and effective type checking.
The type system features a unified treatment of both recursive and corecursive definitions,
and further admits mutual recursion between type and function definitions.
We establish normalization through a sized types approach.
We define a logical relation which associates a set of reducible values to each type,
and then show soundness of verification by proving that evaluation of a type checked expression terminates with a reducible value.

We further discuss a set of transformations which encode high-level Scala constructs into
our dependently-typed language. These transformations allow our verification system to
support object-oriented features such as traits and classes with multiple inheritance,
as well as abstract and concrete methods with overriding. We further present a measure
inference transformation which enables automated termination checking in our system.
In addition to encoding language features, we discuss how Scala can be
augmented with natural specification constructs and annotations that empower verification.

Finally, we describe the system implementation and discuss certain practical considerations.
We show that the resulting system is effective by evaluating it on a set of benchmarks
and case studies comprising over 15K lines of Scala code. These benchmarks
showcase both the breadth and flexibility of the system.