Skip to content
/ vut-ibt Public

Bachelor's Thesis - Static Analysis Using Facebook Infer to Find Atomicity Violations

License

Notifications You must be signed in to change notification settings

harmim/vut-ibt

Repository files navigation

Bachelor's Thesis

Static Analysis Using Facebook Infer to Find Atomicity Violations


Bakalářská práce

Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti


Author: Dominik Harmim [email protected]
Specification:
  1. Prostudujte principy statické analýzy založené na abstraktní interpretaci. Zvláštní pozornost věnujte přístupům zaměřeným na odhalování problémů v synchronizaci paralelních procesů.
  2. Seznamte se s nástrojem Facebook Infer, jeho podporou pro abstraktní interpretaci a s existujícímí analyzátory vytvořenými v prostředí Faceboook Infer.
  3. V prostředí Facebook Infer navrhněte a naimplementujte analyzátor zaměřený na odhalování chyb typu porušení atomicity.
  4. Experimentálně ověřte funkčnost vytvořeného analyzátoru na vhodně zvolených netriviálních programech.
  5. Shrňte dosažené výsledky a diskutujte možnosti jejich dalšího rozvoje v budoucnu.
Category: Software analysis and testing
Implementation language: OCaml
Free software: Facebook Infer
Literature:
  • Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
  • Blackshear, S., O'Hearn, P.: Open-Sourcing RacerD: Fast Static Race Detection at Scale, 2017. Dostupné on-line: https://code.fb.com/android/open-sourcing-racerd-fast-static-race-detection-at-scale.
  • Atkey, R., Sannella, D.: ThreadSafe: Static Analysis for Java Concurrency, Electronic Communications of the EASST, 72, 2015. Dostupné on-line: https://bentnib.org/threadsafe.html.
  • Bielik, P., Raychev, V., Vechev, M.T.: Scalable Race Detection for Android Applications, In: Proc. of OOPSLA'15, ACM, 2015.
  • 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.

Implementation

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.

Wiki

More information about the product, including examples, installation, and usage are available at the Wiki.

Useful links: