Category
13 posts
Although Model Checking can seem a very specific topic, understanding its concepts is a crucial point for many theoretical Formal Verification jobs, but also for many real-world applications. Our blog tries to combine what we have learned from the previous blogs with the coding.
Büchi Automata define a class of languages where the words are infinite. Discover how they are used in Model Checking to describe both models and properties.
Similar to Linear Temporal Logic (LTL), Computational Tree Logic (CTL) is a crucial Model Checking tool that is used to test model's properties.
How does Model Checking work? How to verify properties on a model? This depends in general from the logic type used, and this blog post covers all of it!
Learn how Linear Temporal Logic (LTL) is used in Model Checking to express and verify system properties over time. Explore Kripke structures, syntax, semantics, and examples with clear explanations.
Model Checking is the verification of the correctness of a system's models. In this blog, we discover the different ways to correctly and easily model our system.
Model Checking is a core method used in Formal Verification to prove properties of a running system after modeling it. Step by step, we dicover together how modelling, defining properties and the actual model checking actually works. We start with the small introduction into different tools that will be used in this series.
How diffusion models generate images by reversing a gradual noise process — forward and reverse Markov chains, DDPM, and why they rival GANs on sample quality.
How GANs learn by pitting a generator against a discriminator — the minimax game, and why adversarial training replaced explicit density estimation.
Normalizing Flows turn a simple Gaussian into a complex distribution through invertible transformations, enabling exact and tractable likelihood computation.
A Variational Autoencoder (VAE) is a generative model that learns a compressed, continuous representation (a latent space) of data. It consists of an encoder network that maps data to a distribution in the latent space and a decoder network that reconstructs data from samples drawn from that latent distribution.
Gaussian Mixture Models express a probability distribution as a weighted combination of Gaussians, capturing multi-modal data through interpretable components.
An introduction to probabilistic generative modeling: how generative models differ from discriminative ones, and the concepts behind five key model families.