Arena-Based Allocation in Compilers
Arena-based allocation is a memory management strategy in which a large block of memory is pre-allocated, and then many small objects are quickly carved out from that block.
Blog
Technical articles on programming languages, formal methods, and software verification
Understanding the C Runtime: crt0, crt1, crti, and crtn
The C runtime (CRT) is a collection of startup routines, initialization code, standard library support, and sometimes system call wrappers that form the environment in which a C program executes.
Introduction into Logic in computer science
This blog outlines the basics of propositional logic, as explained by the book "Logic in compuer science".
Commit to marriage with TLA+ pt.2
The second part of the conspect of the "Intoduction to TLA+" course by Leslie Lamport.
Do not die hard with TLA+ pt.1
The first part of the conspect of the "Intoduction to TLA+" course by Leslie Lamport.
Small and Big Step Semantics
This blog outlines small-step and big-step semantics, their differences, and applications in analyzing computer programs.
LTL and CTL Applications for Smart Contracts Security
In this blog we explore linear temporal logic as well as computation tree logic, and how we could use them to verify smart-contracts.
Why use formal specification
This blog explores the benefits of formal specification in the context of program verification.