K-user mailing list

[Dustin Wehr <dustin.wehr AT gmail.com>]

Hi, I'm working on evaluating K for our use at Legalese by writing a
semantics for a minimal version of our DSL for computational legal
contracts (https://legalese.com/#L4). I have some questions about the
current status of symbolic execution.

(a) Does K have a Real sort that works with symbolic execution
(translated to SMT's Real)?

(b) The core of our DSL is an event-driven abstract state machine that
responds to events deterministically. In most respects it is strictly
simpler than the smart contract languages that the K team has worked
on. I am wondering what would be the most important examples for me to
study of K formalizations *that support symbolic execution*. Since I'm
just learning K, the simpler the better,

(c) Are there examples I can read of finer-than-default control over
State Merging and Pruning Unrealizable Paths? I'm using the
terminology of https://arxiv.org/abs/1610.00502.

(d) What other techniques from that survey have been implemented?

(e) Have speed comparisons been done between K's symbolic execution
for some language L and a symbolic execution suite made specifically
for L?

Thanks,
Dustin Wehr