Peter Sewell

I don't (now I think of it) really want to make them publicly visible and archived. On 12 November 2017 at 23:30, Boris Veytsman wrote: > Maybe you could attach...

On 12 November 2017 at 23:56, Boris Veytsman wrote: > Here is the problem: \renewcommand{\rmdefault}{ptm}. This changes the > font of your document. This leads to many other problems, since...

On 13 November 2017 at 15:18, Craig-Rodkin wrote: > Hi, > > We will take this issue up with the volunteers with the end of year > template review. >...

There is also the Isla symbolic execution engine https://github.com/rems-project/isla, which in some cases might be used for this. peter On Mon, 7 Feb 2022 at 23:24, Martin Berger ***@***.***> wrote:...

no - but why would you want to? On Tue, 8 Feb 2022 at 10:23, Martin Berger ***@***.***> wrote: > @PeterSewell Does Isla handle > unrestricted recursion? > > —...

On Tue, 8 Feb 2022 at 10:36, Martin Berger ***@***.***> wrote: > Bill wants to prove equivalence of two full models .. > Some refactorings would just be of a...

It should do two independent accesses, separately translated, no? On Mon, 28 Jun 2021, 10:54 Robert Norton, ***@***.***> wrote: > Unfortunately looks like we still need a fix for this....

I don't know exactly how the model is structured, but my point is that the decomposition of misaligned accesses into multiple accesses should happen slightly higher up, before one even...

On Mon, 28 Jun 2021 at 13:30, Robert Norton ***@***.***> wrote: > I haven't checked the spec but I imagine you'd want to do both of the > translations first...

On Tue, 12 Mar 2024 at 06:15, Allen Baum ***@***.***> wrote: > Note that the spec doesn't require that the write to the 2 halves appear > in > a...