Alastair Reid
Alastair Reid
I ran into four problems while installing the CVC4 support in OSX. 1) A deprecation warning about a feature that will disappear in python 3.8 2) A problem due to...
While using KLEE (current master df04aeadefb4e1c34c7ef8b9123947ff045a34d9, also observed on commit abdb0b650b8fce419dc5695e037557708f374021 from March) in a recent Ubuntu-based system (also in a docker container based on Ubuntu 20.04) on [the attached...
The experimental support for LLVM-11 does not fully work. - Verifying a program (i.e., that defines 'main') seems to work (but has not been tested extensively) - Verifying a function...
This issue is to keep track of the status of Rust language/feature support. It is limited to LLVM-based verifiers because MIR-based verifiers will probably have completely different issues. Add new...
List of LLVM-based verifiers that we know of (edit this issue to add new ones) - [x] [KLEE](http://klee.github.io/) - [ ] [KLEE-Native](https://github.com/lifting-bits/klee) - [x] [SeaHorn](http://seahorn.github.io/) - [ ] [SMACK](http://smackers.github.io/) -...
Thread support will probably have to be implemented separately for every verifier we support. Some verifiers that we plan to use do not support threads or only have very limited...
Lazy construction will work better with concolic execution because it defers path splitting to the point where a value is accessed. This cannot be done for types like Option But...
This project should have some CI checking. There’s two steps to this 1. Setup a standard CI flow that does *any* check - this mostly needs github familiarity 2. Start...
Proptest has a great interface that provides a lot of control over the values that you fuzz with. But (as far as I can tell), it is a blackbox fuzzer...
cargo-verify currently exploits parallelism between verification targets but not within each individual verification. To exploit parallelism. we need some way of doing a case split on input values (which hopefully...