title = { Modular Abstractions of Reactive Nodes using Disjunctive Invariants },
    author = {Monniaux, David and Bodin, Martin},
    year = {2011},
    booktitle = {Programming Languages and Systems (APLAS)},
    team = {SYNC,PACSS},
    abstract = {We wish to abstract nodes in a reactive programming language, such as Lustre, into nodes with a simpler control structure, with a bound on the number of control states. In order to do so, we compute disjunctive invariants in predicate abstraction, with a bounded number of disjuncts, then we abstract the node, each disjunct representing an abstract state. The computation of the disjunctive invariant is performed by a form of quantifier elimination expressed using SMT-solving. The same method can also be used to obtain disjunctive loop invariants. },



Publication Sections

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

info visites 818897