sopher

README

Sopher

Runtime verification of Probabilistic time-sensitive hypercontracts defined using hyper hoare logic in Go.

To show contracts can be extended to hyperproperties using hyper hoare logic reasoning over sets of executions. With FISSC as motivation we will show how to express hyperproperties in contracts to show how hyperproperties can help us capture violations of contracts for programs which can undergo bit flips.

Quickstart

go run ./cmd/main.go
# Or
make run

go build ./cmd/main.go
# Or
make build

go test ./...
# Or
make test

go fmt ./...
# Or
make fmt