This repository contains the implementation of the DBM (Differential Bound Matrix) algorithm and its associated data structures in Rust. The DBM algorithm is widely used for time constraint management in real-time system. To enhance robustness, these implementations have been formally verified using Creusot.

We have verified the following properties for each DBM operation:

• Changes on these operations
• Preservation of canonicity in these operations

• up
• down
• free
• reset

• shift
• and
• etc...

To use this repository, you will need to have Creusot installed on your machine. If you haven't installed it yet, refer to the README.md in the official repository. Make sure to install version 0.1.1 of Creusot, either by installing from source ref v0.1.1 or by downloading the source from the release page.

Next, clone this repository and then move into to the dbm-creusot directory:

$ git clone https://github.com/ruth561/VerifiedDBM.git
$ cd dbm-creusot

Now, all necessary procedures are completed! To perform proofs for each DBM operation, please execute the following command:

$ cargo creusot why3 ide

All implementations for DBM operations are contained within the src/ directory. We have implemented each DBM operation in separate files. For example, the down operation is implemented in the src/down.rs file.

Although we have implemented these features in a simplified manner to ensure successful verification, more accurate implementations are needed for practical use. Future implementations should include:

• Distinguishing between (<, m) and (<=, m)
• $k\text{-Normalization}$
• $k,\mathcal{G}\text{-Normalization}$