A simple induction and BMC engine.

Overview

Mikino is a (relatively) simple induction and BMC engine. Its goal is to serve as a simple yet interesting tool for those interested in formal verification, especially SMT-based induction.

"Mikino" does not mean cinema. It is a contraction of "mini" and "kinō" (帰納: induction, recursion). It is a significantly simpler version of the now defunct kino k-induction engine on transition systems.

crates.io

Contents:

Installing

Make sure Rust is installed and up to date.

> rustup update

Use cargo to install mikino.

> cargo install mikino

That's it. Alternatively, you can build it from source.

Basics

You can run mikino in demo mode with mikino demo demo.mkn. This will write a heavily commented example system in demo.mkn. There is a discussion on transition systems below that goes into details on the input format, using this exact system as an example.

Running mikino help is also probably a good idea.

Note that mikino files are designed to work well with Rust syntax highlighting.

SMT Solver (Z3)

Mikino requires an SMT solver to run induction (and BMC). More precisely, it requires Z3 which you can download directly from the Z3 release page. You must either

  • make sure the Z3 binary is in your path, and is called z3, or
  • use mikino's --z3_cmd to specify how to call it, for instance:
    • mikino --z3_cmd my_z3 ... if my_z3 is in your path, or
    • mikino --z3_cmd ./path/to/my_z3 ... if path/to/my_z3 is where the Z3 binary is.

Building From Source

> cargo build --release
> ./target/release/mikino --version
mikino 0.5.0

Transition Systems

A (transition) system is composed of some variable declarations, of type bool, int or rat (rational). A valuation of these variables is usually called a state. (An int is a mathematical integer here: it cannot over/underflow. A rat is a fraction of ints.)

Let's use a simple counter system as an example. Say this system has two variables, cnt of type int and inc of type bool.

The definition of a system features an initial predicate. It is a boolean expression over the variables of the system that evaluate to true on the initial states of the system.

Assume now that we want to allow our counter's cnt variable's initial value to be anything as long as it is positive. Our initial predicate will be cnt ≥ 0. Note that variable inc is irrelevant in this predicate.

Next, the transition relation of the system is an expression over two versions of the variables: the current variables, and the next variables. The transition relation is a relation between the current state and the next state that evaluates to true if the next state is a legal successor of the current one. A the next version of a variable v is written 'v, and its current version is just written v.

Our counter should increase by 1 whenever variable inc is true, and maintain its value otherwise. There is several ways to write this, for instance

(inc ⋀ 'cnt = cnt + 1) ⋁ (¬inc ⋀ 'cnt = cnt)

or

if inc { 'cnt = cnt + 1 } else { 'cnt = cnt }

or

'cnt = if inc { cnt + 1 } else { cnt }

Last, the transition system has a list of named candidates (candidate invariants) which are boolean expressions over the variables. The system is safe if and only if it is not possible to reach a falsification of any of these candidates from the initial states by applying the transition relation repeatedly.

A reasonable candidate for the counter system is (≥ cnt 0). The system is safe for this candidate as no reachable state of the counter can falsify it.

The candidate ¬(cnt = 7) does not hold in all reachable states, in fact the initial state { cnt: 7, inc: _ } falsifies it. But assume we change the initial predicate to be cnt = 0. Then the candidate is still falsifiable by applying the transition relation seven times to the (only) initial state { cnt: 0, inc: _ }. In all seven transitions, we need inc to be true so that cnt is actually incremented.

A falsification of a candidate is a concrete trace: a sequence of states i) that starts from an initial state, ii) where successors are valid by the transition relation and iii) such that the last state of the sequence falsifies the PO.

A falsification of ¬(cnt = 7) for the last system above with the modified initial predicate is

Step 0
| cnt: 0
Step 1
| cnt: 1
| inc: true
Step 2
| cnt: 2
| inc: true
Step 3
| cnt: 3
| inc: true
Step 4
| cnt: 4
| inc: true
Step 5
| cnt: 5
| inc: true
Step 6
| cnt: 6
| inc: true
Step 7
| cnt: 7
| inc: true

Dependencies

Mikino relies on the following stellar libraries:

License

Mikino is distributed under the terms of both the MIT license and the Apache License (Version 2.0).

See LICENSE-APACHE and LICENSE-MIT for details.


Copyright © OCamlPro SAS

You might also like...
Simple MHV6 extension used to download custom songs efficiently and effectively.

nong-downloader-extension A simple MegaHack v6 extension that helps you download NONG songs directly to GD. Compiling. Why would you want to compile??

A clean and simple network looking glass application
A clean and simple network looking glass application

lg lg is my custom Looking Glass server software for use in ZZANet. The whole application is lightweight, self-contained, and easy to use even outside

Fast and simple PHP version manager written in rust

[WIP] phpup (PHP-up): Fast and Simple PHP version manager ⚡ Fast and simple PHP version manager, written in rust Features No requirements for system P

A simple and fast FRC autonomous path planner (designed for swerve drive)! (Desktop/Laptop only)

This is a website developed for planning autonomous paths for FRC robots. It is intended to be a simple and fast tool to create autos, which works offline at competitions.

qn (quick note) is a simple, fast and user-friendly way to save notes 🦀⚙️
qn (quick note) is a simple, fast and user-friendly way to save notes 🦀⚙️

Quick Note qn Install This is currently for my personal use. I may push breaking changes at any time. If you want to use it, bring down the code and r

A simple, stable and thread-safe implementation of a lazy value

Laizy Laizy is a Rust library that provides a simple, stable and thread-safe implementation of a Lazy Features Name Description Dependencies nightly A

A simple, fast and fully-typed JSPaste API wrapper for Rust

rspaste A simple, fast and fully-typed JSPaste API wrapper for Rust. aidak.tk » Installation Put the desired version of the crate into the dependencie

Amethyst is a systems language aimed at being simple, small, portable, and safe.

amethyst Amethyst is a systems language aimed at being simple, small, portable, and safe. What is this language? From the r/ProgLangs discord server:

Cassette A simple, single-future, non-blocking executor intended for building state machines.

Cassette A simple, single-future, non-blocking executor intended for building state machines. Designed to be no-std and embedded friendly. This execut

Comments
  • V0.4

    V0.4

    • updated to mikino_api v0.4
    • expressions now have a Rust-like syntax (including if-then-else-s)
    • section keywords have changed: state, init, trans, candidates
    opened by AdrienChampion 0
Releases(v0.9.3)
Owner
OCamlPro
OCamlPro
This is a simple Telegram bot with interface to Firefly III to process and store simple transactions.

Firefly Telegram Bot Fireflies are free, so beautiful. (Les lucioles sont libres, donc belles.) ― Charles de Leusse, Les Contes de la nuit This is a s

null 13 Dec 14, 2022
MeiliSearch is a powerful, fast, open-source, easy to use and deploy search engine

MeiliSearch is a powerful, fast, open-source, easy to use and deploy search engine. Both searching and indexing are highly customizable. Features such as typo-tolerance, filters, and synonyms are provided out-of-the-box. For more information about features go to our documentation.

MeiliSearch 31.6k Dec 30, 2022
A collection of exponentially-smoothed camera controllers for the Bevy Engine.

smooth-bevy-cameras A collection of exponentially-smoothed camera controllers for the Bevy Engine. Look Transform All controllers are based on a LookT

Duncan 122 Dec 24, 2022
A scalable differentiable probabilistic Datalog engine, with Rust

Scallop A scalable probabilistic datalog engine with Rust. Usage The Scallop system is best integrated inside of the Rust context. With scallop! { ...

null 74 Oct 24, 2022
Blueboat is an open-source alternative to Cloudflare Workers. The monolithic engine for serverless web apps.

Blueboat Blueboat is an open-source alternative to Cloudflare Workers. Blueboat aims to be a developer-friendly, multi-tenant platform for serverless

Heyang Zhou 1.8k Jan 9, 2023
A prisma query-engine concurrency runner

Smash A prisma query-engine concurrency runner. Smash can be used to run concurrent requests against the prisma query engine. Currently it has workloa

garren smith 2 Jan 26, 2022
This crate converts Rust compatible regex-syntax to Vim's NFA engine compatible regex.

This crate converts Rust compatible regex-syntax to Vim's NFA engine compatible regex.

kaiuri 1 Feb 11, 2022
Toy: Layout-Engine

Toy: Layout-Engine

Oanakiaja 5 Mar 29, 2022
Safe API to embed an ECMAScript engine.

Kopi Kopi is a small abstraction to easily and safely embed an ECMAScript runtime inside a Rust based application. It uses the V8 execution engine to

Nils Hasenbanck 3 Dec 20, 2022
Small and simple stateful applications, designed to facilitate the monitoring of unwanted behaviors of the same.

Violet Violet é um pequeno e simples monitorador de aplicação, voltado para receber eventos de erro e estado. Instalação simples: Dependencias: Docker

Lucas Mendes Campos 3 Jun 4, 2022