POPL 2017 (series) / VMCAI 2017 (series) / VMCAI /
Static Analysis of Communicating Process using Symbolic Transducers
We present a general model allowing static analysis based on abstract interpretation for systems of communicating processes. Our technique, inspired by Regular Model Checking, represent 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 and therefore allowing us to prove safety properties. We implemented this method in a prototype that targets the MPI library for C programs.
slides (botbol-slides.pdf) | 700KiB |
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | |||
14:00 30mTalk | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI | ||
14:30 30mTalk | Independence Abstractions and Models of Concurrency VMCAI | ||
15:00 30mTalk | Static Analysis of Communicating Process using Symbolic Transducers VMCAI Vincent Botbol CEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le Gall CEA LIST, Emmanuel Chailloux LIP6 - UPMC Media Attached File Attached |