Deductive Verification of Parameterized Embedded Systems Modeled in SystemC

Explore a conference talk that delves into a novel approach for deductive verification of parameterized embedded systems modeled in SystemC. Learn about the challenges of verifying global safety properties in embedded systems and how the presenters address these issues. Discover a formal encoding and automated transformation method for SystemC designs, enabling verification with the VerCors deductive verifier. Understand the innovative technique for invariant construction that allows for abstract capture of global dependencies, facilitating local reasoning about global properties with reduced manual effort. Examine the application of this approach through three parameterized case studies, including an automotive control system, demonstrating its practical utility in real-world scenarios.

[VMCAI'24] Deductive Verification of Parameterized Embedded Systems modeled in SystemC