Anonymous user
User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
User:Realazthat/Projects wishlist/LLVM/Formal methods (view source)
Revision as of 04:19, 1 November 2010
, 13 years agono edit summary
No edit summary |
No edit summary |
||
Line 22:
** Restricting heap allocation
* Allow a programmer to make certain assumptions on input (probably through assertions)
* Prove that no '''undefined behavior''' can occur
** Math overflows/underflows
** Out of bounds access
** Memory leaks
** Dangling pointers
*** etc.
** Null dereferencing
** What else
* Determine valid input ranges (if the type of the input does not already assert this)
* Show proofs for all of the above
** Create [[wp:Proof-carrying_code| Proof-carrying code]]
* Impossible stuff
** Be able to calculate a function inverse if possible
**: Hmmmm
** Transformation of function to set of equivalent functions
**: Hmmmm
* Side effect free functions
* Pure functions
* Reentrant functions
* No deadlocks etc.
* If any of the above can't be proven, show test counter examples; that is exploitable input
** Related
| |||