Symbolic Detection of Assertion Dependencies for Bounded Model Checking
| Autor: | Antti E. J. Hyvärinen, Andrea Callia D'Iddio, Natasha Sharygina, Grigory Fedyukovich |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
Model checking
Theoretical computer science Dependency relation Computer science Programming language Assertion 020207 software engineering 02 engineering and technology computer.software_genre 020202 computer hardware & architecture Bounded function Encoding (memory) Scalability Symbolic trajectory evaluation 0202 electrical engineering electronic engineering information engineering Boolean satisfiability problem computer |
| Zdroj: | Fundamental Approaches to Software Engineering ISBN: 9783662466742 FASE |
| DOI: | 10.1007/978-3-662-46675-9_13 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|