Zobrazeno 1 - 10
of 160
pro vyhledávání: '"Hayes, Ian J."'
Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for sequential programs but further issues arise for concurrent programs
Externí odkaz:
http://arxiv.org/abs/2409.07741
Autor:
Colvin, Robert J., Hayes, Ian J., Heiner, Scott, Höfner, Peter, Meinicke, Larissa, Su, Roger C.
Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A particular feature is pipelined "out-of-order execution" of the code as writ
Externí odkaz:
http://arxiv.org/abs/2407.20559
The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to all
Externí odkaz:
http://arxiv.org/abs/2405.05690
Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of programs that use more efficient concrete representations. Data reification (
Externí odkaz:
http://arxiv.org/abs/2405.05546
Autor:
Meinicke, Larissa A., Hayes, Ian J.
Distributive laws are important for algebraic reasoning in arithmetic and logic. They are equally important for algebraic reasoning about concurrent programs. In existing theories such as Concurrent Kleene Algebra, only partial correctness is handled
Externí odkaz:
http://arxiv.org/abs/2403.13425
Publikováno v:
Formal Methods and Software Engineering. ICFEM 2023. Lecture Notes in Computer Science, vol 14308. Springer, Singapore
This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential products, adhering to a weak exchange law. This development of
Externí odkaz:
http://arxiv.org/abs/2305.18017
Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms.
Externí odkaz:
http://arxiv.org/abs/2212.06956
We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph transformations. We have built high-level models of the data structures and
Externí odkaz:
http://arxiv.org/abs/2212.01748
Publikováno v:
In: Relational and Algebraic Methods in Computer Science. RAMiCS 2023. Lecture Notes in Computer Science, vol 13896. Springer, Cham (2023)
We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions,
Externí odkaz:
http://arxiv.org/abs/2210.09476
The optimization phase of a compiler is responsible for transforming an intermediate representation (IR) of a program into a more efficient form. Modern optimizers, such as that used in the GraalVM compiler, use an IR consisting of a sophisticated gr
Externí odkaz:
http://arxiv.org/abs/2107.01815