Skip to content

b-hilprecht/verified-distributed-log

Repository files navigation

P verification of distributed log

Blog

Find out about the project here.

Setup

Install the P programming language.

Run

p compile 
p check

# run on a single seed
p compile && p check --fail-on-maxsteps --max-steps 100000 --seed 3

# run for a specific time
p compile && p check --fail-on-maxsteps --max-steps 100000 --seed 1 --timeout 800 --explore

Run for all seeds and find a failing one

# on fish:
for seed in (seq 0 1000)
    echo "Running with seed: $seed"
    if not p check --fail-on-maxsteps --max-steps 100000 --seed $seed
        echo "Command failed with seed: $seed"
        break
    end
end

About

Formal verification of a distributed logging protocol with P

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published