Automated Invariant Generation for Efficient Deductive Reasoning About Embedded Systems

Deductive verification is often more efficient than alternative techniques like model checking at reasoning about functional properties of programs. This is especially true when the program under verification contains very large or unbounded data ranges that model checkers struggle with. However, modular deductive verifiers struggle with verifying global properties, which are often crucial in concurrent and reactive embedded systems. Embedded systems often require complex user-defined invariants to capture the global state for the verification of local annotations, demanding high effort and expertise from the user. In this paper, we propose a method to automatically generate compact invariants that are sufficiently strong to enable effective deductive verification of global properties in embedded systems. Our key idea is that a good level of abstraction can be found automatically by choosing variables for refinement that influence relevant events and process interactions. We use this idea together with abstract interpretation to build a system’s state space, abstracted to the relevant part for a given global property. We demonstrate the effectiveness of our approach on a SystemC design of an automotive control system that has in the past proved challenging to verify.