2016/11/23 by Vincent Botbol, Botbol, Vincent, Emmanuel Chailloux +3
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Security and Verification in Computing #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.1611.07812
openalex publication_date 2016/11/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a general model allowing static analysis based on abstract interpretation for systems of communicating processes. Our technique, inspired by Regular Model Checking, represents set of program states as lattice automata and programs semantics as symbolic transducers. This model can express dynamic creation/destruction of processes and communications. Using the abstract interpretation framework, we are able to provide a sound over-approximation of the reachability set of the system thus allowing us to prove safety properties. We implemented this method in a prototype that targets the MPI library for C programs.