esverify
esverify copied to clipboard
levjj
ECMAScript verification with SMT solvers
esverify currently generates verifications and dispatches these sequentially to the SMT solver. As a performance improvement, it would be possible to parallize this process. In addition to solving VCs, this...
There is already adhoc support for higher-order annotations by using `spec` with verification-only functions. However, this should become a core langauge feature to provide better support for parametric polymorphism, etc.
I really like the concept, and thought it would be better to have a typescript-integration. - most typescript-codes already have types have types ```typescript function max(a: number, b: number) {...
esverify should support mutually recursive functions. Example: ```javascript function isEven(n) { requires(Number.isInteger(n) && n >= 0); return n === 0 ? true : isOdd(n - 1); } function isOdd(n) {...
The current rudamentary support for (immutable) classes does not include inheritance. However, it should be possible to extend a superclass, use `super` and check whether the overriden methods adhere to...
Just wanted to raise awareness of [Vampire Prover](https://vprover.github.io/) Vampire prover uses z3 and minisat internally and performs significantly better in many tasks. One of its unique features is to can...
Hello, esverify looks nice. I think it may be more practical for existing projects to put the `ensures` and `requires` annotations in comments, to avoid any side-effect during the execution....
[Flow](https://flow.org/) is Facebook's take on type annotations for JavaScript. There are a couple of libraries [[1][1], [2][2]] for converting between TypeScript and Flow, so the functionality could piggyback on the...
Adding support for import and export statements. This also includes importing and exporting of annotations such as pre-, postconditions and invariants. Example: ```javascript // File a.js export function f(x) {...
esverify currently only supports immutable object literals and arrays. Improved support for mutability probably requires some redesign of the fundamental base of the vcgen, e.g. segmentation logic or frames/regions. Example:...