Methods

Galois employs an innovative approach to specify, model, verify, and monitor critical software based on sound theoretical, scientific, and technological research. The methods address the problems of developing high assurance systems through an iterative approach that applies mathematical formalisms across all phases of development.

Four major artifacts evolve as each iteration refines the system specification and implementation: A natural language specification captures customer requirements while a formal model is used simultaneously to model and verify the correct understanding and behavior of the target system; an executable model then embodies design decisions and is verifiably consistent with the formal model; and an executable system emerges that is verifiable through automated test generation from the executable model.

Galois has a unique advantage in this process using the formal methods embodied in Haskell, a purely functional language that supports all formal phases of development. Functional programming is more like mathematics than programming. For the developer, it represents a significant step up in abstraction and capability from languages such as C++ and Java, enabling much higher coding efficiency, in addition to formalisms that greatly ease verification.

All programming languages suffer from a semantic gap: once the developer has worked out how to solve a problem, they have to translate that solution into the concrete syntax of the programming language. In traditional languages, such as C, C++, and Java, the semantic gap is large, and the translation is error-prone and time-consuming. In comparison, functional languages, such as Haskell, ML, and Caml, allow developers to express their ideas relatively directly. The rest of the translation is handled by the compiler, and is governed by strict, mathematical principles. By removing the ad-hoc, error-prone, time-consuming translation step, functional languages enable developers to produce correct code in a fraction of the time.