search

viperproject / gobra

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
https://gobra.ethz.ch
Other
111 stars 28 forks source link

Use named axioms instead of anonymous axioms #750

Open dnezam opened 7 months ago

dnezam commented 7 months ago

At the moment, it seems that Gobra uses anonymous quantified axioms. This makes measuring the quantifier instantiations as described in this Silicon PR harder for those axioms. If possible, it may be useful to give names to those axioms.

jcp19 commented 6 months ago

@dnezam what are the domains for which adding names to quantifiers would help the most?

dnezam commented 6 months ago

@jcp19 This problem came up when doing experiments on the examples from chapter 10.2 of Program Proofs, so I think AdtEncoding.scala.

Additionally, perhaps SlicesImpl.scala, ArrayImpl.scala, Option(ToSeq)Impl.scala and StringEncoding.scala could be interesting, as these sound like types that could end up in the standard library at some point (and hence more likely to be evaluated more thoroughly).