Doubly-Linked-List-VST
The final project for CS2603 (2021 Spring), aiming to verify a doubly linked list library using VST. Collaborating with @karzexcc (by junqi-xie)
vericert
A formally verified high-level synthesis tool based on CompCert and written in Coq. (by ymherklotz)
Our great sponsors
| Doubly-Linked-List-VST | vericert | |
|---|---|---|
| 1 | 1 | |
| 2 | 80 | |
| - | - | |
| 10.0 | 8.3 | |
| almost 3 years ago | about 2 months ago | |
| Coq | Coq | |
| GNU General Public License v3.0 only | GNU General Public License v3.0 only |
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Doubly-Linked-List-VST
Posts with mentions or reviews of Doubly-Linked-List-VST.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2021-12-09.
vericert
Posts with mentions or reviews of vericert.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2021-12-03.
-
There's an ongoing effort to rewrite Principia Mathematica using Coq
There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.
What are some alternatives?
When comparing Doubly-Linked-List-VST and vericert you can also consider the following projects:
Log4jPatcher - A mitigation for CVE-2021-44228 (log4shell) that works by patching the vulnerability at runtime. (Works with any vulnerable java software, tested with java 6 and newer)
koika - A core language for rule-based hardware design 🦑
ConCert - A framework for smart contract verification in Coq
CompCert - The CompCert formally-verified C compiler
Spring Boot - Spring Boot
silveroak - Formal specification and verification of hardware, especially for security and privacy.
kami - A Platform for High-Level Parametric Hardware Specification and its Modular Verification