2015/09/08 by Herbert Rocha, Rocha, Herbert, Hussama Ismail +5 · 1 citation
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Radiation Effects in Electronics #Real-time simulation and control systems #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.1509.02471
openalex publication_date 2015/09/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a proof by induction algorithm, which combines k-induction with invariants to model check embedded C software with bounded and unbounded loops. The k-induction algorithm consists of three cases: in the base case, we aim to find a counterexample with up to k loop unwindings; in the forward condition, we check whether loops have been fully unrolled and that the safety property P holds in all states reachable within k unwindings; and in the inductive step, we check that whenever P holds for k unwindings, it also holds after the next unwinding of the system. For each step of the k-induction algorithm, we infer invariants using affine constraints (i.e., polyhedral) to specify pre- and post-conditions. Experimental results show that our approach can handle a wide variety of safety properties in typical embedded software applications from telecommunications, control systems, and medical devices; we demonstrate an improvement of the induction algorithm effectiveness if compared to other approaches.