PRISMATIC: UNIFIED HIERARCHICAL PROBABILISTIC VERIFICATION TOOL Verification of entire cyber-physical systems poses several key challenges, including heterogeneous designs that span cyber and physical domains; uncertainty in component reliability and partially-sensed, uncontrollable environments; and large-scale designs with operating state spaces far larger than can be handled by existing verification approaches. To meet these challenges we developed PRISMATIC, a workflow/process and tool that can generate probabilistic “certificates of correctness” for entire large-scale cyber-physical systems such as ground combat vehicles or aircraft. Our team had previously developed several ground-breaking verification methods and state-of-the art open-source verification tools. We built on these existing tools and develop unique new capabilities for scaling through compositionality to meet the challenges of cyber-physical system design and manufacturing flow. David J. Musliner and Eric Engstrom
 Smart Information Flow Technologies (SIFT, LLC)