Astral is a SMT solver for separation logics.
Operations over constant values.
Constructors and operations over pure formulae.
Access to Astral's memory model.
Basic operations over separation logic formulae.
Operations over separation logic which take into account semantics of inductive predicates.
Constructors for built-in definitions provided by Astral.
Stack-heap models of separation logic.