Verimag

bibtex

@inproceedings{KMW16a,
    title = { Program Analysis with Local Policy Iteration },
    author = {Karpenkov, Egor George and Monniaux, David and Wendler, Philipp},
    year = {2016},
    booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
    eprint = {1509.03424},
    pages = {127--146},
    publisher = {Springer},
    series = {LNCS},
    volume = {9583},
    team = {PACSS},
    timestamp = {Tue, 05 Jan 2016 12:40:34 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/KarpenkovMW16}, bibsource = {dblp computer science bibliography, http://dblp.org}, eprinttype = {arXiv},
    abstract = {We present a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis (CPA) framework, thus allowing inter-analysis communication. It uses adjustable-block encoding in order to traverse loop-free program sections, possibly containing branching, without introducing extra abstraction. Our technique operates over any template linear constraint domain, including the interval and octagon domains; templates can also be derived from the program source. The implementation is evaluated on a set of benchmarks from the Software Verification Competition (SV-Comp). It competes favorably with state-of-the-art analyzers.},
}

URL

Publication Sections


Contact | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 912776