Forgot your password?
New user?
Verisoft Repository Summary
Document Actions
Verisoft Repository Summary
In the Verisoft project, the pervasive verification of four exemplary computer systems, three of which come from industrial sector, is attempted. The layers, which are considered, range from the gate-level hardware over system software to communicating and distributed applications.
The Verisoft repository allows to concurrently develop the many individual results that contribute to the overall verification result and manage them in a tractable manner.
In the repository, the artefacts developed by the project partners are being collected as `modules' and related to each other via `dependencies'. Modules include documentations, specifications, implementations, proofs, and tools for development and verification. Modules may come in different `versions' and `specializations'. `Versions' correspond to branches, as done in regular software development. `Specializations' tailor a module to a given dependency set, e.g., there may be different specializations of a proof depending on the version of the verification tool being used.
In the end, the repository must be self-contained: the set of modules for a given computer system under verification must allow to (i) build an executable implementation of that system and (ii) prove the top-level correctness of that system.
Currently, substantial parts of the Verisoft theories and systems have been imported into the Verisoft repository and the repoistory is being used for further development. In the future, when the verification is complete, snapshots of selected parts of the repository will be made publicly available.
