000186012 001__ 186012
000186012 005__ 20190117220154.0
000186012 037__ $$aCONF
000186012 245__ $$a-Overify: Optimizing Programs for Fast Verification
000186012 269__ $$a2013
000186012 260__ $$c2013
000186012 336__ $$aConference Papers
000186012 520__ $$aDevelopers rely on automated testing and verification tools to gain confidence in their software. The input to such tools is often generated by compilers that have been designed to generate code that runs fast, not code that can be verified easily and quickly. This makes the verification tool's task unnecessarily hard. We propose that compilers support a new kind of switch, -Overify, that generates code optimized for the needs of verification tools. We implemented this idea for one class of verification (symbolic execution) and found that, when run on the Coreutils suite of UNIX utilities, it reduces verification time by up to 95x.
000186012 6531_ $$aVerification
000186012 6531_ $$aCompilers
000186012 6531_ $$aTesting
000186012 6531_ $$aSymbolic Execution
000186012 700__ $$0246103$$aWagner, Jonas$$g169983
000186012 700__ $$0244621$$aKuznetsov, Volodymyr$$g194743
000186012 700__ $$0241982$$aCandea, George$$g172241
000186012 7112_ $$a14th Workshop on Hot Topics in Operating Systems (HotOS XIV)$$cSanta Ana Pueblo, New Mexico, USA$$dMay 13-15, 2013
000186012 8564_ $$s529485$$uhttps://infoscience.epfl.ch/record/186012/files/overify.pdf$$yn/a$$zn/a
000186012 909C0 $$0252225$$pDSLAB$$xU11275
000186012 909CO $$ooai:infoscience.tind.io:186012$$pconf$$pIC
000186012 917Z8 $$x169983
000186012 917Z8 $$x169983
000186012 917Z8 $$x169983
000186012 937__ $$aEPFL-CONF-186012
000186012 973__ $$aEPFL$$rREVIEWED$$sACCEPTED
000186012 980__ $$aCONF