  Static verification of a program source code correctness is an important
element of software reliability. Formal verification of software programs
involves proving that a program satisfies a formal specification of its
behavior. Many languages use both static and dynamic type checking. With such
approach, the static type checker verifies everything possible at compile time,
and dynamic checks the remaining. The current state of the Jolie programming
language includes a dynamic type system. Consequently, it allows avoidable
run-time errors. A static type system for the language has been formally
defined on paper but lacks an implementation yet. In this paper, we describe a
prototype of Jolie Static Type Checker (JSTC), which employs a technique based
on a SMT solver. We describe the theory behind and the implementation, and the
process of static analysis.

Software Engineering;Programming Languages