Astral

Astral is a solver for separation logic based on translation to SMT. Astral supports clasical separation logic as well as strong-separation logic (SSL), in particular, it supports several features that are not supported by other solvers such as limited support for magic wands and arbitrary mixing and nesting of boolean and spatial connectives (see supported fragment).

The solver is currently able to use two SMT backends – Z3 and cvc5.

Supported fragment

Let $x, y$ be variables. Atomic formulae are defined as follow:

Atomic formula	Input syntax	Semantics
$x = y$	(= x y)	$s(x) = s(y)$ and $h = \emptyset$
$x \neq y$	(distinct x y)	$s(x) \neq s(y)$ and $h = \emptyset$
$x \mapsto y$	(pto x y)	$h = \lbrace s(x) \mapsto s(y) \rbrace$
$\mathsf{emp}$	emp	$h = \emptyset$
$\mathsf{ls}$(x,y)	(ls x y)	$\mathsf{dom}(h) = \emptyset \land s(x) = s(y) \text{ or there exist } n \geq 1, \ell_0, ..., \ell_n \text{ such that } \mathsf{distinct}(\ell_0, ..., \ell_n)$ $\text{ and } h = \lbrace \ell_0 \mapsto \ell_1, ..., \ell_{n-1} \mapsto \ell_n \rbrace \text{ and } s(x) = \ell_0, s(y) = \ell_n$

Let $\phi, \psi$ be formulae.

Connective	Input syntax	Semantics
$\varphi \land \psi$	(and $\varphi$ $\psi$)	$(s,h) \models \varphi \text{ and } (s,h) \models \psi$
$\varphi \lor \psi$	(or $\varphi$ $\psi$)	$(s,h) \models \varphi \text{ or } (s,h) \models \psi$
$\varphi \land_\neg \psi$	(and $\varphi \text{ (not } \psi$))	$(s,h) \models \varphi \text{ and } (s,h) \not\models \psi$
$\varphi \ast \psi$	(sep $\phi$ $\psi$)	$\exists h_1, h_2. h = h_1 \uplus^s h_2 \text{ and } (s,h_1) \models \varphi \text{ and } (s,h_2) \models \psi$
$\varphi -\kern-.46em{\circledast}$ $\psi$	(septraction $\phi$ $\psi$)	$\exists h_1. (s,h_1) \models \varphi \text { and } h_1 \uplus^s h_2 \neq \bot \text{ and } (s,h_1 \uplus^s h_2) \models \psi$

Example input

A formula $x \mapsto y -\kern-.46em{\circledast}$ $\mathsf{ls}(x,y)$ can be represented as:

(declare-sort Loc 0)      ;; Declaration of location sort. Currently fixed to this form by Astral.
(declare-heap (Loc Loc))  ;; Declaration of heap sort. Currently fixed to this form by Astral.

;; Declaration of location variables
(declare-const x Loc)
(declare-const y Loc)

;; Input formula
(assert
  (septraction
    (pto x y)
    (ls x y)
  )
)

(check-sat)

Installation & Usage

After cloning the repository, run opam install . to install Astral. Then the solver can be run by the command astral formula.smt2.

Related Papers

• Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar, and Florian Zuleger. Deciding Boolean Separation Logic via Small Models. In TACAS 2024. Technical report. Artifact.

• Dacík, Tomáš. A Decision Procedure for Strong-Separation Logic. Brno, 2022. Master's Thesis. Brno University of Technology, Faculty of Information Technology. 2022-08-25. Supervised by Vojnar Tomáš.

Contact

If you have any questions, do not hesitate to contact the tool/method authors:

• Tomáš Dacík <[email protected]>
• Adam Rogalewicz <[email protected]>
• Tomáš Vojnar <[email protected]>
• Florian Zuleger<[email protected]>

License

The tool is available under MIT license.

Acknowledgements

The development was supported by projects SNAPPY and AIDE of the Czech Science Foundation. The main author of the tool was supported by Brno Ph.D. Talent Scholarship funded by the Brno City Municipality.