equal
deleted
inserted
replaced
52 support for higher-order features (esp. lambda abstractions). |
52 support for higher-order features (esp. lambda abstractions). |
53 It is an incomplete decision procedure based on external SMT |
53 It is an incomplete decision procedure based on external SMT |
54 solvers using the oracle mechanism; for the SMT solver Z3, |
54 solvers using the oracle mechanism; for the SMT solver Z3, |
55 this method is proof-producing. Certificates are provided to |
55 this method is proof-producing. Certificates are provided to |
56 avoid calling the external solvers solely for re-checking proofs. |
56 avoid calling the external solvers solely for re-checking proofs. |
|
57 Due to a remote SMT service there is no need for installing SMT |
|
58 solvers locally. |
57 |
59 |
58 * New commands to load and prove verification conditions |
60 * New commands to load and prove verification conditions |
59 generated by the Boogie program verifier or derived systems |
61 generated by the Boogie program verifier or derived systems |
60 (e.g. the Verifying C Compiler (VCC) or Spec#). |
62 (e.g. the Verifying C Compiler (VCC) or Spec#). |
61 |
63 |