Overview
L3Cover (L-three-cover) is a framework library for building program verifiers for low-level languages (such as assembly language and machine language). Our goal is to provide a common basis which helps the developers build their program verifier easily.
For low-level languages, program verifiers have been hard to develop.
This is mainly because such languages are very specific to the underlying architectures (i.e. CPUs).
Each time we build a verifier for a low-level language, we first have to model its underlying architecture and describe the semantics of the language.
These steps require substantial effort, because we then have to assure that the description is correct before we use it.
Also porting a verifier from one architecture to another generally requires a great amount of work.
Existing verifiers often do not consider portability and incorporate architecture-specific features even into the core of their verification logics.
Then we will have to re-implement a large part of the system when we try to port them.
In L3Cover model, one verifier is splitted into a few independent parts: (1) common language ADL, (2) program translator and (3) verification logic. These parts are implemented independently, so they can easily be replaced from one to another. Thus this independence improves code reusability, and reduces the implementation burden present in the conventional systems.