Viewing profile — Aurel300

As a follow-up to a CTF challenge I wrote, I created a small proof-of-concept virtual machine embedded in the Rust type system. Trait resolution and in particular associated types …

Welcome to the research field of program refinement. There are a couple of approaches one can take: - Certify: the program isn't actually checked/proven to satisfy the spec, but ex…

That's not inherent to PHP, but rather the ecosystem it's usually used in. The standard "LAMP" stack, for example, has Apache in it for the actual server, talking to PHP using a CG…

Maybe you are thinking of zahada? It is as you describe, individual HTML pages solved by typing the correct answer into the address bar. It involved a lot of lateral thinking. Some…

Our verification is based on symbolic execution, miri is an interpreter (concrete execution). So (at least in theory), our approach is more general. We have considered miri in rela…

Currently they are not handled. But (you guessed it) we also have a project working on this: attaching trusted specifications to external methods. In the long term we might investi…

We are working on improving the error reporting for the IDE extension. Regardless of the audience, Prusti is based on the Viper verification framework which is mainly implemented i…

The two tools address similar problems. The kinds of properties you can prove (automatically) should also be similar, because both Prusti and Liquid Haskell ultimately use an SMT s…

This is an active research topic in our group. Within unsafe Rust code you lose the guarantees of the Rust ownership type system, which are important for framing (figuring out whic…

The short answer is: it could be used for that. But there's a couple of things to say: - Prusti is doing _modular_ verification: every method is verified in isolation, and all call…

Yes, we could improve the wording -- suggestions and users are welcome! The tool is indeed much more general purpose than integer overflows: it is a based on a deductive verifier w…

I have been using Haxe (not professionally, but still quite intensively) for more than 3 years now. I've moved to it from AS3.0 / Flash initially to make games. As I learnt the lan…