How To Install pvs-sbcl on Fedora 36
In this tutorial we learn how to install pvs-sbcl in Fedora 36. pvs-sbcl is Interactive theorem prover from SRI
Introduction
In this tutorial we learn how to install pvs-sbcl on Fedora 36.
What is pvs-sbcl
PVS is a verification system integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. This build of PVS must be invoked as “pvs-sbcl”, both to distinguish it from builds with other Common Lisp engines, and to distinguish it from /usr/sbin/pvs in the lvm2 package.
We can use yum or dnf to install pvs-sbcl on Fedora 36. In this tutorial we discuss both methods but you only need to choose one of method to install pvs-sbcl.
Install pvs-sbcl on Fedora 36 Using dnf
Update yum database with dnf using the following command.
sudo dnf makecache --refresh
After updating yum database, We can install pvs-sbcl using dnf by running the following command:
sudo dnf -y install pvs-sbcl
Install pvs-sbcl on Fedora 36 Using yum
Update yum database with yum using the following command.
sudo yum makecache --refresh
After updating yum database, We can install pvs-sbcl using yum by running the following command:
sudo yum -y install pvs-sbcl
How To Uninstall pvs-sbcl on Fedora 36
To uninstall only the pvs-sbcl package we can use the following command:
sudo dnf remove pvs-sbcl
pvs-sbcl Package Contents on Fedora 36
/usr/bin/proveit
/usr/bin/provethem
/usr/bin/pvs-sbcl
/usr/bin/pvsio
/usr/lib/.build-id
/usr/lib/.build-id/13
/usr/lib/.build-id/13/725df466c9623a86de2b6d84fc7b37472820f9
/usr/lib/.build-id/69
/usr/lib/.build-id/69/d64617e248dcb4d7ee8fd841d1d8b3278179eb
/usr/lib/.build-id/b1
/usr/lib/.build-id/b1/82af1531b1a25d3ee555ddb121b7b7c061652b
/usr/lib/.build-id/d4
/usr/lib/.build-id/d4/48eb7a844a542111a80e7255c29933e223d807
/usr/lib64/pvs
/usr/lib64/pvs/bin
/usr/lib64/pvs/bin/ix86_64-Linux
/usr/lib64/pvs/bin/ix86_64-Linux/b64
/usr/lib64/pvs/bin/ix86_64-Linux/runtime
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/bdd-sbcl.fasl
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/bdd-sbcl.lisp
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/dfa-foreign-sbcl.fasl
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/dfa-foreign-sbcl.lisp
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/mu-sbcl.fasl
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/mu-sbcl.lisp
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/mu.so
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/pvs-sbclisp
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/sbcl
/usr/lib64/pvs/bin/ix86_64-Linux/runtime/ws1s.so
/usr/lib64/pvs/bin/ix86_64-Linux/yices2
/usr/lib64/pvs/bin/pvs-platform
/usr/lib64/pvs/bin/tar-b64-mail
/usr/lib64/pvs/bin/tarmail
/usr/lib64/pvs/bin/untarmail
/usr/lib64/pvs/doc
/usr/lib64/pvs/doc/release-notes
/usr/lib64/pvs/doc/release-notes/pvs-release-notes.info
/usr/lib64/pvs/emacs
/usr/lib64/pvs/emacs/README
/usr/lib64/pvs/emacs/configured-for-x
/usr/lib64/pvs/emacs/go-pvs.el
/usr/lib64/pvs/emacs/ilisp
/usr/lib64/pvs/emacs/ilisp/ACKNOWLEDGMENTS
/usr/lib64/pvs/emacs/ilisp/COPYING
/usr/lib64/pvs/emacs/ilisp/HISTORY
/usr/lib64/pvs/emacs/ilisp/comint-ipc.el
/usr/lib64/pvs/emacs/ilisp/comint-ipc.elc
/usr/lib64/pvs/emacs/ilisp/completer.el
/usr/lib64/pvs/emacs/ilisp/completer.elc
/usr/lib64/pvs/emacs/ilisp/docs
/usr/lib64/pvs/emacs/ilisp/docs/ilisp.texi
/usr/lib64/pvs/emacs/ilisp/ilcompat.el
/usr/lib64/pvs/emacs/ilisp/ilcompat.elc
/usr/lib64/pvs/emacs/ilisp/ilfsf18.el
/usr/lib64/pvs/emacs/ilisp/ilfsf19.el
/usr/lib64/pvs/emacs/ilisp/ilfsf20.el
/usr/lib64/pvs/emacs/ilisp/ilfsf20.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-acl.el
/usr/lib64/pvs/emacs/ilisp/ilisp-acl.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-aut.el
/usr/lib64/pvs/emacs/ilisp/ilisp-aut.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-bat.el
/usr/lib64/pvs/emacs/ilisp/ilisp-bat.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-chs.el
/usr/lib64/pvs/emacs/ilisp/ilisp-chs.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-cl-easy-menu.el
/usr/lib64/pvs/emacs/ilisp/ilisp-cl-easy-menu.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-cl.el
/usr/lib64/pvs/emacs/ilisp/ilisp-cl.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-cmp.el
/usr/lib64/pvs/emacs/ilisp/ilisp-cmp.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-cmt.el
/usr/lib64/pvs/emacs/ilisp/ilisp-cmt.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-cmu.el
/usr/lib64/pvs/emacs/ilisp/ilisp-cmu.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-def.el
/usr/lib64/pvs/emacs/ilisp/ilisp-def.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-dia.el
/usr/lib64/pvs/emacs/ilisp/ilisp-dia.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-doc.el
/usr/lib64/pvs/emacs/ilisp/ilisp-doc.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-ext.el
/usr/lib64/pvs/emacs/ilisp/ilisp-ext.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-hi.el
/usr/lib64/pvs/emacs/ilisp/ilisp-hi.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-hnd.el
/usr/lib64/pvs/emacs/ilisp/ilisp-hnd.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-imenu.el
/usr/lib64/pvs/emacs/ilisp/ilisp-imenu.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-ind.el
/usr/lib64/pvs/emacs/ilisp/ilisp-ind.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-inp.el
/usr/lib64/pvs/emacs/ilisp/ilisp-inp.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-key.el
/usr/lib64/pvs/emacs/ilisp/ilisp-key.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-kil.el
/usr/lib64/pvs/emacs/ilisp/ilisp-kil.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-low.el
/usr/lib64/pvs/emacs/ilisp/ilisp-low.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-menu.el
/usr/lib64/pvs/emacs/ilisp/ilisp-mnb.el
/usr/lib64/pvs/emacs/ilisp/ilisp-mnb.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-mod.el
/usr/lib64/pvs/emacs/ilisp/ilisp-mod.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-mov.el
/usr/lib64/pvs/emacs/ilisp/ilisp-mov.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-out.el
/usr/lib64/pvs/emacs/ilisp/ilisp-out.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-prc.el
/usr/lib64/pvs/emacs/ilisp/ilisp-prc.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-prn.el
/usr/lib64/pvs/emacs/ilisp/ilisp-prn.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-rng.el
/usr/lib64/pvs/emacs/ilisp/ilisp-rng.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-sbcl.el
/usr/lib64/pvs/emacs/ilisp/ilisp-sbcl.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-snd.el
/usr/lib64/pvs/emacs/ilisp/ilisp-snd.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-src.el
/usr/lib64/pvs/emacs/ilisp/ilisp-src.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-sym.el
/usr/lib64/pvs/emacs/ilisp/ilisp-sym.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-utl.el
/usr/lib64/pvs/emacs/ilisp/ilisp-utl.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-val.el
/usr/lib64/pvs/emacs/ilisp/ilisp-val.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-xfr.el
/usr/lib64/pvs/emacs/ilisp/ilisp-xfr.elc
/usr/lib64/pvs/emacs/ilisp/ilisp-xls.el
/usr/lib64/pvs/emacs/ilisp/ilisp-xls.elc
/usr/lib64/pvs/emacs/ilisp/ilisp.el
/usr/lib64/pvs/emacs/ilisp/ilisp.elc
/usr/lib64/pvs/emacs/ilisp/illuc19.el
/usr/lib64/pvs/emacs/ilisp/ilxemacs.el
/usr/lib64/pvs/emacs/manip-debug-utils.el
/usr/lib64/pvs/emacs/manip-debug-utils.elc
/usr/lib64/pvs/emacs/newcomment.el
/usr/lib64/pvs/emacs/newcomment.elc
/usr/lib64/pvs/emacs/prooflite.el
/usr/lib64/pvs/emacs/prooflite.elc
/usr/lib64/pvs/emacs/pvs-abbreviations.el
/usr/lib64/pvs/emacs/pvs-abbreviations.elc
/usr/lib64/pvs/emacs/pvs-browser.el
/usr/lib64/pvs/emacs/pvs-browser.elc
/usr/lib64/pvs/emacs/pvs-byte-compile.el
/usr/lib64/pvs/emacs/pvs-byte-compile.elc
/usr/lib64/pvs/emacs/pvs-cmds.el
/usr/lib64/pvs/emacs/pvs-cmds.elc
/usr/lib64/pvs/emacs/pvs-eval.el
/usr/lib64/pvs/emacs/pvs-eval.elc
/usr/lib64/pvs/emacs/pvs-file-list.el
/usr/lib64/pvs/emacs/pvs-file-list.elc
/usr/lib64/pvs/emacs/pvs-ilisp.el
/usr/lib64/pvs/emacs/pvs-ilisp.elc
/usr/lib64/pvs/emacs/pvs-load.el
/usr/lib64/pvs/emacs/pvs-load.elc
/usr/lib64/pvs/emacs/pvs-ltx.el
/usr/lib64/pvs/emacs/pvs-ltx.elc
/usr/lib64/pvs/emacs/pvs-macros.el
/usr/lib64/pvs/emacs/pvs-macros.elc
/usr/lib64/pvs/emacs/pvs-menu.el
/usr/lib64/pvs/emacs/pvs-menu.elc
/usr/lib64/pvs/emacs/pvs-mode.el
/usr/lib64/pvs/emacs/pvs-mode.elc
/usr/lib64/pvs/emacs/pvs-prelude-files-and-regions.el
/usr/lib64/pvs/emacs/pvs-prelude-files-and-regions.elc
/usr/lib64/pvs/emacs/pvs-print.el
/usr/lib64/pvs/emacs/pvs-print.elc
/usr/lib64/pvs/emacs/pvs-proofstate.el
/usr/lib64/pvs/emacs/pvs-proofstate.elc
/usr/lib64/pvs/emacs/pvs-prover-helps.el
/usr/lib64/pvs/emacs/pvs-prover-helps.elc
/usr/lib64/pvs/emacs/pvs-prover-manip.el
/usr/lib64/pvs/emacs/pvs-prover-manip.elc
/usr/lib64/pvs/emacs/pvs-prover.el
/usr/lib64/pvs/emacs/pvs-prover.elc
/usr/lib64/pvs/emacs/pvs-pvsio.el
/usr/lib64/pvs/emacs/pvs-pvsio.elc
/usr/lib64/pvs/emacs/pvs-set-prelude-info.el
/usr/lib64/pvs/emacs/pvs-set-prelude-info.elc
/usr/lib64/pvs/emacs/pvs-tcl.el
/usr/lib64/pvs/emacs/pvs-tcl.elc
/usr/lib64/pvs/emacs/pvs-utils.el
/usr/lib64/pvs/emacs/pvs-utils.elc
/usr/lib64/pvs/emacs/pvs-view.el
/usr/lib64/pvs/emacs/pvs-view.elc
/usr/lib64/pvs/emacs/pvs.xpm
/usr/lib64/pvs/emacs/pvslogo.gif
/usr/lib64/pvs/emacs/tcl.el
/usr/lib64/pvs/emacs/tcl.elc
/usr/lib64/pvs/lib
/usr/lib64/pvs/lib/bitvectors
/usr/lib64/pvs/lib/bitvectors/BitvectorMultiplication.prf
/usr/lib64/pvs/lib/bitvectors/BitvectorMultiplication.pvs
/usr/lib64/pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.prf
/usr/lib64/pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.pvs
/usr/lib64/pvs/lib/bitvectors/BitvectorOneComplementDivision.prf
/usr/lib64/pvs/lib/bitvectors/BitvectorOneComplementDivision.pvs
/usr/lib64/pvs/lib/bitvectors/BitvectorTwoComplementDivision.prf
/usr/lib64/pvs/lib/bitvectors/BitvectorTwoComplementDivision.pvs
/usr/lib64/pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.prf
/usr/lib64/pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.pvs
/usr/lib64/pvs/lib/bitvectors/BitvectorUtil.prf
/usr/lib64/pvs/lib/bitvectors/BitvectorUtil.pvs
/usr/lib64/pvs/lib/bitvectors/DivisionUtil.prf
/usr/lib64/pvs/lib/bitvectors/DivisionUtil.pvs
/usr/lib64/pvs/lib/bitvectors/bv_adder.prf
/usr/lib64/pvs/lib/bitvectors/bv_adder.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_caret.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_caret.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_caret_concat_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_caret_concat_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_caret_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_caret_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_concat.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_concat.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_extend.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_extend.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_int_caret.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_int_caret.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_int_concat.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_int_concat.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_int_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_int_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_minus_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_minus_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_nat.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_nat.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_nat_caret_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_nat_caret_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_nat_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_nat_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arith_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_arith_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_arithmetic.prf
/usr/lib64/pvs/lib/bitvectors/bv_arithmetic.pvs
/usr/lib64/pvs/lib/bitvectors/bv_bitwise_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_bitwise_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_caret_bitwise.prf
/usr/lib64/pvs/lib/bitvectors/bv_caret_bitwise.pvs
/usr/lib64/pvs/lib/bitvectors/bv_caret_bitwise_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_caret_bitwise_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_caret_concat.prf
/usr/lib64/pvs/lib/bitvectors/bv_caret_concat.pvs
/usr/lib64/pvs/lib/bitvectors/bv_caret_concat_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_caret_concat_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_caret_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_caret_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_concat.prf
/usr/lib64/pvs/lib/bitvectors/bv_concat.pvs
/usr/lib64/pvs/lib/bitvectors/bv_concat_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_concat_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_constants.prf
/usr/lib64/pvs/lib/bitvectors/bv_constants.pvs
/usr/lib64/pvs/lib/bitvectors/bv_core.pvs
/usr/lib64/pvs/lib/bitvectors/bv_extend.prf
/usr/lib64/pvs/lib/bitvectors/bv_extend.pvs
/usr/lib64/pvs/lib/bitvectors/bv_fract.prf
/usr/lib64/pvs/lib/bitvectors/bv_fract.pvs
/usr/lib64/pvs/lib/bitvectors/bv_int.prf
/usr/lib64/pvs/lib/bitvectors/bv_int.pvs
/usr/lib64/pvs/lib/bitvectors/bv_mult_div_rem.prf
/usr/lib64/pvs/lib/bitvectors/bv_mult_div_rem.pvs
/usr/lib64/pvs/lib/bitvectors/bv_nat_rules.prf
/usr/lib64/pvs/lib/bitvectors/bv_nat_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_notes.pvs
/usr/lib64/pvs/lib/bitvectors/bv_overflow.prf
/usr/lib64/pvs/lib/bitvectors/bv_overflow.pvs
/usr/lib64/pvs/lib/bitvectors/bv_rotate.prf
/usr/lib64/pvs/lib/bitvectors/bv_rotate.pvs
/usr/lib64/pvs/lib/bitvectors/bv_rules.pvs
/usr/lib64/pvs/lib/bitvectors/bv_shift.prf
/usr/lib64/pvs/lib/bitvectors/bv_shift.pvs
/usr/lib64/pvs/lib/bitvectors/bv_sum.prf
/usr/lib64/pvs/lib/bitvectors/bv_sum.pvs
/usr/lib64/pvs/lib/bitvectors/div.prf
/usr/lib64/pvs/lib/bitvectors/div.pvs
/usr/lib64/pvs/lib/bitvectors/mod_rules.prf
/usr/lib64/pvs/lib/bitvectors/mod_rules.pvs
/usr/lib64/pvs/lib/bitvectors/sums.prf
/usr/lib64/pvs/lib/bitvectors/sums.pvs
/usr/lib64/pvs/lib/bitvectors/top.pvs
/usr/lib64/pvs/lib/character_adt.pvs
/usr/lib64/pvs/lib/finite_sets
/usr/lib64/pvs/lib/finite_sets/card_tricks.prf
/usr/lib64/pvs/lib/finite_sets/card_tricks.pvs
/usr/lib64/pvs/lib/finite_sets/finite_cross.prf
/usr/lib64/pvs/lib/finite_sets/finite_cross.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_below.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_below.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_card_eq.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_card_eq.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_eq.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_eq.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_inductions.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_inductions.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_int.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_int.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_minmax.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_minmax.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_minmax_props.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_minmax_props.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_nat.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_nat.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_pred.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_pred.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_product.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_product.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_product_real.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_product_real.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_subtype_props.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_subtype_props.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_sum.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_sum.pvs
/usr/lib64/pvs/lib/finite_sets/finite_sets_sum_real.prf
/usr/lib64/pvs/lib/finite_sets/finite_sets_sum_real.pvs
/usr/lib64/pvs/lib/finite_sets/fs_constructors.prf
/usr/lib64/pvs/lib/finite_sets/fs_constructors.pvs
/usr/lib64/pvs/lib/finite_sets/func_composition.prf
/usr/lib64/pvs/lib/finite_sets/func_composition.pvs
/usr/lib64/pvs/lib/finite_sets/prelude_aux.prf
/usr/lib64/pvs/lib/finite_sets/prelude_aux.pvs
/usr/lib64/pvs/lib/finite_sets/top.prf
/usr/lib64/pvs/lib/finite_sets/top.pvs
/usr/lib64/pvs/lib/lift_adt.pvs
/usr/lib64/pvs/lib/list_adt.pvs
/usr/lib64/pvs/lib/ordstruct_adt.pvs
/usr/lib64/pvs/lib/orphaned-proofs.prf
/usr/lib64/pvs/lib/prelude.prf
/usr/lib64/pvs/lib/prelude.pvs
/usr/lib64/pvs/lib/pvs-gui.json
/usr/lib64/pvs/lib/pvs-language.help
/usr/lib64/pvs/lib/pvs-prover.help
/usr/lib64/pvs/lib/pvs-style.css
/usr/lib64/pvs/lib/pvs-unicode.help
/usr/lib64/pvs/lib/pvs.bnf
/usr/lib64/pvs/lib/pvs.grammar
/usr/lib64/pvs/lib/pvs.help
/usr/lib64/pvs/lib/pvs.json
/usr/lib64/pvs/lib/pvs.rnc
/usr/lib64/pvs/lib/pvsio_prelude.prf
/usr/lib64/pvs/lib/pvsio_prelude.pvs
/usr/lib64/pvs/lib/union_adt.pvs
/usr/lib64/pvs/pvs-tex.sub
/usr/lib64/pvs/wish
/usr/lib64/pvs/wish/gray.xbm
/usr/lib64/pvs/wish/pvs-support.tcl
/usr/lib64/pvs/wish/sequent.xbm
/usr/share/applications/pvs-sbcl.desktop
/usr/share/doc/pvs-sbcl
/usr/share/doc/pvs-sbcl/Examples
/usr/share/doc/pvs-sbcl/Examples/AgExample
/usr/share/doc/pvs-sbcl/Examples/AgExample/AgExample.dmp
/usr/share/doc/pvs-sbcl/Examples/AgExample/AgSpec.txt
/usr/share/doc/pvs-sbcl/Examples/AgExample/FA_Element.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FA_Language.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FA_axioms.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/FA_axioms.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FA_lemmas.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FA_semantic.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/FA_semantic.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_Language.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_axioms.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_axioms.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_conversions.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_conversions.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_lemmas.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_lemmas.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_semantic.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/FODL_semantic.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/RTC.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/SRI-report.pdf
/usr/share/doc/pvs-sbcl/Examples/AgExample/SpecActions.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/SpecActions.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/SpecPredicates.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/SpecPredicates.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/SpecProperties.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/SpecProperties.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/ag-pp.lisp
/usr/share/doc/pvs-sbcl/Examples/AgExample/dom-finitos.txt
/usr/share/doc/pvs-sbcl/Examples/AgExample/list_max.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/list_max.pvs
/usr/share/doc/pvs-sbcl/Examples/AgExample/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/AgExample/run.el
/usr/share/doc/pvs-sbcl/Examples/AgExample/validate.el
/usr/share/doc/pvs-sbcl/Examples/AgExample/wf_FODL_Language.prf
/usr/share/doc/pvs-sbcl/Examples/AgExample/wf_FODL_Language.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/README
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/arbiter.dump
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/arbiter.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/arbiter.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Arbiter/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/README
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/blackjack.dump
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/blackjack.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/blackjack.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Blackjack/transition.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/README
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/components.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/detect110.dump
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/detect110.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/detect110.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/quantifier_rules.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/quantifier_rules.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/signal.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Detect110/time.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/README
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/fir_filter5.dump
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/fir_filter5.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/fir_filter5.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/signal.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/sum.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/sum.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Fir_filter5/time.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/README
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/new_pipe.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/new_pipe.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/pipe.dump
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/signal.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Pipeline/time.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/README
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/README
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/singlepulser.dump
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/singlepulser.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Singlepulser/singlepulser.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/README
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/hard2.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/hard2.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/microrom_rewrite.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/microrom_rewrite.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/soft.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/tamarack.dump
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/trace_equiv.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/trace_equiv.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/traces.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/traces.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/verification.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/verification.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/verification_rewrites.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/verification_rewrites.pvs
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/wordth.prf
/usr/share/doc/pvs-sbcl/Examples/HWVbookchap/Tamarack/wordth.pvs
/usr/share/doc/pvs-sbcl/Examples/README
/usr/share/doc/pvs-sbcl/Examples/ackerman.pvs
/usr/share/doc/pvs-sbcl/Examples/byzantine
/usr/share/doc/pvs-sbcl/Examples/byzantine/C1.ps
/usr/share/doc/pvs-sbcl/Examples/byzantine/C2.ps
/usr/share/doc/pvs-sbcl/Examples/byzantine/README
/usr/share/doc/pvs-sbcl/Examples/byzantine/byzantine.dmp
/usr/share/doc/pvs-sbcl/Examples/byzantine/byzantine.prf
/usr/share/doc/pvs-sbcl/Examples/byzantine/byzantine.ps
/usr/share/doc/pvs-sbcl/Examples/byzantine/byzantine.pvs
/usr/share/doc/pvs-sbcl/Examples/byzantine/cardinality
/usr/share/doc/pvs-sbcl/Examples/byzantine/cardinality/cardinality.prf
/usr/share/doc/pvs-sbcl/Examples/byzantine/cardinality/cardinality.pvs
/usr/share/doc/pvs-sbcl/Examples/byzantine/csl-92-1.dvi.Z
/usr/share/doc/pvs-sbcl/Examples/byzantine/csl-92-1.html
/usr/share/doc/pvs-sbcl/Examples/byzantine/csl-92-1.ps
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/README
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline.dmp
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/basic_defs.prf
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/basic_defs.pvs
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/ops.prf
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/ops.pvs
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/airline/validate.el
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/csl-95-10.html
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/csl-95-10.ps
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar.dmp
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar/mizar.prf
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar/mizar.pvs
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/mizar/validate.el
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/noninterference.sub
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/pvs-strategies
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding.dmp
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding/unwinding.prf
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding/unwinding.pvs
/usr/share/doc/pvs-sbcl/Examples/elementary-tutorial/unwinding/validate.el
/usr/share/doc/pvs-sbcl/Examples/f91.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99
/usr/share/doc/pvs-sbcl/Examples/fm99/bakery.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/bakery.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/bakery.sal
/usr/share/doc/pvs-sbcl/Examples/fm99/bijections.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/bijections.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/eval.lisp
/usr/share/doc/pvs-sbcl/Examples/fm99/expression.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/expression.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/fm99tut.pdf
/usr/share/doc/pvs-sbcl/Examples/fm99/fm99tut.ps
/usr/share/doc/pvs-sbcl/Examples/fm99/fm99tut.tex
/usr/share/doc/pvs-sbcl/Examples/fm99/glade.lisp
/usr/share/doc/pvs-sbcl/Examples/fm99/gprint.lisp
/usr/share/doc/pvs-sbcl/Examples/fm99/hassen.ps
/usr/share/doc/pvs-sbcl/Examples/fm99/lang.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/lang.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/light_bakery.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/light_bakery.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/phone_1.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/phone_1.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/phone_2.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/phone_2.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/phone_3.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/phone_3.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/phone_4.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/phone_4.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/phones.dmp
/usr/share/doc/pvs-sbcl/Examples/fm99/phones.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/phones.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/print.lisp
/usr/share/doc/pvs-sbcl/Examples/fm99/print.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/print.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/sine.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/sine.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/stamps.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/stamps.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/sum.lisp
/usr/share/doc/pvs-sbcl/Examples/fm99/sum.prf
/usr/share/doc/pvs-sbcl/Examples/fm99/sum.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/top.pvs
/usr/share/doc/pvs-sbcl/Examples/fm99/validate.el
/usr/share/doc/pvs-sbcl/Examples/fme96
/usr/share/doc/pvs-sbcl/Examples/fme96/fme96-tutorial.ps
/usr/share/doc/pvs-sbcl/Examples/fme96/half.dmp
/usr/share/doc/pvs-sbcl/Examples/fme96/half.prf
/usr/share/doc/pvs-sbcl/Examples/fme96/half.pvs
/usr/share/doc/pvs-sbcl/Examples/fme96/index.shtml
/usr/share/doc/pvs-sbcl/Examples/fme96/validate.el
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/README
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache.dmp
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/abs_cache.prf
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/abs_cache.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/cache2.prf
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/cache2.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/cache_array.prf
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/cache_array.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/refinement.prf
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/refinement.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/top.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache/trans.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2-3.dmp
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/abs_cache.prf
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/abs_cache.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/cache2.prf
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/cache2.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/cache_array.prf
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/cache_array.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/refinement.prf
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/refinement.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/top.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/cache2.3/trans.pvs
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/forte97.dvi.Z
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/forte97.html
/usr/share/doc/pvs-sbcl/Examples/forte97-tutorial/forte97.ps.gz
/usr/share/doc/pvs-sbcl/Examples/groups.pvs
/usr/share/doc/pvs-sbcl/Examples/pvs-tables
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot.dmp
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/autopilot.prf
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/autopilot.pvs
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/hassen.prf
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/hassen.pvs
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/scr.pvs
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/autopilot/validate.el
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise.dmp
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise/cruise.prf
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise/cruise.pvs
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise/scr.pvs
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/cruise/validate.el
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/csl-95-12.dvi.Z
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/csl-95-12.html
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/csl-95-12.ps.gz
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables.dmp
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables/tablewise.prf
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables/tablewise.pvs
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/decision_tables/validate.el
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables.dmp
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables/simple_tables.prf
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables/simple_tables.pvs
/usr/share/doc/pvs-sbcl/Examples/pvs-tables/simple_tables/validate.el
/usr/share/doc/pvs-sbcl/Examples/stack.pvs
/usr/share/doc/pvs-sbcl/Examples/stacks.pvs
/usr/share/doc/pvs-sbcl/Examples/sum.prf
/usr/share/doc/pvs-sbcl/Examples/sum.pvs
/usr/share/doc/pvs-sbcl/Examples/sum2.pvs
/usr/share/doc/pvs-sbcl/Examples/ustacks.pvs
/usr/share/doc/pvs-sbcl/Examples/vstte12
/usr/share/doc/pvs-sbcl/Examples/vstte12/BFS.prf
/usr/share/doc/pvs-sbcl/Examples/vstte12/BFS.pvs
/usr/share/doc/pvs-sbcl/Examples/vstte12/README
/usr/share/doc/pvs-sbcl/Examples/vstte12/combinators.prf
/usr/share/doc/pvs-sbcl/Examples/vstte12/combinators.pvs
/usr/share/doc/pvs-sbcl/Examples/vstte12/finseq_ops.prf
/usr/share/doc/pvs-sbcl/Examples/vstte12/finseq_ops.pvs
/usr/share/doc/pvs-sbcl/Examples/vstte12/problems.pdf
/usr/share/doc/pvs-sbcl/Examples/vstte12/ring_buffer.prf
/usr/share/doc/pvs-sbcl/Examples/vstte12/ring_buffer.pvs
/usr/share/doc/pvs-sbcl/Examples/vstte12/sri-vstte12-competition.tgz
/usr/share/doc/pvs-sbcl/Examples/vstte12/top.pvs
/usr/share/doc/pvs-sbcl/Examples/vstte12/tree_reconstruction.prf
/usr/share/doc/pvs-sbcl/Examples/vstte12/tree_reconstruction.pvs
/usr/share/doc/pvs-sbcl/Examples/vstte12/two_way_sort.prf
/usr/share/doc/pvs-sbcl/Examples/vstte12/two_way_sort.pvs
/usr/share/doc/pvs-sbcl/Examples/vstte12/vstte12-pvs.tgz
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/README.md
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder.dmp
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder/adder.prf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder/adder.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/adder/validate.el
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones.dmp
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_1.prf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_1.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_2.prf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_2.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_3.prf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_3.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_4.prf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phone_4.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phones.prf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/phones.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/phones/validate.el
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe.dmp
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/pipe.prf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/pipe.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/signal.prf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/signal.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/time.pvs
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/pipe/validate.el
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/wift-tutorial.pdf
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/wift95.html
/usr/share/doc/pvs-sbcl/Examples/wift-tutorial/wift95.ps
/usr/share/doc/pvs-sbcl/PVSio-2.d.pdf
/usr/share/doc/pvs-sbcl/ProofLite-4.2.pdf
/usr/share/doc/pvs-sbcl/README.md
/usr/share/doc/pvs-sbcl/csl-93-9.ps.gz
/usr/share/doc/pvs-sbcl/csl-97-2.ps.gz
/usr/share/doc/pvs-sbcl/extrategies.pdf
/usr/share/doc/pvs-sbcl/interpretations.pdf
/usr/share/doc/pvs-sbcl/language.pdf
/usr/share/doc/pvs-sbcl/manip-guide.pdf
/usr/share/doc/pvs-sbcl/prover.pdf
/usr/share/doc/pvs-sbcl/pvs-api.pdf
/usr/share/doc/pvs-sbcl/pvs-prelude.pdf
/usr/share/doc/pvs-sbcl/pvs-release-notes.pdf
/usr/share/doc/pvs-sbcl/user-guide.pdf
/usr/share/licenses/pvs-sbcl
/usr/share/licenses/pvs-sbcl/LICENSE
/usr/share/licenses/pvs-sbcl/NOTICES
/usr/share/mime/packages/pvs.xml
/usr/share/texlive/texmf-local/tex/latex/pvs
/usr/share/texlive/texmf-local/tex/latex/pvs/pvs.sty
References
Summary
In this tutorial we learn how to install pvs-sbcl on Fedora 36 using yum and [dnf]((/fedora/36/dnf/).
