Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Necessary and Sufficient Preconditions via Eager Abstraction
verfasst von : Mohamed Nassim Seghir, Peter Schrammel
Erschienen in: Programming Languages and Systems
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The precondition for safe execution of a procedure is useful for understanding, verifying and debugging programs. We have previously presented a cegar-based approach for inferring necessary and sufficient preconditions based on the iterative abstraction-refinement of the set of safe and unsafe states until they become disjoint. A drawback of that approach is that safe and unsafe traces are explored separately and each time they are built entirely before being checked for consistency. In this paper, we present an
eager
approach that explores shared prefixes between safe and unsafe traces conjointly. As a result, individual state sets, by construction, fulfil the property of separation between safe and unsafe states without requiring any refinement. Experiments using our implementation of this technique in the precondition generator P-Gen show a significant improvement compared to our previous cegar-based method. In some cases the running time drops from several minutes to several seconds.