Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Sun 15 Jan 2017 15:00 - 15:30 at Amphitheater 44 - Concurrency 1 Chair(s): Camille Coti

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 Jan

VMCAI-2017-papers
14:00 - 15:30: VMCAI - Concurrency 1 at Amphitheater 44
Chair(s): Camille CotiLIPN, Université Paris 13
VMCAI-2017-papers148448520000014:00 - 14:30
Talk
VMCAI-2017-papers148448700000014:30 - 15:00
Talk
Vijay D'SilvaGoogle Inc., Daniel KroeningUniversity of Oxford, Marcelo SousaUniversity of Oxford
VMCAI-2017-papers148448880000015:00 - 15:30
Talk
Vincent BotbolCEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le GallCEA LIST, Emmanuel ChaillouxLIP6 - UPMC
Media Attached File Attached