Abstract

  • Full functional-correctness verification is becoming more automatic
  • Interaction is moving closer to the problem domain
  • A well-designed language and verifier, plus a great SMT solver, go a long way