Counterexample-guided Abstraction Refinement (CEGAR) algorithm reduces the state space by merging multiple states and refining only when necessary, thereby improving the state explosion problem in model checking.

This article briefly describes the program synthesis algorithm presented in the paper 'Synthesis of Reactive(1) designs'.

This article writes about what is adjoints in category theory.

This article writes about what is limits/colimits in category theory.

This article writes about what is natural transformation.

How to prove x in computability theory

Introduction to two ways of defining real numbers: Dedekind cuts and Cauchy sequences, and discussion of their equivalence

This article explains the concepts of Büchi automata, ω-regular languages and ω-regular expressions, and the conversion algorithms between Büchi automata and ω-regular expressions.

This article explains the concept of pushdown automata.

This article is about set quotients.