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)
ConCert
A framework for smart contract verification in Coq (by AU-COBRA)
Our great sponsors
| Doubly-Linked-List-VST | ConCert | |
|---|---|---|
| 1 | 1 | |
| 2 | 108 | |
| - | 1.9% | |
| 10.0 | 8.0 | |
| almost 3 years ago | 3 months ago | |
| Coq | Coq | |
| GNU General Public License v3.0 only | MIT License |
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.
ConCert
Posts with mentions or reviews of ConCert.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2021-06-23.
-
Rustlang Cryptography Interest Group & Formal Verification Sync-up Call 2
Bas Spitter will be speaking on Hacspec and ConCert
What are some alternatives?
When comparing Doubly-Linked-List-VST and ConCert 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)
hacspec - Please see https://github.com/hacspec/hax
vericert - A formally verified high-level synthesis tool based on CompCert and written in Coq.
scilla - Scilla - A Smart Contract Intermediate Level Language
Spring Boot - Spring Boot
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
toychain - A minimalistic blockchain consensus implemented and verified in Coq