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

@article{Betts:2017:10.1109/TSE.2017.2718516,
author = {Betts, A and Chong, N and Deligiannis, P and Donaldson, AF and Ketema, J},
doi = {10.1109/TSE.2017.2718516},
journal = {IEEE Transactions on Software Engineering},
pages = {631--650},
title = {Implementing and evaluating candidate-based invariant generation},
url = {http://dx.doi.org/10.1109/TSE.2017.2718516},
volume = {44},
year = {2017}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - The discovery of inductive invariants lies at the heart of static program verification. Presently, many automatic solutions toinductive invariant generation are inflexible, only applicable to certain classes of programs, or unpredictable. An automatic techniquethat circumvents these deficiencies to some extent iscandidate-based invariant generation, whereby a large number of candidateinvariants are guessed and then proven to be inductive or rejected using a sound program analyser. This paper describes our efforts toapply candidate-based invariant generation in GPUVerify, a static checker of programs that run on GPUs. We study a set of383GPUprograms that contain loops, drawn from a number of open source suites and vendor SDKs. Among this set,253benchmarks requireprovision of loop invariants for verification to succeed.We describe the methodology we used to incrementally improve the invariant generation capabilities of GPUVerify to handle thesebenchmarks, throughcandidate-based invariant generation, whereby potential program invariants are speculated using cheap staticanalysis and subsequently either refuted or proven. We also describe a set of experiments that we used to examine the effectiveness ofour rules for candidate generation, assessing rules based on theirgenerality(the extent to which they generate candidate invariants),hitrate(the extent to which the generated candidates hold),effectiveness(the extent to which provable candidates actually help in allowingverification to succeed), andinfluence(the extent to which the success of one generation rule depends on candidates generated byanother rule). We believe that our methodology for devising and evaluation candidate generation rules may serve as a useful frameworkfor other researchers interested in candidate-based invariant generation.The candidates produced by GPUVerify help to verify231of these253programs. An increase in precision, however, has createdsluggishness in GPUVerify because more candidates are gen
AU  - Betts,A
AU  - Chong,N
AU  - Deligiannis,P
AU  - Donaldson,AF
AU  - Ketema,J
DO  - 10.1109/TSE.2017.2718516
EP  - 650
PY  - 2017///
SN  - 1939-3520
SP  - 631
TI  - Implementing and evaluating candidate-based invariant generation
T2  - IEEE Transactions on Software Engineering
UR  - http://dx.doi.org/10.1109/TSE.2017.2718516
UR  - http://hdl.handle.net/10044/1/47865
VL  - 44
ER  -
Download