SpringerLink
Log in

Equid—A Static Analysis Framework for Industrial Applications

  • Conference paper
  • First Online:
Computational Science and Its Applications – ICCSA 2019 (ICCSA 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11619))

Included in the following conference series:

Abstract

The rise of the software engineering industry sparkled the research on static analyzers in both academia and industry. Academic tools historically have an exhaustive feature set but don’t easily apply to industrial applications, and industrial verifiers are still very limited. The Equid project, which loosely stands for “Engine for performing queries on unified intermediate representations of program and domain models” is an attempt to fill the gap between theory and practice by building a language-agnostic analyzer in close contact with development and security community. In this introductory paper we set project goals, reveal motivation and describe code processing stages, such as preprocessing, translation to project’s own intermediate codes, virtual machine execution, constraint solving, all done to make static and interactive contract violation checks easier, more precisive yet informative. The project is compared to other analyzers. We believe that such a framework can draw attention to industrial uses clearly missed by verification communities and help shape a vision of universal static analyzer architectures.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://github.com/maximmenshikov/acsl-grammar.

References

  1. C11 Standard ISO/IEC 9899:2011. https://www.iso.org/standard/57853.html

  2. Clang: a C language family frontend for LLVM. http://clang.llvm.org

  3. Roslyn -.NET Compiler Platform. https://github.com/dotnet/roslyn

  4. SMT-COMP 2018 Results. http://smtcomp.sourceforge.net/2018/results-summary.shtml

  5. Akhin, M., Belyaev, M., Itsykson, V.: Borealis bounded model checker: the coming of age story. In: Mazzara, M., Meyer, B. (eds.) Present and Ulterior Software Engineering, pp. 119–137. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67425-4_8

    Chapter  Google Scholar 

  6. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  7. Bessey, A., et al.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66–75 (2010)

    Article  Google Scholar 

  8. 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_16

    Chapter  Google Scholar 

  9. Christakis, M., Bird, C.: What developers want and need from program analysis: an empirical study. In: 31st IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 332–343. IEEE (2016)

    Google Scholar 

  10. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  11. Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Autom. Soft. Eng. 6(1), 69–95 (1999). https://doi.org/10.1023/A:1008649901864

    Article  MATH  Google Scholar 

  12. Dillig, I., Dillig, T., Aiken, A.: SAIL: static analysis intermediate language with a two-level representation. Technical report. Stanford University (2009)

    Google Scholar 

  13. Dullien, T., Porst, S.: REIL : a platform-independent intermediate representation of disassembled code for static code analysis (2009)

    Google Scholar 

  14. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  15. Ivannikov, V., Belevantsev, A., Borodin, A., Ignatiev, V., Zhurikhin, D., Avetisyan, A.: Static analyzer Svace for finding defects in a source program code. Program Comput. Soft. 40(5), 265–275 (2014). https://doi.org/10.1134/S0361768814050041

    Article  Google Scholar 

  16. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Form. Asp. Comp. 27(3), 573–609 (2015). https://doi.org/10.1007/s00165-014-0326-7

    Article  MathSciNet  Google Scholar 

  17. Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization, p. 75c. IEEE Computer Society (2004)

    Google Scholar 

  18. McMillan, K.: Applications of craig interpolation to model checking. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 22–23. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30124-0_3

    Chapter  Google Scholar 

  19. Menshchikov, M.: Scalable semantic virtual machine framework for language-agnostic static analysis. In: Distributed Computing and Grid-technologies in Science and Education, pp. 213–217 (2018)

    Google Scholar 

  20. Menshchikov, M., Lepikhin, T.: 5W+1H static analysis report quality measure. In: Itsykson, V., Scedrov, A., Zakharov, V. (eds.) TMPA 2017. CCIS, vol. 779, pp. 114–126. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-71734-0_10

    Chapter  Google Scholar 

  21. Menshchikov, M.A., Lepikhin, T.A.: Applying MapReduce to static analysis. Control Proc. Stab. 4(1), 433–444 (2017)

    Google Scholar 

  22. Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45937-5_16

    Chapter  Google Scholar 

  23. Parr, T.: The definitive ANTLR 4 reference. Pragmatic Bookshelf (2013)

    Google Scholar 

  24. Terekhov, A.N.: Programming and compiler techniques educational tool. Comput. Tools Educ. 1, 36–47 (2016)

    Google Scholar 

  25. Terekhov, A.N., Golovan, A.A., Terekhov, M.A.: Parallel programs in RuC project. Comput. Tools Educ. 2, 25–30 (2018)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Saint Petersburg State University, 7–9, Universitetskaya nab., St. Petersburg, 199034, Russian Federation

    Maxim Menshikov

Authors
  1. Maxim Menshikov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maxim Menshikov .

Editor information

Editors and Affiliations

  1. Covenant University, Ota, Nigeria

    Sanjay Misra

  2. University of Perugia, Perugia, Italy

    Osvaldo Gervasi

  3. University of Basilicata, Potenza, Italy

    Beniamino Murgante

  4. Saint Petersburg State University, Saint Petersburg, Russia

    Elena Stankova

  5. Saint Petersburg State University, Saint Petersburg, Russia

    Vladimir Korkhov

  6. Polytechnic University of Bari, Bari, Italy

    Carmelo Torre

  7. University of Minho, Braga, Portugal

    Ana Maria A.C. Rocha

  8. Monash University, Clayton, VIC, Australia

    David Taniar

  9. Kyushu Sangyo University, Fukuoka, Japan

    Bernady O. Apduhan

  10. Polytechnic University of Bari, Bari, Italy

    Eufemia Tarantino

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Menshikov, M. (2019). Equid—A Static Analysis Framework for Industrial Applications. In: Misra, S., et al. Computational Science and Its Applications – ICCSA 2019. ICCSA 2019. Lecture Notes in Computer Science(), vol 11619. Springer, Cham. https://doi.org/10.1007/978-3-030-24289-3_50

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-24289-3_50

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-24288-6

  • Online ISBN: 978-3-030-24289-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation