Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Symbolic Detection of Assertion Dependencies for Bounded Model Checking
verfasst von : Grigory Fedyukovich, Andrea Callia D’Iddio, Antti E. J. Hyvärinen, Natasha Sharygina
Erschienen in: Fundamental Approaches to Software Engineering
Verlag: Springer Berlin Heidelberg
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
Automatically generating assertions through static or runtime analysis is becoming an increasingly important initial phase in many software testing and verification tool chains. The analyses may generate thousands of redundant assertions often causing problems later in the chain, including scalability issues for automatic tools or a prohibitively large amount of information for final processing. We present an algorithm which uses a SAT solver on a bounded symbolic encoding of the program to reveal the implication relationships among spatially close assertions for use in a variety of bounded model checking applications. Our experimentation with different applications demonstrates that this technique can be used to reduce the number of assertions that need to be checked thus improving overall performance.