Home

Contents

1. What is Zen?
2. Why use Zen?
3. How does Zen work?

What is Zen?

Zen is a C# library that simplifies the application of formal methods techniques to various domains. This includes problems such as finding inputs to search problems (e.g., scheduling) with constraint solvers, identifying bugs in software or proving software's correctness with model checking, generating high-coverage test suits with symbolic execution, and more.

Why use Zen?

What many of the above problems have in common is that, despite their high theoretical computational cost, they often can be solved efficiently via low-level encodings to general constraint solver technologies such as SMT solvers. However, such encodings are frequently low-level, tedious to implement, and challenging to optimize and debug. Zen aims to simplify this process for many common tasks by providing a higher-level symbolic reasoning API and then automating this encoding process for the user of the library.

How does Zen work?

The library provides a new type Zen<T> for a C# type T, which represents a "searchable" value. These values are manipulated either by using library-provided functions or by writing custom user-functions. Given functions that process Zen values, the library can search over their inputs to find values of interest to the user. Internally, Zen makes heavy use of C#'s reflection capabilities to introspect the C# types used for search and produce an efficient encoding without requiring any additional user effort.