acsl-by-example
RecordFlux
| acsl-by-example | RecordFlux | |
|---|---|---|
| 1 | 2 | |
| 94 | 100 | |
| - | 0.0% | |
| 1.8 | 9.6 | |
| almost 3 years ago | 1 day ago | |
| TeX | Ada | |
| MIT License | GNU Affero General Public License v3.0 |
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.
acsl-by-example
-
Why the C Language Will Never Stop You from Making Mistakes
Yes, Frama-C uses a plugin architecture, and there are plugins to verify all kinds of things, including functional correctness. The Frama-C tutorials page,
https://frama-c.com/html/tutorials.html
Has a link to the ACSL-by-example PDF which gives examples of creating in C various C++ STL inspired data structures and routines:
https://github.com/fraunhoferfokus/acsl-by-example/blob/mast...
Also, it is less effort to write bug-free code in OCaml than C. The Coq/Gallina proof assistant even has an OCaml-extraction (and also Haskell-extraction) feature where you extract runnable code from a formally verified algorithm in the Gallina specification language. (It's generally easier to proof theorems about code in the theorem prover itself, go figure.) Most of these C verification tools are written in OCaml, not C, with varying levels of assistance from Coq/Gallina.
The main reason the functional languages make it easier is because you generally execute side-effect free functions on data structures to give them the mathematical property you want. For example, you execute a lexicographical sort function on a list of strings and then the strings in the list all satisfy the mathematical property of a total ordering. You don't have to do any reasoning about the "in-between state" where pointers under the hood are being manipulated, and you don't have to add pre-conditions and post-conditions about the global environment if the code is side effect free and does not access non-local memory.
RecordFlux
- Why isn't there a Swagger/OpenAPI for binary formats?
-
Althttpd: Simple webserver in a single C-code file by the author of SQLite
RecordFlux[0] is a DSL written in Ada for specifying messages in a binary protocol. Code for parsing these messages is then generated automatically with a number of useful properties automatically proven including that no runtime errors will occur.
[0] https://github.com/Componolit/RecordFlux
What are some alternatives?
sol2 - Sol3 (sol2 v3.0) - a C++ <-> Lua API wrapper with advanced features and top notch performance - is here, and it's great! Documentation:
kaitai-to-wireshark - Converts a Kaitai Struct file description to a Wireshark LUA plugin
hacl-star - HACL*, a formally verified cryptographic library written in F*
darkhttpd - When you need a web server in a hurry.
CompCert - The CompCert formally-verified C compiler
flsplit - Simple tool to split FL Studio project files by playlist track.
spark-by-example - SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
grpc-swagger - Debugging gRPC application with swagger-ui.
gcc
FreeRTOS-Kernel - FreeRTOS kernel files only, submoduled into https://github.com/FreeRTOS/FreeRTOS and various other repos.
restruct - Rich binary (de)serialization library for Golang