Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Bringing LTL Model Checking to Biologists Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Static Analysis of Communicating Processes Using Symbolic Transducers

Authors : Vincent Botbol, Emmanuel Chailloux, Tristan Le Gall

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Synthesizing Non-Vacuous Systems
next chapter Reduction of Workflow Nets for Generalised Soundness Verification
Footnotes
1
See [10] or [2].
 
2
No transition is labeled by \(\bot \).
 
Literature
1.
Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-28644-8_​3 CrossRef
2.
3.
4.
Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications. LNCS, vol. 735, pp. 128–141. Springer, Heidelberg (1993)CrossRef
5.
6.
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of POPL 1977: The 4th ACM Symposium on Principles of Programming Languages, pp. 238–252 (1977)
7.
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of POPL 1978: The 5th ACM Symposium on Principles of Programming Languages, pp. 84–96 (1978)
8.
9.
Ferrara, P.: Checkmate: a generic static analyzer of java multithreaded programs. In: 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, pp. 169–178, November 2009
10.
Le Gall, T., Jeannet, B.: Lattice automata: a representation for languages on infinite alphabets, and some applications to verification. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 52–68. Springer, Berlin, Heidelberg (2007). doi:10.​1007/​978-3-540-74061-2_​4 CrossRef
11.
Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Berlin, Heidelberg (2009). doi:10.​1007/​978-3-642-02658-4_​52 CrossRef
12.
Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015)MathSciNetCrossRef
13.
14.
15.
Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J.: MPI-The Complete Reference: The MPI Core, vol. 1, 2nd edn. MIT Press, Cambridge (1998)
16.
Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjørner, N.: Symbolic finite state transducers: algorithms and applications. In: Conference Record of POPL 2012: The 39th ACM Symposium on Principles of Programming Languages, pp. 137–150 (2012)
17.
Vo, A., Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical MPI programs. ACM Sigplan Not. 44(4), 261–270 (2009)CrossRef
Metadata
Title
Static Analysis of Communicating Processes Using Symbolic Transducers
Authors
Vincent Botbol
Emmanuel Chailloux
Tristan Le Gall
Copyright Year
2017
Book
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-319-52233-3

Electronic ISBN: 978-3-319-52234-0

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-52234-0_5

Premium Partner

    Image Credits