Symbolic Execution in Algorithm Design

Abstract

Sy rnbu!ic exec uticn of part ial algorithm descriptions is a i >rHw ;rfll! mc !!tod f(,, (l tJ idinu il1 c (licJtlri\inn c!e:-; ign process (as is born e ou t !1y studyi:1u protoc(;l:> oi l wm :· q aluorilhPl desig ners). Yi"t t11e rol e of ~;yrnbo li c ex ecution in algori thm design has not b ee n c 1 0 $f! ly uxarn ined, cl esp~ te th 2 work c)n syrnbo! ic e :.-: ec ution of complete prourams e.s an :) ;d in the va licl ::tion of so ftware. In the cunt er : of t! 1e DESI GNER p r oj~ct . w,~ have dev e l cpo~ d a data-fiow lan juagc; for i'epr es c; nli :ly p a rtt~iiy de signee! <ligo rithrn s and n pr or.•! -.~ lc1 r .<; ~· tnlvll i c• · !i y r:xr:c trt iniJ d:ltu -ll,lw cn nliuurations th ~tt c;tf1 u<:;c uver us dul kno\'!led<;e to quid; • de si <Jn . rilE: t2chniques O ' ~: ;:.;r: i 11;d IHcre Cilnt rillut e s i ~Jnifica nlly tr,warcls cur goal of t:-,uik:it t!J ~~ fu ll y au t unuted alyoritl ll l t C: cs iQ n ~y:> l e m .