search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
429 stars 40 forks source link

[FEATURE] proof scripts #490

Open konnov opened 3 years ago

konnov commented 3 years ago

It would be great to have a tool (or at least a collection of patterns) that produce a sequence of queries to Apalache, in order to check the standard properties:

  1. Inductive invariants. A well-known pattern, but it is annoying that one has to run Apalache three times by hand.
  2. Refinement. When proving by hand, this requires some thinking. The process should be fairly easy to automate. E.g., see #469.
  3. Some forms of liveness?

There is no good reason why these patterns should be hidden inside Apalache. We should be able to produce external proof scripts. This will help the user to understand what kind of reasoning is implemented.

konnov commented 3 years ago

Before we go in automating anything, let's write HOWTOs: #546

Kukovec commented 2 years ago

We should revisit this when #730 is implemented.