Author: Harmim Dominik, Bc. xharmi00@stud.fit.vutbr.cz
Supervisor: Vojnar Tomáš, prof. Ing. Ph.D. (UITS FIT VUT) vojnar@fit.vutbr.cz
Reviewer: Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT) rogalew@fit.vut.cz
- Study limitations of the atomicity analyser Atomer developed in your bachelor thesis as well as the latest developments concerning the Facebook Infer framework.
- Propose ways of significantly improving precision and/or scalability of the analysis even if for the price of the user providing more input and/or combining it with dynamic analysis.
- Implement a new version of Atomer including the proposed improvements and supporting analysis of programs written in more programming languages than just C supported by the first version of Atomer.
- Evaluate the new version of Atomer on suitable benchmarks, including at least real-life code in which some atomicity problems were previously detected.
- Describe and discuss the achieved results and their further possible improvements.
Implementation language: OCaml
Free software: Facebook Infer
- Rival, X., Yi, K.: Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press, 2020.
- Blackshear, S., Gorogiannis, N., O'Hearn, P. W., Sergey, I.: RacerD: Compositional Static Race Detection. In: Proc. of OOPSLA'18, PACMPL 2(OOPSLA):144:1-144:28, 2018.
- Gorogiannis, N., O'Hearn, P.W., Sergey, I.: A True Positives Theorem for a Static Race Detector. In: Proc. of POPL'19, PACMPL 3(POPL):57:1-57:29, 2019.
- Dias, R.J., Ferreira, C., Fiedor, J., Lourenço, J.M., Smrčka, A., Sousa, D.G., Vojnar, T.: Verifying Concurrent Programs Using Contracts, In: Proc. of ICST'17, IEEE, 2017.
- Harmim, D.: Static Analysis Using Facebook Infer to Find Atomicity Violations. Bachelor thesis, Brno University of Technology, 2019.
- Marcin, V.: Static Analysis Using Facebook Infer Focused on Deadlock Detection. Bachelor thesis, Brno University of Technology, 2019.
The implementation is in the repository harmim/infer. It is a fork of the repository facebook/infer. It is implemented under the branch atomicity-sets, see the diff.
More information about the tool, including examples, installation and usage instructions are available at the Wiki.
- Facebook Infer
- Facebook Infer repository
- OCaml
- Patrick Cousot - Abstract Interpretation
- Patrick Cousot - Abstract Interpretation in a Nutshell
- Facebook Infer lab
- Facebook Infer talk
- Facebook Infer INSTALL.md
- Facebook Infer CONTRIBUTING.md
- Open-sourcing RacerD: Fast static race detection at scale
- ThreadSafe: Static Analysis for Java Concurrency
- ThreadSafe: Static Analysis for Java Concurrency - benchmark
- Gluon
- Gluon - validation examples
- VeriFIT Static Analysis Plugins
- ANaConDA Framework
- Apache Cassandra repository
- Apache Cassandra - reported bugs
- Apache Tomcat repository
- Apache Tomcat - reported bugs
- Inferbo: Infer-based buffer overrun analyzer