Skip to content

Encoding Vesicle Traffic System in Z3 and CBMC

Notifications You must be signed in to change notification settings

arey0pushpa/pyZ3

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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