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

(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 also https://github.com/mkf/asdspark

This repository contains the end-of-semester project at ISEP in formal approach. The aim was to prove the proper functioning of a bubble sorter via frama-c.

Small examples of ACSL specifications.

Using an automated software engineering tool like Frama-C to analyze a program or system.

Frama-C is a suite of tools for analyzing C code, verifying correctness, and detecting issues. This repository includes folders for programming exercises and code analysis, covering basic programs, arrays, and loops.

Tiny programs with ACSL specifications.

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

Programming Languages

exploring program slicing and documenting my discoveries

generative programming & verification

Linux kernel library functions formally verified.