Release snapshots of the Frama-C platform for source code analysis

• UpdatedOct 21, 2020
• OCaml

Public snapshots of "ACSL by Example"

• UpdatedJun 17, 2021
• TeX

Frama-C and WP tutorial

• UpdatedDec 19, 2024
• TeX

Linux kernel library functions formally verified.

• UpdatedFeb 11, 2021
• C

generative programming & verification

• UpdatedNov 20, 2021
• C

Generation of mutant programs

• UpdatedOct 31, 2018
• OCaml

Fully proved small C functions (examples for verification course).

• UpdatedJun 26, 2017
• C

Frama-C plugins for deadlock and data race detection

• UpdatedDec 23, 2024
• OCaml

Static & Dynamic Verification of C programs

• UpdatedOct 5, 2019
• OCaml

Github Action for running the Eva plug-in and producing a SARIF report

• UpdatedOct 20, 2021
• Shell

Tiny programs with ACSL specifications.

• UpdatedFeb 10, 2017
• C

Towards a formally verified, tiny and permissively licensed C standard library, using Frama-C (fork of Baselibc/Klibc)

• UpdatedJun 17, 2019
• C

sonar-frama-c-plugin is a plugin sonarqube to integrate frama-c results

• UpdatedMay 3, 2023
• Java

Inlining of ACSL predicates and logic functions

• UpdatedSep 19, 2018
• OCaml

exploring program slicing and documenting my discoveries

• UpdatedJun 23, 2024
• C

Cybersecurity master courses

• UpdatedNov 4, 2022
• Python

Docker image for Frama-C

• UpdatedApr 18, 2021
• Dockerfile

A complete basic implementation of Queue data structure tested in Frama-c

• UpdatedJan 5, 2022
• Coq

• UpdatedMay 19, 2017
• C

(at turn of) 2019/2020: kilka zadań z przedm. Algorytmy zrobionych z dowodami we Frama-C. See the WIP in feature branches. For some other problems from this set done with Spark2014, see alsohttps://github.com/mkf/asdspark

• UpdatedJan 13, 2020
• C