Generating Invariant-Based Certificates for Embedded Systems

摘要: Automatic verification tools, such as model checkers and tools based on static analysis or abstract interpretation, have become popular in software hardware development. They increase confidence potentially provide rich feedback. However, with increasing complexity, themselves are more likely to contain errors.In contrast automatic higher-order theorem provers use mathematically founded proof strategies checked by a small checker guarantee selected properties. Thus, they enjoy high level of trustability. Properties systems their justifications can be encapsulated into certificate, thereby guaranteeing correctness the systems, respect These results offer much higher degree than achieved tools. usually slow, due general minimalistic nature. Even for lot human interaction is required establishing certificate.In this work, we combine advantages (i.e., speed automation) those trustability). The tool generates certificate each invocation. This prover, desired property. generation certificates easier producing first place. In our able create that come an algorithmic description property justification. We concentrate generate invariants certify automatically these do indeed hold. Our approach applied certification verdicts deadlock-detection asynchronous component-based language.