Static analysis of communicating processes using symbolic transducers

DOI10.1007/978-3-319-52234-0_5MaRDI QIDQ2961555zbMATH OpenOpenAlexFDO

Authors Vincent Botbol, Emmanuel Chailloux, Tristan Le Gall

Publication date 21 February 2017

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1611.07812

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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.

Recommendations

• An algorithm for analyzing communicating processes
• Process-local static analysis of synchronous processes
• scientific article; zbMATH DE number 4033050
• A Generic Approach to the Static Analysis of Concurrent Programs with Procedures
• A generic approach to the static analysis of concurrent programs with procedures

Cites work

• Computer Aided Verification
• CONCUR 2004 - Concurrency Theory
• Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification
• Relational thread-modular static value analysis by abstract interpretation
• Static analysis of communicating processes using symbolic transducers
• Symbolic finite state transducers: algorithms and applications
• The octagon abstract domain

Cited in

(7)

• Static analysis of communicating processes using symbolic transducers
• Static Analysis of Dynamic Communication Systems by Partner Abstraction
• scientific article; zbMATH DE number 4033050 (Why is no real title available?)
• Quantitative static analysis of communication protocols using abstract Markov chains
• Process-local static analysis of synchronous processes
• An algorithm for analyzing communicating processes
• Clustered relational thread-modular abstract interpretation with local traces

Describes a project that uses

Uses Software

• Checkmate
• Frama-C
• ISP
• Apron
• MPI

This page was built for publication: Static analysis of communicating processes using symbolic transducers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2961555)