Alpha: This is still a research prototype and not yet ready for production use.
A detailed documentation of esverify and its theoretical foundations is currently work-in-progress and will be published soon.
max function, we can add pre- and post-conditions using special pseudo-calls to
ensures with boolean expressions.
These expressions will then be statically verified with respect to the function body with an SMT solver.
More examples can be found in the
- expressions with boolean values, strings, integer and real number arithmetic
- function pre- and post conditions as well as inline assertions and invariants
- automatically generates counter-examples for failed assertions
- mutable variables and limited temporal reasoning, e.g.
old(x) > x
- control flow including branching, returns and while loops with manually specified invariants
- inductive reasoning with loop invariants and recursive functions
- automatic inlining of function body for external proofs of function properties (restricted to one level of inlining)
- checking of function purity
- higher-order functions
- simple proof checking using Curry-Howard correspondence
- simple immutable classes with fields, methods and class invariant (no inheritance)
- immutable arrays (no sparse arrays)
- restricted verifier preamble for global objects such as
It is based on the z3 SMT solver but avoids trigger heuristics and thereby (most) timeouts and other unpredictable results by requiring manual instantiation. Function definitions and class invariants correspond to universal quantifiers and function calls and field access act as triggers that instantiate these quantifiers in a deterministic way.
- termination checking
- mutable objects, arrays and classes
- modules with imports and exports
- prototype and subclass inheritance
- verifier-only “ghost” variables, arguments and functions/predicates
- TypeScript as input language
Simple usage without installation:
$ npx esverify file.js
$ npm install -g esverify
Command Line Options:
$ esverify --help Usage: esverify [OPTIONS] FILE Options: --z3path PATH Path to local z3 executable (default path is "z3") -r, --remote Invokes z3 remotely via HTTP request --z3url URL URL to remote z3 web server --noqi Disables quantifier instantiations -t, --timeout SECS Sets timeout in seconds for z3 (default timeout is 10s, 0 disables timeout) -f, --logformat FORMAT Format can be either "simple" or "colored" (default format is "colored") -q, --quiet Suppresses output -v, --verbose Prints SMT input, output and test code --logsmt PATH Path for logging SMT input in verbose mode (default path is "/tmp/vc.smt") -h, --help Prints this help text and exit --version Prints version information
Usage as Library
Installation via npm:
$ npm install esverify --save
verify and invoke on source code to receive a promise of messages.
The options and returned messages have the following structure:
type opts = "colored" = "colored", z3path: string = "z3", z3url: string, remote: boolean = false, quiet: true, verbose: false, logsmt: '/tmp/vc.smt' timeout: 5, qi: true type msg = "timeout"
More tool support will be coming soon.
This project is developed by the Software and Languages Research Group at University of California, Santa Cruz. Thanks also to Tommy, Sohum and Cormac for support and advice.