### 8 releases (5 breaking)

0.9.1 | May 6, 2022 |
---|---|

0.9.0 | May 3, 2022 |

0.5.1 | Sep 28, 2021 |

0.4.0 | Sep 26, 2021 |

0.1.0 | Aug 27, 2021 |

#**155** in Science

Used in mikino

**MIT/Apache**

280KB

6.5K
SLoC

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. For instance, mikino as an input language much easier to get into than SMT-LIB 2 (the SMT solver input language standard). Also, we took great care in making its output as readable and easy to understand as possible.

Mikino comes with [a tutorial on SMT, induction (and strengthening)][dummies]. Definitely read it if you're new to either of these topics, or just take a look at the examples throughout to get a taste of mikino.

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

k

Contents:

- Installing
- Basics
- SMT Solver (Z3)
- Building From Source
- Transition Systems
- Scripts
- Dependencies
- License

# 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.

`>` mikino `-V`
`mikino`` 0.9.0`

# Basics

You can run mikino in demo mode with

. This will write a heavily commented
example system in `mikino demo demo .mkn`

`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

is also probably a good idea.`mikino help`

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

, or`z3` - use mikino's

to specify how to call it, for instance:`--z3_cmd`

if`mikino``-``-`z3_cmd my_z3`...`

is in your path, or`my_z3`

if`mikino``-``-`z3_cmd`.``/`path`/`to`/`my_z3`...`

is where the Z3 binary is.`path``/`to`/`my_z3

# Building From Source

`>` cargo `build`` --`release
`>` ./target/release/mikino `--version`
`mikino`` 0.9.0`

# Transition Systems

A (transition) system is composed of some variable declarations, of type

, `bool`

or `int`

(rational). A valuation of these variables is usually called a `rat`*state*. (An

is a
`int`*mathematical* integer here: it cannot over/underflow. A

is a fraction of `rat`

s.)`int`

Let's use a simple counter system as an example. Say this system has two variables,

`of type`

cnt`and`

int`of type bool.`

inc

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

`variable's initial value to be anything as long as it is positive. Our initial predicate will be`

cnt`. Note that variable`

cnt ≥0`is irrelevant in this predicate.`

inc

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

is written `v`

, and its `'v`*current*
version is just written

.`v`

Our counter should increase by

`whenever variable`

1`is true, and maintain its value otherwise. There is several ways to write this, for instance`

inc

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

ifinc{'cnt=cnt+1}else{'cnt=cnt}or

'cnt=ifinc{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

`. The system is safe for this candidate as no reachable state of the counter can falsify it.`

(≥ cnt0)The candidate

`does not hold in all reachable states, in fact the initial state`

¬(cnt=7)`falsifies it. But assume we change the initial predicate to be`

{cnt:7,inc:_}`. Then the candidate is still falsifiable by applying the transition relation seven times to the (only) initial state`

cnt=0`. In all seven transitions, we need`

{cnt:0,inc:_}`to be true so that`

inc`is actually incremented.`

cnt

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

`for the last system above with the modified initial predicate is`

¬(cnt=7)

Step0|cnt:0Step1|cnt:1|inc:trueStep2|cnt:2|inc:trueStep3|cnt:3|inc:trueStep4|cnt:4|inc:trueStep5|cnt:5|inc:trueStep6|cnt:6|inc:trueStep7|cnt:7|inc:true

# Scripts

Mikino also has a

mode which runs scripts in Rust-flavored SMT-LIB 2. The syntax is very
similar to that of transition system, check out the demo by running `script`

.`mikino demo --script demo_script.rs`

# 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][apache] and [LICENSE-MIT][mit] for details.

Copyright © OCamlPro SAS

(SMT on wikipedia)

(Z3's wiki on github)

(Z3's release page on github)

(kino on github) [apache]: https://github.com/AdrienChampion/mikino/blob/master/LICENSE-APACHE (Apache 2.0 license on github) [mit]: https://github.com/AdrienChampion/mikino/blob/master/LICENSE-MIT (MIT license on github) [dummies]: https://ocamlpro.com/blog/2021_10_14_verification_for_dummies_smt_and_induction (Induction for Dummies: SMT and Induction)

#### Dependencies

~3.5–5.5MB

~107K SLoC