Probabilistic and symbolic tools for p program verification

Is a programming language based on state machines, especially suited for the definition of asynchronous event-driven open systems. The language was designed with verification in mind and it is bundled with back-end analysis engines for model checking. The aim of this proposal is to develop techniques for extending such verification capabilities in two directions: by enabling probabilistic modeling and statistical model checking, and symbolic modeling and reachability analysis for checking P programs against an open environment. In both cases, defining the probabilistic or symbolic behavior of ghost machines is at the heart of the approach. Rewriting logic is the formal semantic framework of choice for the proposed verification techniques and tools. The verification algorithms will be bundled and made available via an API (with a proof-of-concept tool with a GUI), thus allowing its later integration to different programming environments and existing tools. Case studies will be developed to illustrate the capabilities of the approach.