search

viperproject / silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
81 stars 34 forks source link

Incompletenesses in various examples (to investigate) #301

Open viper-admin opened 7 years ago

viper-admin commented 7 years ago

Created by @alexanderjsummers on 2017-08-10 16:57 Last updated on 2017-08-11 09:22

These come from the Program Verification course, and are all examples for which Carbon succeeds (in reasonable time).

Link_List_BUB_Base_verifies.vpr: one failure

Link_List_BUB_Ex1_verifies.vpr: variant of the previous example, which passes

Array_Quick_Base_verifies.vpr: takes just under a minute, one failure

Array_Quick_Ex2_verifies.vpr: variant of the previous example, which passes (but needs fewer methods..)

problem4_base.vpr: this one doesn't seem to terminate - it uses plenty of non-linear arithmetic so that's perhaps not surprising, but susprisingly Carbon terminates fairly fast on this and variants of this example.

Attachments:

viper-admin commented 7 years ago

@alexanderjsummers on 2017-08-10 16:57:

  • edited the description
viper-admin commented 7 years ago

@alexanderjsummers on 2017-08-10 17:04:

  • changed attachment from (none) to Array_Quick_Base_verifies.vpr
  • edited the description
viper-admin commented 7 years ago

@alexanderjsummers on 2017-08-10 20:21:

  • changed attachment from (none) to problem4_base.vpr
  • edited the description
viper-admin commented 7 years ago

@alexanderjsummers on 2017-08-11 09:22:

  • edited the description