Lars Helander

About Lars Helander

Senior Developer at Prover Technology.

Floating Point Model Checking

We at Prover are very happy to announce the release of version 4.0 of our model checker Prover SL CE (PSL). The most interesting new feature is support for IEEE 754 floating point calculations, so I will dedicate this technical blog post to floats with a concrete example of a floating point system which we [...]

By |2019-11-04T10:55:48+01:00November 4th, 2019|Formal Verification|

Using HLL to solve Sudoku puzzles

In a recent post we celebrated the 10th anniversary of the declarative, formal language HLL. The language is used extensively in the railway signaling domain for the formal verification of interlocking logic and CBTC subsystems (such as zone controllers). In this more technical post we will familiarize the reader further with HLL, by formalizing the famous [...]

By |2019-07-11T09:08:21+01:00July 10th, 2019|Formal Methods, HLL – High Level Language|

HLL formal language celebrates 10 years

The formal language HLL (High Level Language) has emerged in recent years as a quite popular language for formal verification of safety-critical systems, especially in the railway signaling domain. This year marks the 10th anniversary of its conception. The history of HLL The language has its roots in the proof engine technologies developed by Prover in the 1980s (Stålmarck's [...]

By |2019-07-03T09:25:55+01:00June 30th, 2018|Formal Methods, HLL – High Level Language|