SRI-CSL / PVSLinks
The People's Verification System
☆155Updated this week
Alternatives and similar repositories for PVS
Users that are interested in PVS are comparing it to the libraries listed below
Sorting:
- ACL2 System and Books as Maintained by the Community☆397Updated this week
- Lecture material for DeepSpec Summer School 2018☆68Updated 6 years ago
- An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logt…☆145Updated 8 months ago
- A Verified Compiler for Gallina, Written in Gallina☆152Updated 2 months ago
- SRI Sally: A model checker for infinite-state systems.☆74Updated this week
- Verification-condition-generation-based verifier for the Viper intermediate verification language.☆30Updated last week
- An efficient implementation of the higher-order logic programming language Lambda Prolog☆155Updated last year
- Tools for interacting with Boogie☆47Updated 3 months ago
- Mostly Automated Synthesis of Correct-by-Construction Programs☆153Updated 2 months ago
- Lecture notes for a short course on proving/programming in Coq via SSReflect.☆168Updated 3 years ago
- Randomized Property-Based Testing Plugin for Coq☆265Updated this week
- A fast implementation of miniKanren with disequality and absento, compatible with Racket and Chez.☆158Updated 4 months ago
- Communication between Coq and SAT/SMT solvers☆159Updated 9 months ago
- Emacs support for F*☆70Updated 2 months ago
- Lem semantic definition language☆139Updated 3 months ago
- An implementation of Hoare and He's Unifying Theories of Programming in Isabelle☆36Updated last year
- ☆56Updated 2 months ago
- A less devious proof assistant☆224Updated 2 years ago
- Git mirror of https://isabelle.in.tum.de/repos/isabelle☆70Updated this week
- SPARK 2014 repository for the Why3 verification platform.☆31Updated this week
- The Mechanization of Standard ML☆73Updated 2 years ago
- Embeddable Lambda Prolog Interpreter☆312Updated 3 weeks ago
- CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory☆228Updated 2 months ago
- Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintaine…☆76Updated 5 months ago
- The Ciao Preprocessor☆11Updated this week
- Modeling and Proving in Computational Type Theory☆101Updated last week
- Coq Protocol Playground with Se(xp)rialization of Internal Structures.☆133Updated 7 months ago
- Public snapshots of "ACSL by Example"☆111Updated last month
- A Coq IDE build on top of Proof General's Coq mode☆356Updated 2 years ago
- Gallina to Bedrock2 compilation toolkit☆56Updated this week