Safe and Sound Program Analysis with Flix

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

DOI

Program development tools such as bug finders, build automation tools, compilers, debuggers, integrated development environments, and refactoring tools increasingly rely on static analysis techniques to reason about program behavior. Implementing such static analysis tools is a complex and difficult task with concerns about safety and soundness. Safety guarantees that the fixed point computation - inherent in most static analyses - converges and ultimately terminates with a deterministic result. Soundness guarantees that the computed result over-approximates the concrete behavior of the program under analysis. But how do we know if we can trust the result of the static analysis itself? Who will guard the guards? In this paper, we propose the use of automatic program verification techniques based on symbolic execution and SMT solvers to verify the correctness of the abstract domains used in static analysis tools. We implement a verification toolchain for Flix, a functional and logic programming language tailored for the implementation of static analyses.We apply this toolchain to several abstract domains. The experimental results show that we are able to prove 99.5% and 96.3% of the required safety and soundness properties, respectively.

Original languageEnglish
Title of host publicationISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis
EditorsEric Bodden, Frank Tip
Number of pages11
Place of publicationNew York, NY, USA
PublisherAssociation for Computing Machinery
Publication year12 Jul 2018
Pages38-48
ISBN (print)978-1-4503-5699-2
ISBN (Electronic)9781450356992
DOIs
Publication statusPublished - 12 Jul 2018
Externally publishedYes
EventACM SIGSOFT International Symposium on Software Testing and Analysis - Amsterdam, Netherlands
Duration: 15 Jul 201821 Jul 2018
Conference number: 27
https://conf.researchr.org/home/issta-2018

Conference

ConferenceACM SIGSOFT International Symposium on Software Testing and Analysis
Nummer27
LandNetherlands
ByAmsterdam
Periode15/07/201821/07/2018
Internetadresse
SeriesISSTA 2018

    Research areas

  • Lattices, Monotonicity, Safety, Soundness, Static analysis

See relations at Aarhus University Citationformats

ID: 138359976