title = { A tool for symbolic program verification and abstraction },
    author = {Graf, Susanne and Loiseaux, Claire},
    year = {1993},
    booktitle = {Conference on Computer Aided Verification CAV 93, Heraklion Crete},
    publisher = {Springer Verlag},
    series = {LNCS},
    volume = {697},
    team = {DCS},
    abstract = {We give the description of a verification tool taking boolean programs of guarded commands as input; internal representation of programs are sets of Binary Decision Diagrams (BDD) (one for each guarded command). It allows to construct an abstract program of the same form obtained using an abstraction relation given by a boolean expression on ``concrete\'\' and ``abstract\'\' variables. The tool allows the verification of CTL formulas on programs. We illustrate its possibilities on an example. },


Publication Sections

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

info visites 872937