Safe and Sound Program Analysis with Flix

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

Standard

Safe and Sound Program Analysis with Flix. / Madsen, Magnus; Lhoták, Ondrej.

ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. ed. / Eric Bodden; Frank Tip. New York, NY, USA : Association for Computing Machinery, 2018. p. 38-48 (ISSTA 2018).

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

Harvard

Madsen, M & Lhoták, O 2018, Safe and Sound Program Analysis with Flix. in E Bodden & F Tip (eds), ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. Association for Computing Machinery, New York, NY, USA, ISSTA 2018, pp. 38-48, Amsterdam, Netherlands, 15/07/2018. https://doi.org/10.1145/3213846.3213847

APA

Madsen, M., & Lhoták, O. (2018). Safe and Sound Program Analysis with Flix. In E. Bodden, & F. Tip (Eds.), ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 38-48). New York, NY, USA: Association for Computing Machinery. ISSTA 2018 https://doi.org/10.1145/3213846.3213847

CBE

Madsen M, Lhoták O. 2018. Safe and Sound Program Analysis with Flix. Bodden E, Tip F, editors. In ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York, NY, USA: Association for Computing Machinery. pp. 38-48. (ISSTA 2018). https://doi.org/10.1145/3213846.3213847

MLA

Madsen, Magnus and Ondrej Lhoták "Safe and Sound Program Analysis with Flix". and Bodden, Eric Tip, Frank (editors). ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York, NY, USA: Association for Computing Machinery. (ISSTA 2018). 2018, 38-48. https://doi.org/10.1145/3213846.3213847

Vancouver

Madsen M, Lhoták O. Safe and Sound Program Analysis with Flix. In Bodden E, Tip F, editors, ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York, NY, USA: Association for Computing Machinery. 2018. p. 38-48. (ISSTA 2018). https://doi.org/10.1145/3213846.3213847

Author

Madsen, Magnus ; Lhoták, Ondrej. / Safe and Sound Program Analysis with Flix. ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. editor / Eric Bodden ; Frank Tip. New York, NY, USA : Association for Computing Machinery, 2018. pp. 38-48 (ISSTA 2018).

Bibtex

@inproceedings{315e9ea53da449268b9167a95407d133,
title = "Safe and Sound Program Analysis with Flix",
abstract = "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.",
keywords = "lattices, monotonicity, safety, soundness, static analysis, Lattices, Monotonicity, Safety, Soundness, Static analysis",
author = "Magnus Madsen and Ondrej Lhot{\'a}k",
year = "2018",
month = "7",
day = "12",
doi = "10.1145/3213846.3213847",
language = "English",
isbn = "978-1-4503-5699-2",
pages = "38--48",
editor = "Eric Bodden and Frank Tip",
booktitle = "ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis",
publisher = "Association for Computing Machinery",

}

RIS

TY - GEN

T1 - Safe and Sound Program Analysis with Flix

AU - Madsen, Magnus

AU - Lhoták, Ondrej

PY - 2018/7/12

Y1 - 2018/7/12

N2 - 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.

AB - 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.

KW - lattices, monotonicity, safety, soundness, static analysis

KW - Lattices

KW - Monotonicity

KW - Safety

KW - Soundness

KW - Static analysis

U2 - 10.1145/3213846.3213847

DO - 10.1145/3213846.3213847

M3 - Article in proceedings

SN - 978-1-4503-5699-2

SP - 38

EP - 48

BT - ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis

A2 - Bodden, Eric

A2 - Tip, Frank

PB - Association for Computing Machinery

CY - New York, NY, USA

ER -