Comments (1)
The first step towards producing a cogent explanation of why a proof is correct is to plumb the necessary information into places that are easy to access. Currently, the following information is tucked away under the hood of the verifier, and we should bring it to the surface:
- Undefined behavior checks in Crucible
- Other Crucible assertions
- What4 formulae for the bullet points above
- Raw SMT solver interactions corresponding to the What4 formulae (#36)
- Equality checks between Copilot stream values and C array values
- Equality checks between trigger arguments on the Copilot and C side
- Checks that the trigger functions are invoked at the same times on the Copilot and C side
- Copilot line number information (#37)
- Anything else?
It might make sense to open smaller issues for each of these subtasks as we work on them.
from copilot-verifier.
Related Issues (20)
- Improve error reporting
- More complete test coverage
- Floating-point `signum` operation fails to verify HOT 5
- `FPOps` example fails when verifying `Float`s instead of `Double`s HOT 4
- Allow verification of more programs with partial functions HOT 5
- Ask Copilot for the names of generated global variables
- Minor soundness issue with trigger functions HOT 1
- Can't verify trigger function using array of structs
- Add CI for `copilot-verifier`
- Display Copilot-related line number information HOT 1
- `LLVMParseError` on LLVM 14.0.0 HOT 3
- Prepare for eventual release to Hackage HOT 1
- Add CI status and Hackage badges to README
- Fix hyperlinks in `copilot-verifier` Hackage page
- Mention ICFP paper in the README
- Log when Crucible simplifies trivial proof goals HOT 1
- Make it clearer which equality-related proof goals happen before and after calling `step()`
- Release 3.19 to Hackage HOT 1
- Support structs HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from copilot-verifier.