SymInfer
ThanhVu H. Nguyen, KimHao Nguyen, Hai Duong · 2022
We demonstrate the implementation and usage of SymInfer, a tool that automatically discovers numerical invariants using concrete and symbolic states collected from dynamic and symbolic executions. SymInfer supports expressive invariants under various forms, including nonlinear equalities, octagonal inequalities, and disjunctive min/max invariants. Experimental results show that SymInfer is effective in generating complex invariants and can often discover unknown, yet useful program properties. Video demo: https://www.youtube.com/watch?v=VEuhJw1RBUE.