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:
Cover of the book

2018 | OriginalPaper | Chapter

Distributed Analysis of the BMC Kind: Making It Fit the Tornado Supercomputer

Authors : Azat Abdullin, Daniil Stepanov, Marat Akhin

Published in: Tools and Methods of Program Analysis

Publisher: Springer International Publishing

Log in

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

search-config
loading …

Abstract

Software analysis is becoming increasingly important as a way of software quality assurance. Most works in this area focus their attention on a single machine scenario, when the analysis is run and implemented on a single processing node, as it seems to be a good fit for the current software development methodologies. We argue that in some cases it is reasonable to employ high performance computing (HPC) to do software analysis, if the performance impact is worth the increase in computational requirements. In this paper we present our experience with the implementation of a HPC version of the bounded model checker Borealis, major problems we encountered together with their solutions, and the evaluation results on a number of different real-world projects.

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
next chapter Predicate Abstraction Based Configurable Method for Data Race Detection in Linux Kernel
Footnotes
1
Result of one SMT query may make other SMT queries redundant, e.g., these queries correspond to the same error on different loop iterations.
 
2
The pass management system of LLVM 3.5.1 does not allow one to rerun a subset of passes on a module without re-running all their dependencies.
 
3
A machine with Intel Core i7-4790 3.6 GHz processor, 32 GB of RAM and Intel 535 SSD storage.
 
Literature
1.
Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O’Hearn, P., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). https://​doi.​org/​10.​1007/​978-3-319-17524-9_​1
2.
Ayewah, N., Hovemeyer, D., Davidmorgenthaler, J., Penix, J., Pugh, W.: Experiences using static analysis to find bugs. IEEE Softw. 25, 22–29 (2008)CrossRef
3.
Akhin, M., Belyaev, M., Itsykson, V.: Software defect detection by combining bounded model checking and approximations of functions. Autom. Control Comput. Sci. 48(7), 389–397 (2014)CrossRef
4.
Akhin, M., Belyaev, M., Itsykson, V.: Borealis bounded model checker: the coming of age story. In: Meyer, B., Mazzara, M. (eds.) PAUSE: Present And Ulterior Software Engineering. Springer, Cham (2017)
5.
6.
7.
Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO 2004, pp. 75–86 (2004)
8.
9.
Karger, D., Lehman, E., Leighton, T., Panigrahy, R., Levine, M., Lewin, D.: Consistent hashing and random trees: distributed caching protocols for relieving hot spots on the world wide web. In: STOC 1997, pp. 654–663 (1997)
10.
Lusk, E., Huss, S., Saphir, B., Snir, M.: MPI: A message-passing interface standard, 4 June 2015 (2015)
11.
Artemiev, S.S., Korneev, V.D.: Numerical solution of stochastic differential equations on supercomputers. Numer. Anal. Appl. 4(1), 1–11 (2011)CrossRef
12.
Zhukovskii, M.E., Uskov, R.V.: Hybrid paralleling of the algorithms of radiation cascade transport modelling. Matematicheskoe Modelirovanie 27(5), 39–51 (2015)MATH
13.
Szpakowski, A., Pustelny, T.: Parallel implementation of the concurrent algorithm for acoustic field distribution calculating in heterogeneous HPC environment. J. Phys. IV (Proc.) 137, 153–156 (2006). EDP Sciences
14.
Avdyushenko, A.Y., Cherny, S.G., Astrakova, A.S., Chirkov, D.V., Lyutov, A.: High-perfomance computations in problems of simulation and optimization of turbine hydrodynamics (2013)
15.
Getmanskiy, V.V., Gorobtsov, A.S., Ismailov, T.D., Andreev, A.E.: Heuristic method of dynamic stress analysis in multibody simulation using HPC. In: WCCM’XI, pp. 3115–3124 (2014)
16.
Teplukhin, A.V.: Parallel and distributed computing in problems of supercomputer simulation of molecular liquids by the Monte Carlo method. J. Struct. Chem. 54(1), 65–74 (2013)CrossRef
17.
Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the Saturn project. In: PASTE 2007, pp. 43–48 (2007)
18.
19.
Garavel, H., Mateescu, R., Bergamini, D., Curic, A., Descoubes, N., Joubert, C., Smarandache-Sturm, I., Stragier, G.: DISTRIBUTOR and BCG_MERGE: tools for distributed explicit state space generation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 445–449. Springer, Heidelberg (2006). https://​doi.​org/​10.​1007/​11691372_​30 CrossRef
Metadata
Title
Distributed Analysis of the BMC Kind: Making It Fit the Tornado Supercomputer
Authors
Azat Abdullin
Daniil Stepanov
Marat Akhin
Copyright Year
2018
Book
Tools and Methods of Program Analysis

Print ISBN: 978-3-319-71733-3

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

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-319-71734-0_1

Premium Partner

    Image Credits