/pyZ3

Encoding Vesicle Traffic System in Z3 and CBMC

Primary LanguageTeX

PyZ3

A Eukaryotic cell contains multiple membrane-bound compartments. Transport vesicles move cargo between these compartments, just as trucks move cargo between warehouses.

The complete vesicle fusion process is modeled as a constraint over a labeled graph. Where node represents compartments and directed edges are vesicles. The whole network is recyclable [molecule moves only in cycles]. We call this labeled network as Vesicle Traffic System (VTS).

We have modeled the VTS using CBMC [C Bounded Model Checker] and python Z3 [Z3 Theorem Prover].