arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 0810.3332

A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices

Cezara Dragoi·Gheorghe Stefanescu
View original source ↗Read source document ↗Export metadata ↓

Abstract

Interactive systems with registers and voices (shortly, "rv-systems") are a model for interactive computing obtained closing register machines with respect to a space-time duality transformation ("voices" are the time-dual counterparts of "registers"). In the same vain, AGAPIA v0.1, a structured programming language for rv-systems, is the space-time dual closure of classical while programs (over a specific type of data). Typical AGAPIA programs describe open processes located at various sites and having their temporal windows of adequate reaction to the environment. The language naturally supports process migration, structured interaction, and deployment of components on heterogeneous machines. In this paper a sound Hoare-like spatio-temporal logic for the verification of AGAPIA v0.1 programs is introduced. As a case study, a formal verification proof of a popular distributed termination detection protocol is presented.

Explore related subjects

cs.PLcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Cezara Dragoi, Gheorghe Stefanescu. 2008-10-19. A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices. https://arxiv.org/abs/0810.3332

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Equality saturation theory exploration `a la carte

Rewrite rules are critical in equality saturation, an increasingly popular technique in optimizing compilers, synthesizers, and verifiers. Unfortunately, developing high-quality rulesets is difficult and error-prone. Recent work to automatically infer rewrite rules does not scale to large terms or grammars. Users struggle to guide inference and incrementally construct rulesets because existing rule inference tools are monolithic and opaque. As a result, most equality saturation users still manually develop and maintain rulesets. This paper proposes Enumo, a new domain-specific language for programmable theory exploration. Enumo provides a small set of core operators that enable users to strategically guide rule inference and incrementally build rulesets. Short Enumo programs easily replicate results from state-of-the-art tools like Ruler, but Enumo programs can also scale to infer deeper rules from larger grammars than prior approaches. Enumo's composable operators even facilitate developing new strategies for ruleset inference. We introduce a new fast-forwarding strategy which does not require evaluating terms in the target language, and thus supports domains that were out of scope for prior work. Enumo is also easy to extend: two new operators suffice to incorporate large language models into rule inference, where they complement guided search. We evaluate Enumo and fast-forwarding across a variety of domains. Compared to state-of-the-art techniques, Enumo can synthesize better rulesets over a diverse set of domains, in some cases matching the effects of manually developed rulesets in systems driven by equality saturation.

cs.PL↗
arXiv2026

SkyEgg: Heterogeneity-Aware Hardware Synthesis via Equality Saturation

Hardware synthesis is a key interface between high-level programs and accelerator designs. Modern FPGAs increasingly expose heterogeneity in resource functionality and timing configurability. Exploiting these resources requires synthesis to choose among hardware implementations and fine-grained configuration options, and coordinate these choices across multiple stages. However, prior frameworks fail to fully explore these choices due to resource models confined to per-operation mappings and limited fusion patterns. Moreover, they perform transformation, scheduling, and mapping sequentially, selecting an expression form and assigning cycle boundaries before full mapping information is available. This problem precludes chaining and fusion, excludes viable implementations from subsequent optimization stages, and limits end-to-end performance. We present SkyEgg, a heterogeneity-aware hardware synthesis framework for FPGAs. The key insight of SkyEgg is to bring algebraic equivalence and diverse resource capabilities together throughout the synthesis flow. Specifically, it encodes target-specific hardware mappings and configurations as extensible mapping rules alongside algebraic rewrite rules in equality saturation, placing algebraic and resource alternatives in a common representation. It further proposes transformation- and mapping-aware scheduling that uses these alternatives and configuration-specific timing to jointly select an equivalent form, its resource mappings, and cycle assignments to minimize end-to-end latency under target-frequency and hardware constraints. This algebraic exploration reveals forms that enable otherwise unavailable mappings. SkyEgg also provides a heuristic solver that rapidly finds high-quality solutions. Against two commercial HLS tools, SkyEgg achieves average speedups of 3.12x over Vitis HLS and 3.18x over Altera HLS across target frequencies.

cs.PL↗
arXiv2026

Folding the dragon

The Heighway Dragon Curve is one of the best known fractal curves. There are two ways to construct the curve: starting from a straight line segment, repeatedly make a copy of the current curve, rotate it by 90 degrees, and connect them; or repeatedly replace each straight segment in the curve by two segments with a right angle. A natural question is: how do we prove the equivalence of the two approaches? We generalise the construction of the curve to allow rotations to both sides. It then turns out that the two approaches are respectively a foldr and a foldl, and that the key property for proving their equivalence, using the second duality theorem, is the distributivity of an `interleave' operator.

cs.PL↗