search

flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14 stars 1 forks source link

Add some missing documentation #97

Closed tchajed closed 1 year ago

tchajed commented 1 year ago

For updr I made fewer things public and then didn't document the private items (I don't understand the code well enough to add that documentation in any case).

Alex-Fischman commented 1 year ago

Is this branch intended to completely resolve #95, or just part of it?

tchajed commented 1 year ago

It's only part of it. @edenfrenkel will have to write the documentation for most of the inference code.