K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

K does not have a real sort. We do however have support for IEEE 754 floating point numbers as well as the SMTLIB floating point theory.

If you want to study how K can be used for symbolic execution, I would suggest reading the 1_k/5_types  and 2_languages/4_logik sections of the K tutorial.

K does not currently have any ability to customize how states are merged with one another, but any path that is found to be infeasible either by the K simplifier or by SMTLIB is pruned, and you do have a certain amount of control over both through lemmas introduced with the lemma attribute or smtlib attributes on productions to pass them to the solver.

I don't have time to familiarize myself with the paper you mention but maybe someone else can answer.

In terms of performance, there is definitely room for improvement in K's performance of symbolic execution, but my experience is that many real languages do not even have any way to symbolically execute them with a formal semantics aside from K, as the task of constructing a semantics for a new language is very time consuming and error prone and most such semantics not written in K have not been adequately tested or cover only some fragment of the real language, or both. If you have an example language L in mind, I might be willing to take a look though. That being said, most performance optimizations we've done have focused on concrete execution.