2 papers
cs.CR2021
Verifying Security Vulnerabilities in Large Software Systems using Multi-Core k-Induction
Thales Silva, Carmina Porto, Erickson Alves +2
Computer-based systems have been used to solve several domain problems, such as industrial, military, education, and wearable. Those systems need high-quality software to guarantee…
cs.LO2015
Model Checking C Programs with Loops via k-Induction and Invariants
Herbert Rocha, Hussama Ismail, Lucas Cordeiro +1
We present a novel proof by induction algorithm, which combines k-induction with invariants to model check C programs with bounded and unbounded loops. The k-induction algorithm co…