Semantics, languages and tools for layered attestation
Runtime flags processed by Chase. The flag bound limits the size of the
universe of constants. The flag input_order changes Chase’s default scheduling
of formulas. This is required for good performance of the Layered Attestation
theory.
[ bound = 500, input_order ]
Simply include various files with Chase formulas. The first file is generated
from bank2.cop before calling Chase.
m4_include(`bank2.gli')m4_dnl
m4_include(`bank2_supps.gli')m4_dnl
m4_include(`thy.gli')m4_dnl