PVS Examples

PVS 6.0

Compression function of Timed-Triggered Ethernet: dump
Model of an asynchronous fault-tolerant systems that uses mid-value select: dump

PVS 3.1

Modeling and Verification of a secure protocol supporting the group-management services of Enclaves. The developments are based on PVS theories developed by Harald Rueß and Jon Millen. dump (gzipped).
Priority Ceiling Protocol. dump (gzipped)
Embedding CSP's trace model in PVS with application to authentication protocols. This is joint work with Steve Schneider.
- CSP trace model alone: dump (gzipped)
- CSP model and applications to authentication: dump (gzipped)
Roots, square roots and various lemmas about exponentiation. dump (gzipped)
Real analysis: Continuous functions, derivatives, limits, etc. dump (gzipped)
Some extensions of the finite set library: powersets, cartesian product, pigeon-hole principle. dump (gzipped)
GCD, prime numbers, prime factorization, etc.: dump (gzipped)
RSA (The PVS dump includes part of the previous one.) dump (gzipped)
Well-Ordering Principle and Zorn's lemma: dump (gzipped)

PVS 2.4 and 2.3

The theories below may not be compatible with PVS2.2 (some use the new syntax and judgements). The proofs have been done using the old decision procedures but, with a few exceptions, everything also works with the new ones. When available, the 2.4 versions contain minor modifications.

Modeling and verification of the Enclaves group-management protocol. 2.4 dump (gzipped) or 2.3 dump, (gzipped)
Priority Ceiling Protocol. 2.4 dump (gzipped) or 2.3 dump (gzipped)
Embedding CSP's trace model in PVS with application to authentication protocols. This is joint work with Steve Schneider.
- CSP trace model alone: 2.4 dump (gzipped), or 2.3 dump (gzipped)
- CSP model and applications to authentication: 2.4 dump (gzipped), or 2.3 dump (gzipped)
Roots, square roots and various lemmas about exponentiation. 2.4 dump (gzipped) or 2.3 dump (gzipped)
Real analysis: Continuous functions, derivatives, limits, etc. 2.4 dump (gzipped) or 2.3 dump (gzipped)
Some extensions of the finite set library: powersets, cartesian product, pigeon-hole principle. 2.4 dump (gzipped) or 2.3 dump (gzipped)
A little number theory: GCD, prime numbers, prime factorization, etc.: 2.4 dump (gzipped) or 2.3 dump (gzipped).
RSA (The PVS dump includes part of the previous one.) 2.4 dump (gzipped) or 2.3 dump (gzipped).
Definition of fixed points for monotonic functions of type [set[T] -> set[T]]: 2.4 dump (gzipped) or 2.3 dump (gzipped).
Well-Ordering Principle and Zorn's lemma: 2.4 dump (gzipped) or 2.3 dump (gzipped).

PVS 2.2

Most of the things below are (gzipped) dump files produced with PVS version 2.414 or older.
The proofs should work with newer versions but some adjustments may be necessary.

Well-Ordering Principle and Zorn's lemma: dump file or compressed dump file
Definition of fixed points for monotonic functions of type [set[T] -> set[T]]: dump file or compressed dump file
A little number theory: gcd, prime numbers, prime factorization, etc.: dump file or compressed dump file
RSA (The PVS dump includes part of the previous one.) dump file or compressed dump file
Illustration of inductive definitions using CTL modal operators: dump file or compressed dump file
A little real analysis: Continuous functions, derivatives, limits, etc. dump file or compressed dump file
Roots, square roots and various lemmas about exponentiation. dump file or compressed dump file