M. Kwiatkowska,
G. Norman,
and D. Parker.
Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata.
In Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday,
volume 10460 of LNCS,
pages 289-309,
2017.
Springer.
Keyword(s): model checking,
probability.
@inproceedings{kwiatkowskaSymbolicVerificationStrategy2017,
title = {Symbolic {{Verification}} and {{Strategy Synthesis}} for {{Linearly}}-{{Priced Probabilistic Timed Automata}}},
booktitle = {Models, {{Algorithms}}, {{Logics}} and {{Tools}}: {{Essays Dedicated}} to {{Kim Guldstrand Larsen}} on the {{Occasion}} of {{His}} 60th {{Birthday}}},
author = {Kwiatkowska, M. and Norman, G. and Parker, D.},
year = {2017},
volume = {10460},
pages = {289--309},
publisher = {{Springer}},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4355-Kwiatkowska et al (2017) - Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic.pdf},
keywords = {model checking,probability},
series = {{{LNCS}}}
}
Gagandeep Singh,
Markus Püschel,
and Martin Vechev.
Fast Polyhedra Abstract Domain.
In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages,
POPL 2017,
New York, NY, USA,
pages 46-59,
2017.
ACM.
ISBN: 978-1-4503-4660-3.
Keyword(s): abstract interpretation.
Abstract: |
Numerical abstract domains are an important ingredient of modern static analyzers used for verifying critical program properties (e.g., absence of buffer overflow or memory safety). Among the many numerical domains introduced over the years, Polyhedra is the most expressive one, but also the most expensive: it has worst-case exponential space and time complexity. As a consequence, static analysis with the Polyhedra domain is thought to be impractical when applied to large scale, real world programs. In this paper, we present a new approach and a complete implementation for speeding up Polyhedra domain analysis. Our approach does not lose precision, and for many practical cases, is orders of magnitude faster than state-of-the-art solutions. The key insight underlying our work is that polyhedra arising during analysis can usually be kept decomposed, thus considerably reducing the overall complexity. We first present the theory underlying our approach, which identifies the interaction between partitions of variables and domain operators. Based on the theory we develop new algorithms for these operators that work with decomposed polyhedra. We implemented these algorithms using the same interface as existing libraries, thus enabling static analyzers to use our implementation with little effort. In our evaluation, we analyze large benchmarks from the popular software verification competition, including Linux device drivers with over 50K lines of code. Our experimental results demonstrate massive gains in both space and time: we show end-to-end speedups of two to five orders of magnitude compared to state-of-the-art Polyhedra implementations as well as significant memory gains, on all larger benchmarks. In fact, in many cases our analysis terminates in seconds where prior code runs out of memory or times out after 4 hours. We believe this work is an important step in making the Polyhedra abstract domain both feasible and practically usable for handling large, real-world programs. |
@inproceedings{singhFastPolyhedraAbstract2017,
title = {Fast {{Polyhedra Abstract Domain}}},
booktitle = {Proceedings of the 44th {{ACM SIGPLAN Symposium}} on {{Principles}} of {{Programming Languages}}},
author = {Singh, Gagandeep and P{\"u}schel, Markus and Vechev, Martin},
year = {2017},
pages = {46--59},
publisher = {{ACM}},
address = {{New York, NY, USA}},
doi = {10.1145/3009837.3009885},
abstract = {Numerical abstract domains are an important ingredient of modern static analyzers used for verifying critical program properties (e.g., absence of buffer overflow or memory safety). Among the many numerical domains introduced over the years, Polyhedra is the most expressive one, but also the most expensive: it has worst-case exponential space and time complexity. As a consequence, static analysis with the Polyhedra domain is thought to be impractical when applied to large scale, real world programs. In this paper, we present a new approach and a complete implementation for speeding up Polyhedra domain analysis. Our approach does not lose precision, and for many practical cases, is orders of magnitude faster than state-of-the-art solutions. The key insight underlying our work is that polyhedra arising during analysis can usually be kept decomposed, thus considerably reducing the overall complexity. We first present the theory underlying our approach, which identifies the interaction between partitions of variables and domain operators. Based on the theory we develop new algorithms for these operators that work with decomposed polyhedra. We implemented these algorithms using the same interface as existing libraries, thus enabling static analyzers to use our implementation with little effort. In our evaluation, we analyze large benchmarks from the popular software verification competition, including Linux device drivers with over 50K lines of code. Our experimental results demonstrate massive gains in both space and time: we show end-to-end speedups of two to five orders of magnitude compared to state-of-the-art Polyhedra implementations as well as significant memory gains, on all larger benchmarks. In fact, in many cases our analysis terminates in seconds where prior code runs out of memory or times out after 4 hours. We believe this work is an important step in making the Polyhedra abstract domain both feasible and practically usable for handling large, real-world programs.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/2598-Singh et al (2017) - Fast Polyhedra Abstract Domain.pdf},
isbn = {978-1-4503-4660-3},
series = {{{POPL}} 2017},
keywords = {abstract interpretation}
}