Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6875226 | Science of Computer Programming | 2018 | 20 Pages |
Abstract
Third, we show that the relational encoding can be used to justify a calculus for clash-free ASM rules based on symbolic execution. Such a calculus is useful for interactive theorem provers such as our tool KIV.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller, Wolfgang Reif,