Silicon 2.0

Silicon 2.0

This document is meant to collect ideas, open questions, wishes and visions for a complete rewrite of Silicon

• Implementation language: Rust or Go instead of Scala?

  • A system language for better performance?
  • Z3 API bindings available?
  • Interoperability with Silver?

• Implementation style

  • Replace CPS?
  • Translate a Viper program into a sequence of symbolic execution primitives that can then be executed/interpreted, but also analysed, optimised, etc.?
  • How to implement try-heuristic-retry patterns, e.g. for state consolidations?

• Systematic support for

  • Incremental verification, e.g. in an IDE
  • Debugging, failure understanding, partial (re)verification
  • Logging, tracing, visualisations
  • Custom permission models
  • Tactics/strategies for heuristically applying custom lemmas

• Encoding changes

  • Target larger, frontend generated Viper programs, not the traditional Silver test suite
  • Fewer branches, more merging/joining
  • Reduce the number of Z3 check-sats
  • Replace "evaluations on demand" by parametric pre-evaluations
  • Avoid introduction of new symbols on demand