2019/04/04 by Mikhail Y. R. Gadelha, Gadelha, Mikhail R., Felipe R. Monteiro +7
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Software Reliability and Analysis Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1904.02501
openalex publication_date 2019/04/04 · openalex created_date 2019/04/11 · openalex updated_date 2026/07/28
We describe and evaluate a novel k-induction proof rule called bidirectional k-induction (bkind), which substantially improves the k-induction bug-finding capabilities. Particularly, bkind exploits the counterexamples generated by the over-approximation step to derive new properties and feed them back to the bounded model checking procedure. We also combine an interval invariant generator and bkind to significantly improve the number of correct verification results. Experimental results show that bkind can considerably reduce the verification time compared to the naive k-induction proof rule, since it only requires half the number of steps to find a given safety property violation in an unsafe program. The bkind algorithm outperforms 2LS, another state-of-the-art k-induction verifier, and produces more than twice correct proofs and about 35% more correct alarms than when analysing a large set of public available benchmarks.