HiFrog: SMT-based Function Summarization for Software Verification
TACAS, pp. 207-213, 2017.
Function summarization can be used as a means of incremental verification based on the structure of the program. HiFrog is a fully featured function-summarization-based model checker that uses SMT as the modeling and summarization language. The tool supports three encoding precisions through SMT: uninterpreted functions, linear real arith...More
Full Text (Upload PDF)
PPT (Upload PPT)