Formal verification of reaction systems

Reaction systems are a formalism inspired by the functioning of living cells. They allow for specification and analysis of computational processes in which reactions operate on sets of entities (or molecules).

The behaviour of a reaction system is determined by the interactions of its reactions, which are based on the mechanisms of facilitation and inhibition. The formal treatment of reaction systems is qualitative and there is no direct representation of the number of entities involved in reactions.

ReactICS

ReactICS is a toolkit that allows for verification of Reaction Systems.

The toolkit consists of two separate modules implementing:

• Methods using binary decision diagrams (BDD) for storing and manipulating the state space of the verified system.
• Methods translating the verification problems into satisfiability modulo theories (SMT).

You can read more on ReactICS on the project’s website. The source code of ReactICS is available on Codeberg.