AISE: A Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution)

Abstract

Abstract is a static verifier that can verify the safety properties of C programs. The core of is a program verification framework that synergizes abstract interpretation and symbolic execution in a novel manner. Compared to the individual application of symbolic execution or abstract interpretation, has better efficiency and precision. The implementation of is based on and .