Symbolic crosschecking of data-parallel floating point code
In this thesis we present a symbolic execution-based technique for cross-checking programs accelerated using SIMD or OpenCL against an unaccelerated version, as well as a technique for detecting data races in OpenCL programs. Our techniques are implemented in KLEE-CL, a symbolic execution engine bas...
Main Author: | Collingbourne, Peter Cyrus |
---|---|
Other Authors: | Kelly, Paul ; Yoshida, Nobuko |
Published: |
Imperial College London
2013
|
Subjects: | |
Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.570047 |
Similar Items
-
Symbolic execution of verification languages and floating-point code
by: Liew, Daniel Simon
Published: (2017) -
Biophysically accurate floating point neuroprocessors
by: Zhang, Yiwei
Published: (2011) -
Customisable and reconfigurable platform for optimising floating point computations
by: Hok Ho, Chun
Published: (2010) -
Profile-directed specialisation of custom floating-point hardware
by: Brown, Ashley W.
Published: (2010) -
CrossCheck usage in a journal publication
by: Jaeseok Choi, et al.
Published: (2016-02-01)