Terminology question: is "symbolic execution" of a program restricted to reasoning about just one path through the code or can it reason about all paths through the code? If the latter, does that overlap with/subsume (bounded) model checking of the program?
-
-
Ok so “symbolic evaluation“ includes Sym. Execution and BMC and hybrids. Pure Sym Exec never merges states at join points, BMC always merges states. And Hybrid Sym Ex sometimes merges states. Cool, nice, simple taxo. Thanks
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.