Trustworthy Systems

Perentie: Modular trace refinement and selective value tracking

Authors

Franck Cassez, Takashi Matsuoka, Ed Pierzchalski and Nathan Smyth

NICTA

Abstract

Perentie is a software analysis tool based on iterative refinement of trace abstraction: if the refinement process terminates, the program is either declared correct or a counter-example is provided and the program is incorrect. As the iterative refinement process may not terminate, Perentie limits the number of iterations of the refinement phase. If it is inconclusive, it starts a second, more precise refinement analysis, where it tracks the values of some variables. If this second phase is inconclusive as well then the overall analysis is inconclusive, otherwise the status of the program is determined.

BibTeX Entry

  @inproceedings{Cassez_MPS_15,
    address          = {London, UK},
    author           = {Cassez, Franck and Matsuoka, Takashi and Pierzchalski, Edward and Smyth, Nathan},
    booktitle        = {SV-COMP-2015},
    doi              = {10.1007/978-3-662-46681-0_39},
    editor           = {{Christel Baier, Cesare Tinelli }},
    keywords         = {software verification, smt solving},
    month            = apr,
    pages            = {439--442},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8403.pdf},
    publisher        = {Springer},
    title            = {Perentie: Modular Trace Refinement and Selective Value Tracking},
    year             = {2015}
  }

Download