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

Generalised Symbolic Trajectory Evaluation (GSTE) is a high-capacity formalverification technique for hardware. GSTE uses abstraction, meaning thatdetails of the circuit behaviour are removed from the circuit model. Asemantics for GSTE can be used to predict and understand why certain circuitproperties can or cannot be proven by GSTE. Several semantics have beendescribed for GSTE. These semantics, however, are not faithful to the provingpower of GSTE-algorithms, that is, the GSTE-algorithms are incomplete withrespect to the semantics.  The abstraction used in GSTE makes it hard to understand why a specificproperty can, or cannot, be proven by GSTE. The semantics mentioned abovecannot help the user in doing so. The contribution of this paper is a faithfulsemantics for GSTE. That is, we give a simple formal theory that deems aproperty to be true if-and-only-if the property can be proven by a GSTE-modelchecker. We prove that the GSTE algorithm is sound and complete with respect tothis semantics.

A Faithful Semantics for Generalised Symbolic Trajectory Evaluation