1: \begin{abstract}

2: This paper is concerned with developing a software tool, called \textsf{IMPaCT}, for the parallelized verification and controller synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs), respectively. The tool serves to (i) construct IMCs/IMDPs as finite abstractions of underlying original systems, and (ii) leverage \emph{interval iteration} algorithms for formal verification and controller synthesis over \emph{infinite-horizon} properties, including safety, reachability, and reach-avoid, while offering \emph{convergence guarantees}. \textsf{IMPaCT} is developed in C++ and designed using AdaptiveCpp, an independent open-source implementation of SYCL, for adaptive parallelism over CPUs and GPUs of all hardware vendors,

3: including Intel and NVIDIA. \textsf{IMPaCT} stands as the first software tool for the parallel construction of IMCs/IMDPs, empowered with the capability to leverage high-performance computing platforms and cloud computing services. Specifically, parallelism offered by \textsf{IMPaCT} effectively addresses the challenges arising from the state-explosion problem inherent in discretization-based techniques applied to large-scale stochastic systems. We benchmark \textsf{IMPaCT} on several physical case studies, adopted from the ARCH tool competition for stochastic models, including a $2$-dimensional robot, a $3$-dimensional autonomous vehicle, a $5$-dimensional room temperature system, and a $7$-dimensional building automation system. To show the scalability of our tool, we also employ \textsf{IMPaCT} for the formal analysis of a $14$-dimensional case study.\\

4: 

5: {\bf Keywords:} Interval Markov chain, interval Markov decision process, automated controller synthesis, large-scale stochastic systems, parallel construction, cloud computing

6: \end{abstract}