PrincetonUniversity / Vst
Licence: other
Verified Software Toolchain
Stars: ✭ 264
Labels
Projects that are alternatives of or similar to Vst
RiscvSpecFormal
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
Stars: ✭ 69 (-73.86%)
Mutual labels: coq
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Stars: ✭ 15 (-94.32%)
Mutual labels: coq
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Stars: ✭ 41 (-84.47%)
Mutual labels: coq
multinomials
Multinomials for the Mathematical Components library.
Stars: ✭ 12 (-95.45%)
Mutual labels: coq
FreeSpec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 48 (-81.82%)
Mutual labels: coq
LibHyps
A Coq library providing tactics to deal with hypothesis
Stars: ✭ 14 (-94.7%)
Mutual labels: coq
InfSeqExt
A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
Stars: ✭ 12 (-95.45%)
Mutual labels: coq
topology
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Stars: ✭ 36 (-86.36%)
Mutual labels: coq
Set-Theory
Coq encoding of ZFC and formalization of the textbook Elements of Set Theory
Stars: ✭ 55 (-79.17%)
Mutual labels: coq
chapar
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Stars: ✭ 29 (-89.02%)
Mutual labels: coq
with contributions from
Andrew W. Appel, Lennart Beringer, Robert Dockins, Josiah Dodds, Aquinas Hobor, Jean-Marie Madiot, Gordon Stewart, Qinxiang Cao, Qinshi Wang, and others.
The LICENSE file has information about copyright, licensing, and permissions.
How to install:
Documentation:
Our webpage describes the goals of the project and has links to many related publications.
For an introduction to how to use Verifiable C, read the manual, or consult Software Foundations Volume 5: Verifiable C for a tutorial with exercises.
Program Logics for Certified Compilers, by Andrew W. Appel et al., Cambridge University Press, 2014. Available in hardcover.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].