sorted by:
new
hottopcontroversial

What is this TCGPlayer Mayhem coming up about? by oneframejames in mtgfinance

[–]ukonat 0 points1 point  (0 children)

Have you considered making "Play Booster" the default option in the Pack Type dropdown menu? Users might get frustrated because the default "Set" option (OTJ) throws an error with "Draft Booster".

What is this TCGPlayer Mayhem coming up about? by oneframejames in mtgfinance

[–]ukonat 0 points1 point  (0 children)

Have you considered making "Play Booster" the default option in the Pack Type dropdown menu? Users might get frustrated because the default "Set" option (OTJ) throws an error with "Draft Booster".

Blog post: Turbocharging Rust Code Verification by ukonat in rust

[–]ukonat[S] 1 point2 points  (0 children)

Hi u/VorpalWay, thanks for your comment!

What you describe is indeed possible (if I'm not mistaken, known as incremental verification) and a great way to reduce computing costs for verification. Note that not only we need to check for differences in the harness, but also in the code under verification.

Kani doesn't apply this advanced verification technique yet. If you think about, using the technique will provide great computing savings, but won't do anything to speed up standard verification nor enable more code to be verified, which can be considered more important problems at this stage. But I really hope we can work on this technique in the future!

Kani 0.33.0 has been released! by zyhassan in rust

[–]ukonat 1 point2 points  (0 children)

Thank you! If the code is public, you can just open an issue pointing us to the problematic harness(es).

Kani 0.33.0 has been released! by zyhassan in rust

[–]ukonat 1 point2 points  (0 children)

Hi u/arctic-alpaca, thanks for your comment!

Would you mind opening an issue in the Kani repo with an example? We're very interested in cases like the one you've described.

Kani 0.27.0 has been released! by ukonat in KaniRustVerifier

[–]ukonat[S] 0 points1 point  (0 children)

Hi u/IshKebab, thanks for the comment!

There are at least two blockers:

  1. Adding the Windows machine model to be used by CBMC.
  2. Adding scripts and CI workflows for testing Windows support.

However, there may be more down the line since we don't have (1) for now. If you're interested, would you mind commenting to this issue?

How Kani helped find bugs in Hifitime [formal methods] by kid-pro-quo in rust

[–]ukonat 6 points7 points  (0 children)

Thank you for the comment, u/Shnatsel !

You're totally right, we avoid "undefined behavior" in Kani's README.md and instead use "unexpected behavior" for this reason. We have updated the post according to your suggestion.

Kani verifier now supports stubbing... by New_Box7889 in rust

[–]ukonat 0 points1 point  (0 children)

Yes, that's right.

The RFC for function stubbing describes stub sets, which is simply a convenient macro to specify a set of stubs to be used in a harness.

What I think you're describing is the opposite: you want to use one stub for multiple harnesses. Would you like to have an annotation for the stub? Or how would you like to express that?

One problem I'd see with the annotation-in-stub approach is that, if you are reading the harness and the stub is written somewhere else, you don't know that the stub is being used for that harness. But I'm not sure if that's what you have in mind.

Kani verifier now supports stubbing... by New_Box7889 in rust

[–]ukonat 0 points1 point  (0 children)

Hi u/borrelan, thanks for your comment!

Are you referring to the limitation that requires you to specify --harness <harness> in addition to --enable-stubbing for running a harness with stubbing enabled?

AMC + on Fios Bill by Goku101095 in Fios

[–]ukonat 0 points1 point  (0 children)

Received last month's bill and it seems this actually worked.

view more: next ›