Imperial College London
Portrait Picture

ProfessorAlastairDonaldson

Faculty of Engineering, Department of Computing

Professor of Programming Languages
 
 
 
//

Contact

 

+44 (0)20 7594 8266alastair.donaldson Website

 
 
//

Location

 

422Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Liew:2016:10.1109/ICST.2016.11,
author = {Liew, D and Cadar, C and Donaldson, A},
doi = {10.1109/ICST.2016.11},
publisher = {IEEE},
title = {Symbooglix: A symbolic execution engine for boogie programs},
url = {http://dx.doi.org/10.1109/ICST.2016.11},
year = {2016}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - We  present  the  design  and  implementation  of  Sym-booglix, a symbolic execution engine for the Boogie intermediateverification  language.  Symbooglix  aims  to  find  bugs  in  Boogieprograms  efficiently,  providing  bug-finding  capabilities  for  anyprogram   analysis   framework   that   uses   Boogie   as   a   targetlanguage.  We  discuss  the  technical  challenges  associated  withhandling  Boogie,  and  describe  how  we  optimised  Symbooglixusing   a   small   training   set   of   benchmarks.   This   empirically-driven  optimisation  approach  avoids  over-fitting  Symbooglix  toour  benchmarks,  enabling  a  fair  comparison  with  other  tools.We present an evaluation across 3749 Boogie programs generatedfrom the SV-COMP suite of C programs using the SMACK front-end, and 579 Boogie programs originating from several OpenCLand CUDA GPU benchmark suites, translated by the GPUVerifyfront-end.  Our  results  show  that  Symbooglix  significantly  out-performs Boogaloo, an existing symbolic execution tool for Boogie,and  is  competitive  with  GPUVerify  on  benchmarks  for  whichGPUVerify is highly optimised. While generally less effective thanthe Corral and Duality tools on the SV-COMP suite, Symbooglixis complementary to them in terms of bug-finding ability.
AU  - Liew,D
AU  - Cadar,C
AU  - Donaldson,A
DO  - 10.1109/ICST.2016.11
PB  - IEEE
PY  - 2016///
TI  - Symbooglix: A symbolic execution engine for boogie programs
UR  - http://dx.doi.org/10.1109/ICST.2016.11
UR  - https://ieeexplore.ieee.org/document/7515458
UR  - http://hdl.handle.net/10044/1/29765
ER  -
Download