Skip to content

Commit

Permalink
move install instructions to docs and update link in 2pc verification…
Browse files Browse the repository at this point in the history
… tutorial.
  • Loading branch information
FedericoAureliano committed Nov 28, 2024
1 parent c26fc9b commit 446859b
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 1 deletion.
File renamed without changes.
2 changes: 1 addition & 1 deletion Docs/docs/tutorial/advanced/twophasecommitverification.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Introduction to Formal Verification in P

This tutorial describes the formal verification features of P through an example. We assume that the reader has P installed along with the verification dependencies (i,e., UCLID5 and Z3). Installation instructions are available [here](https://github.com/p-org/P/blob/experimental/pverifier/INSTALL.md).
This tutorial describes the formal verification features of P through an example. We assume that the reader has P installed along with the verification dependencies (i,e., UCLID5 and Z3). Installation instructions are available [here](https://github.com/p-org/P/blob/master/Docs/docs/advanced/install-verification-backend.md).

When using P for formal verification, our goal is to show that no execution of any test driver will violate a specification. To do this, we will rely on proofs by induction---more on that later. This backend is different from P's explicit state model checker, which you are accustomed to using. These differences can influence the modeling decisions you make.

Expand Down

0 comments on commit 446859b

Please sign in to comment.