Hot answers tagged

3 votes
Accepted

What is the difference in heap configurations? Separation logic with CVC5 SMT solver

Thanks for the question. The model construction for the separation logic heap in cvc5 was wrong in this case. This will be fixed by https://github.com/cvc5/cvc5/pull/9574.
1 vote

What is the Kripke semantic for a linear temporal logic?

tl;dr The accessibility relation needs to be the reflexive transitive closure of what you had in mind. Details: Let $P$ be a set of atomic proposition. Write $\Sigma$ for $P$'s powerset. Write $T$ for ...
  • 480

Only top scored, non community-wiki answers of a minimum length are eligible