@inproceedings(aiken:popl98,
 author       = "A. Aiken and D. Gay",
 year         = "1998",
 title        = "Barrier Inference",
 booktitle    = "Procs. of the Symp. on Principles of Programming Languages (POPL)",
 pages        = "342--354",
 doi          = "10.1145/268946.268974",
)
@inproceedings(boyer:stmcs08,
 author       = "M. Boyer and K. Skadron and W. Weimer",
 year         = "2008",
 title        = "Automated Dynamic Analysis of {CUDA} Programs",
 booktitle    = "Proc. of the 3rd Workshop on Software Tools for Multicore Systems",
)
@inproceedings(ellison:popl12,
 author       = "C. Ellison and G. Ro{\cb {s}}u",
 year         = "2012",
 title        = "An Executable Formal Semantics of {C} with Applications",
 booktitle    = "Proc. of the Symp. on Principles of Programming Languages (POPL)",
 doi          = "10.1145/2103656.2103719",
)
@phdthesis(ellison:phd,
 author       = "C. M. Ellison",
 year         = "2012",
 title        = "A Formal Semantics of {C} with Applications",
 school       = "UIUC",
)
@techreport(habermaier:tr11,
 author       = "A. Habermaier",
 year         = "2011",
 title        = "The Model of Computation of {CUDA} and Its Formal Semantics",
 type         = "Technical Report",
 institution  = "Universit{\"a}t Augsburg",
)
@inproceedings(habermaier:esop12,
 author       = "A. Habermaier and A. Knapp",
 year         = "2012",
 title        = "On the Correctness of the {SIMT} Execution Model of {GPU}s",
 booktitle    = "Proc. of the European Symp. on Programming (ESOP)",
 doi          = "10.1007/978-3-642-28869-2\_16",
)
@inproceedings(harris:optimizing-reduction-cuda,
 author       = "M. Harris",
 title        = "Optimizing Parallel Reduction in {CUDA}",
 booktitle    = "GPU Technology Conf.",
 publisher    = "NVIDIA",
)
@inproceedings(li:ppopp12,
 author       = "G. Li and P. Li and G. Sawaya and G. Gopalakrishnan and I. Ghosh and S. P. Rajan",
 year         = "2012",
 title        = "{GKLEE}: {C}oncolic Verification and Test Generation for {GPU}s",
 booktitle    = "Proc. of the Symp. on Principles and Practices of Parallel Prog. (PPoPP)",
 doi          = "10.1145/2145816.2145844",
)
@article(rosu:jlap10,
 author       = "G. Ro{\cb {s}}u and T. F. {\cb {S}}erb{\u {a}}nu{\cb {t}}{\u {a}}",
 year         = "2010",
 title        = "An Overview of the {$\mathbb {K}$} Semantic Framework",
 journal      = "Journal of Logic and Algebraic Programming",
 volume       = "79",
 number       = "6",
 pages        = "397--434",
 doi          = "10.1016/j.jlap.2010.03.012",
)
@inproceedings(rosu:oopsla12,
 author       = "G. Ro{\cb {s}}u and A. {\cb {S}}tef{\u {a}}nescu",
 year         = "2012",
 title        = "Checking Reachability using Matching Logic",
 booktitle    = "Proc. of the Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)",
 doi          = "10.1145/2384616.2384656",
)
@inproceedings(ryoo:ppopp08,
 author       = "S. Ryoo and C. I. Rodrigues and S. S. Baghsorkhi and S. S. Stone and D. B. Kirk and W. W. Hwu",
 year         = "2008",
 title        = "Optimization Principles and Application Performance Evaluation of a Multithreaded {GPU} Using {CUDA}",
 booktitle    = "Proc. of the Symp. on Principles and Practice of Parallel Prog. (PPoPP)",
 pages        = "73--82",
 doi          = "10.1145/1345206.1345220",
)
@inproceedings(tripakis:hotpar10,
 author       = "S. Tripakis and C. Stergiou and R. Lublinerman",
 year         = "2010",
 title        = "Checking Non-Interference in {SPMD} Programs",
 booktitle    = "Proc. of the 2nd USENIX Workshop on Hot Topics in Parallelism (HotPar)",
 pages        = "1--6",
)
@inproceedings(zheng:ppopp11,
 author       = "M. Zheng and V. T. Ravi and F. Qin and G. Agrawal",
 year         = "2011",
 title        = "{GR}ace: {A} Low-Overhead Mechanism for Detecting Data Races in {GPU} Programs",
 booktitle    = "Proc. of the Symp. on Principles and Practice of Parallel Prog. (PPoPP)",
 doi          = "10.1145/1941553.1941574",
)