This repository contains a collection of formal verification models, compiler experiments, and testing suites designed to improve software reliability and correctness. The projects within this repository utilize TLA+ for formal verification, Java for property-based testing, and ANTLR for compiler development.
The repository is organized into several sections:
The formal_verification directory includes various subdirectories, each targeting different systems and concepts using TLA+:
-
TLA+: Contains specific implementations for distributed systems algorithms and designs, such as Kafka's leader election, Raft consensus, and simple algorithmic examples.
kafka: Models focusing on leader election within Kafka.raft: Contains implementations for Raft distributed consensus.simple: Simple models like Dining Philosophers, Stack operations, and counter implementations.strimzi: Models related to Strimzi operations, like topic lifecycle management.
-
Abstract Interpretation: Contains examples in a point language demonstrating abstract interpretation concepts.
-
Model Checking: A directory dedicated to examples that demonstrate model checking.
The compilers directory contains work related to programming languages and compiler construction:
- O-language: A simple imperative language with integer and boolean support, focusing on arithmetic operations and loops.
- Unicorn-language: A Java-like language that replaces semicolons (
;) with🦄, built with ANTLR. - C-compiler: A custom-designed C compiler, structured similarly to
clang/gcc, with lexical analysis, parsing, and code generation.
The assembly directory contains various experiments and implementations related to low-level programming.
The profiling directory includes tools and experiments for analyzing performance characteristics of programs.
The testing directory is focused on software testing methodologies:
- Performance Testing: Contains strategies for performance testing, particularly of the
utosystem. - Property-Based Testing: Demonstrates the implementation of property-based testing in Java.
The other directory contains miscellaneous projects and experiments.
[1] Introduction to Static Analysis - Link