Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Podkopaev, Anton"'
We present CoqPilot, a VS Code extension designed to help automate writing of Coq proofs. The plugin collects the parts of proofs marked with the admit tactic in a Coq file, i.e., proof holes, and combines LLMs along with non-machine-learning methods
Externí odkaz:
http://arxiv.org/abs/2410.19605
Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard noti
Externí odkaz:
http://arxiv.org/abs/2012.01067
Autor:
Watt, Conrad, Pulte, Christopher, Podkopaev, Anton, Barbier, Guillaume, Dolan, Stephen, Flur, Shaked, Pichon-Pharabod, Jean, Guo, Shu-yu
Modern JavaScript includes the SharedArrayBuffer feature, which provides access to true shared memory concurrency. SharedArrayBuffers are simple linear buffers of bytes, and the JavaScript specification defines an axiomatic relaxed memory model to de
Externí odkaz:
http://arxiv.org/abs/2005.10554
Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous "out-of-thin-air" problem. Although it has been shown to have important benefits over other memory models, its established compilation scheme
Externí odkaz:
http://arxiv.org/abs/1911.06567
We develop a new intermediate weak memory model, IMM, as a way of modularizing the proofs of correctness of compilation from concurrent programming languages with weak memory consistency semantics to mainstream multi-core architectures, such as POWER
Externí odkaz:
http://arxiv.org/abs/1807.07892
In this work, we present a family of operational semantics that gradually approximates the realistic program behaviors in the C/C++11 memory model. Each semantics in our framework is built by elaborating and combining two simple ingredients: viewfron
Externí odkaz:
http://arxiv.org/abs/1606.01400
The artifact is a virtual machine image containing two Coq packages which include mechanization of proofs stated in the paper. The first package imm contains a modified version of the Intermediate Memory Model, extended with the support of sequential
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::feca038127b93afc2f175806ce2e96f9
Autor:
Podkopaev, Anton, Boulytchev, Dmitri
Publikováno v:
Perspectives of System Informatics; 2015, p257-265, 9p
