Advertisement

Statistical Model Checking of LLVM Code

  • Axel Legay
  • Dirk Nowotka
  • Danny Bøgsted Poulsen
  • Louis-Marie Tranouez
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

We present the new tool Lodin for statistical model checking of LLVM-bitcode. Lodin implements a simulation engine for LLVM-bitcode and implements classic statistical model checking algorithms on top of it. The simulation engine implements only the core of LLVM but supports extending this core through a plugin-architecture. Besides the statistical model checking algorithms Lodin also provides an interactive simulation front-end. The simulator front-end was integral for our second contribution - an integration of Lodin into Plasma-Lab. The integration with Plasma-Lab is integral to allow reasoning about rare properties of programs.

References

  1. 1.
    AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22944-2_28CrossRefGoogle Scholar
  2. 2.
    Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: QEST, pp. 143–144. IEEE Computer Society (2011).  https://doi.org/10.1109/QEST.2011.24. ISBN 978-1-4577-0973-9
  3. 3.
    Barnat, J., Brim, L., Rockai, P.: Towards LTL model checking of unmodified thread-based C & C++ programs. In: Goodloe, A., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 252–266. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28891-3_25CrossRefGoogle Scholar
  4. 4.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_16CrossRefGoogle Scholar
  5. 5.
    Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160–164. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  6. 6.
    Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed automata. In: Wiklicky, H., Massink, M. (eds.) QAPL. EPTCS, vol. 85, pp. 1–16 (2012).  https://doi.org/10.4204/EPTCS.85.1CrossRefGoogle Scholar
  7. 7.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  8. 8.
    Clopper, C.J., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404–413 (1934)CrossRefGoogle Scholar
  9. 9.
    Jegourel, C., Legay, A., Sedwards, S.: An effective heuristic for adaptive importance splitting in statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 143–159. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-45231-8_11CrossRefGoogle Scholar
  10. 10.
    Jegourel, C., Legay, A., Sedwards, S., Traonouez, L.-M.: Distributed verification of rare properties using importance splitting observers. In: ECEASST, vol. 72 (2015)Google Scholar
  11. 11.
    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  12. 12.
    Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO 2004), Palo Alto, California, March 2004Google Scholar
  13. 13.
    Legay, A., Sedwards, S., Traonouez, L.M.: Plasma lab: a modular statistical model checking platform. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 77–93. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47166-2_6CrossRefGoogle Scholar
  14. 14.
    Legay, A., Nowotka, D., Tranoues, L.-M., Poulsen, D.B.: Lodin and Plasma-Lab examples (2018). https://spark.informatik.uni-kiel.de/data/lodin/FM18/LodinExamples.zip. Accessed 08 May 2018
  15. 15.
    Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST, pp. 251–252. IEEE Computer Society (2005).  https://doi.org/10.1109/QEST.2005.42. ISBN 0-7695-2427-3
  16. 16.
    Younes, H.L.S.: Ymer: a statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_43CrossRefGoogle Scholar
  17. 17.
    Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216–228 (2006)CrossRefGoogle Scholar
  18. 18.
    Zaks, A., Joshi, R.: Verifying multi-threaded C programs with SPIN. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) Model Checking Software SPIN 2008. LNCS, vol. 5156, pp. 325–342. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85114-1_22CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Axel Legay
    • 1
  • Dirk Nowotka
    • 2
  • Danny Bøgsted Poulsen
    • 2
  • Louis-Marie Tranouez
    • 1
  1. 1.InriaRennesFrance
  2. 2.Kiel UniversityKielGermany

Personalised recommendations