English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

There are several approaches of using automated theorem provers and assistants in hardware verification. It has been shown, that hardware behavior can be modelled and verified using theorem proving tools. But the task of generating a proof remains difficult and often needs a big amount of interaction. Therefore, the methods of our hardware verification system VERENA are based on term rewriting. It is shown how we use the expressive power of type theory to model circuit behavior. The crucial point in implementing a term rewriting system is to guarantee that the term rewriting rules used have specific properties like correctness, confluence, completeness, etc. It is demonstrated how we use the HOL prove assistant to prove the correctness of term rewriting rules.

Using the HOL prove assistant for proving the correctness of term rewriting rules reducing terms of sequential behavior