4 papers
Correct and Complete Symbolic Execution for Free
Erik Voogd, Einar Broch Johnsen, à smund Aqissiaq Arild Kløvstad +2
Symbolic execution is a powerful technique for program analysis. However, the formal semantics underlying symbolic execution is often developed on an ad-hoc basis and decoupled fro…
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Cheng Zhang, Qiancheng Fu, Hang Ji +3
This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate a…
Kleene Algebra
Tobias Kappé, Alexandra Silva, Jana Wagemaker
This booklet serves as an introduction to Kleene Algebra (KA), a set of laws that can be used to study general equivalences between programs. It discusses how general programs can…
Weighted GKAT: Completeness and Complexity
Spencer Van Koevering, Wojciech Różowski, Alexandra Silva
We propose Weighted Guarded Kleene Algebra with Tests (wGKAT), an uninterpreted weighted programming language equipped with branching, conditionals, and loops. We provide an operat…