VeriAMOS ANR Project
Julia Lawal, Gilles Muller, Nicolas Palix and Xavier Rival (PI)
Summary
The VeriAMOS project brings together experts in static analysis, operating systems, and programming language design, at Inria, Sorbonne University, and the University of Grenoble, to propose a new approach to producing verified OS services, based on the use of Domain-Specific Languages (DSLs) and automated static analysis. A DSL is a programming language that is designed around abstractions that are specific to a family of programs. A DSL lets programmers implement a specific class of algorithms at a higher level than a conventional programming language, and provides a compilation chain to produce target code. By limiting the language expressiveness, a DSL also constrains programmers, and prevents the misuse of language features. The key insight behind the VeriAMOS project is that by raising the level of abstraction and restricting the program design space, DSLs can make it possible to fully automate strong verifications on implementations of real OS services.