HLL – High Level Language

A Language for Formal Verification of Safety-critical Systems

About HLL – High Level Language

HLL is a formal high level language developed in 2008 by Prover Technology in collaboration with RATP. It includes predicate logic but also supports important common programming features such as arrays and numbers.

It is straightforward to translate programs written in C, Ada etc. to HLL, but also programs written in various vendor-specific programming languages. Properties about these system models can also be expressed in HLL.

HLL is the input language of our tool Prover Certifier. By translating your system to HLL and defining your safety requirements in HLL, you can use Prover Certifier to get safety evidence for the system. Formal verification ensures that your system fulfills the requirements in 100% of the possible scenarios, a coverage that can never be achieved by testing.

Since 2008, HLL has been used by several of our clients to obtain formal safety proofs.

An old version of HLL is published here. HLL is continuously improved and extended to support more kinds of systems and to make it possible to express more kinds of properties