ChemStor

ChemStor verifies safe chemical storage and disposal configurations by applying formal methods to ensure adherence to explicit safety constraints.

Key Features:

• Mathematical Verification: Utilizes formal methods to provide mathematical guarantees about the correctness of chemical storage and disposal configurations.
• Automated System: Automates determination of safe combinations of chemicals and configuration assignments based on encoded constraints.
• Chemical Interaction Graphs: Constructs graphs that map potential interactions between chemicals using reactivity groups defined by the United States Environmental Protection Agency (EPA).
• Chromatic Number Calculation: Computes the chromatic number of interaction graphs to determine the minimum number of distinct storage or disposal containers required to separate reactive chemicals.
• Satisfiability Modulo Theory Equations: Encodes safety constraints into satisfiability modulo theory (SMT) equations and employs SMT solvers to find valid solutions for safe configurations.

Scientific Applications:

• Incident Prevention: Applied to analyze and resolve ten real-world incidents involving chemical storage or disposal mishaps to prevent potential injuries or property damage.

Methodology:

Constructs a chemical interaction graph based on EPA-defined reactivity groups; computes the graph's chromatic number to derive container groupings; assigns chemicals to containers according to color groups while verifying spatial constraints; and validates proposed configurations using satisfiability modulo theory (SMT) solvers.