The Foretellix CTO Blog

Summary: This post acts as a “table of contents” for the whole blog, linking (via tags) to the various posts.

There are now quite a few posts in the Foretellix blog, and readers may get lost. So I added Tags to the various posts, and also created this “general orientation” post, which has links to all the tags (click them to get to the list of related posts). I’ll update this post from time to time.

See also Why this blog, the terminology page and the list of all posts.

So here is what this blog talks about:

Verification is what I am really interested in – how to find bugs before they annoy or kill somebody. I am somewhat interested in formal techniques, but mostly in dynamic verification. I come from HW verification (verifying hardware designs), but am now mainly interested in big-system verification – verifying big, complex systems whose components are made of HW, SW, Machine Learning, Human behavior, physics and so on. Big systems are particularly prone to spec bugs.

Note that verification terminology is different between different verification “tribes” (including the meaning of the term “verification”).

Intelligent Autonomous Systems are an important class of big systems, and IAS verification is really challenging. It includes autonomous-robot verification, the increasingly-important AV verification (verifying Autonomous Vehicles) and more. To a lesser extent, it also touches on security verification (especially fuzzing).

To understand what’s going on in IAS verification I go to verification conferences and follow verification-related blogs.

While thinking about IAS (and automation in general), I blogged about potential results of automation and about AGI safety (keeping the hypothetical, future Artificial General Intelligence safe).

System Verification Framework – SVF – is the (idealized) big-system verification framework I would like to create. SVF is an extension of the constrained-random Coverage-Driven-Verification (CDV) methodology used in HW verification (defined here and detailed here). SVF supports convenient scenario description notations, and tries to deal with the tough problem of generating sensor input streams (also called the Synthetic Sensor Input problem). It can run tests on multiple execution platforms (simulation, physical platforms etc.) and connect to various domain-specific simulators.

SVF relies on multiple kinds of coverage, and supports coverage maximization (the important-but-elusive ability to auto-fill coverage). It supports probabilistic checking (i.e. handling checks which should be TRUE just most of the time).

Machine Learning (ML) is an increasingly-important topic. I wrote several posts about ML-system verification (i.e. verification of systems implemented via ML). I also wrote about Using ML for verification (e.g. using it for coverage maximization). There is also the interesting problem of maintaining ML safety (regardless of how you verify it). Finally, I wrote about training ML via verification environments.