Remy Willems

icon indicating a website link https://keyboarddrummer.github.io/ icon indicating an email [email protected]

icon company @amzn icon location Utrecht, Netherlands icon location I mainly work on Dafny and on Miksilo, a tool to construct programming languages in a modular way.

Results 84 comments of Remy Willems
trafficstars

Unstable test: "DafnyTestGeneration.Test" test run gets cancelled, possibly due to taking too long

@MikaelMayer I'm not working on this. Next step is finding someone to work on resolving it.

Malformed Boogie in match inside forall

The loop detection code produces the following incorrect Dafny code: ```dafny predicate WellTyped(ii: seq, typing: seq) decreases ii, typing { forall pc: int, _t#0: int {:trigger typing[pc], typing[_t#0]} {:trigger typing[_t#0],...

[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny

Can locally reproduce using Z3 4.12.1, although not with `Z3 4.12.6` ``` dafny/AwsEncryptionSdk/src/MessageBody.dfy(1034,13): Error: Verification of 'MessageBody.ReadFramedMessageBody' timed out after 30 seconds | 1034 | assert CorrectlyRead(buffer, Success(SuccessfulRead(nextRegularFrames, regularFrame.tail)), WriteMessageRegularFrames)...

[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny

The `ReadFramedMessageBody` proof uses 48E6 resources on Dafny 4.2.0, so it might just be a verification brittleness issue. Running on 4.2.0, this assertion batch which has an assertion with the...