@inproceedings(Boogie,
 author       = "M. Barnett and B. Chang and R. Deline and B. Jacobs and K.R.M. Leino",
 year         = "2005",
 title        = "Boogie: A Modular Reusable Verifier for Object-Oriented Programs",
 booktitle    = "FMCO 2005",
 doi          = "10.1007/11804192\_17",
)
@inproceedings(GPUVerify,
 author       = "Adam Betts and Nathan Chong and Alastair Donaldson and Shaz Qadeer and Paul Thomson",
 year         = "2012",
 title        = "GPUVerify: A Verifier for GPU Kernels",
 booktitle    = "Proceedings of OOPSLA 2012",
 publisher    = "ACM",
 doi          = "10.1145/2384616.2384625",
)
@article(STOBJ,
 author       = "Robert S. Boyer and J Strother Moore",
 year         = "2002",
 title        = "Single-Threaded Objects in {ACL2}",
 journal      = "PADL 2002",
 doi          = "10.1007/3-540-45587-6\_3",
)
@inproceedings(Ginsburg2011,
 author       = "Dan Ginsburg",
 year         = "2011",
 title        = "Parallelizing Dijkstra's Single-Source Shortest-Path Graph Algorithm",
 editor       = "Aaftab Munshi and Benedict Gaster and Timothy Mattson and James Fung and Dan Ginsburg",
 booktitle    = "OpenCL Programming Guide",
 publisher    = "Addison-Wesley Professional",
 pages        = "411--424",
)
@inproceedings(WildingGreve03,
 author       = "David Greve and Matthew Wilding",
 year         = "2003",
 title        = "Using MBE to Speed a Verified Graph Pathfinder",
 booktitle    = "ACL2 Workshop 2003",
)
@misc(OpenCL,
 author       = "Khronos Group",
 title        = "OpenCL --- The Open Standard for Parallel Programming of Heterogeneous Systems",
 url          = "http://www.khronos.org/opencl",
)
@inproceedings(Hardin2009a,
 author       = "David S. Hardin and Samuel S. Hardin",
 year         = "2009",
 title        = "Efficient, Formally Verifiable Data Structures using ACL2 Single-Threaded Objects for High-Assurance Systems",
 editor       = "S. Ray and D. Russinoff",
 booktitle    = "Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications",
 publisher    = "ACM",
 pages        = "100 -- 105",
 doi          = "10.1145/1637837.1637853",
)
@inproceedings(Harish2007,
 author       = "Parwan Harish and P.J. Narayanan",
 year         = "2007",
 title        = "Accelerating Large Graph Algorithms on the GPU using CUDA",
 booktitle    = "IEEE High Performance Computing -- HiPC 2007",
 series       = "Lecture Notes in Computer Science",
 volume       = "4873",
 publisher    = "Springer",
 pages        = "197--208",
 doi          = "10.1007/978-3-540-77220-0\_21",
)
@misc(HarishWeb,
 author       = "Pawan Harish",
 title        = "Graph Algorithms on CUDA (2007-2011)",
 url          = "http://researchweb.iiit.ac.in/~harishpk",
)
@misc(CUDA,
 author       = "NVIDIA Inc.",
 title        = "CUDA Parallel Programming and Computing Platform",
 url          = "http://www.nvidia.com/object/cuda/home\_new.html",
)
@book(ACL2book,
 author       = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
 year         = "2000",
 title        = "Computer-Aided Reasoning: An Approach",
 publisher    = "Kluwer Academic Publishers",
 doi          = "10.1007/978-1-4757-3188-0",
)
@inproceedings(PUG,
 author       = "G. Li and G. Gopalakrishnan",
 year         = "2010",
 title        = "Scalable SMT-based verification of GPU Kernel Functions",
 booktitle    = "FSE 2010",
 doi          = "10.1145/1882291.1882320",
)
@misc(CommonLispHyperSpec,
 author       = "LispWorks Ltd.",
 title        = "Common Lisp HyperSpec",
 url          = "http://www.lispworks.com/documentation/HyperSpec/Front/index.htm",
)
@inproceedings(mooregraph,
 author       = "J Strother Moore",
 year         = "2000",
 title        = "An Exercise in Graph Theory",
 booktitle    = "Computer-Aided Reasoning: ACL2 Case Studies",
 publisher    = "Kluwer Academic Publishers",
 doi          = "10.1007/978-1-4757-3188-0\_5",
)
@inproceedings(Dijkstra-SSSP-ACL2,
 author       = "J Strother Moore and Q. Zhang",
 year         = "2005",
 title        = "Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2",
 editor       = "J. Hurd and T. Melham",
 booktitle    = "18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005",
 series       = "Lecture Notes in Computer Science",
 volume       = "3603",
 publisher    = "Springer",
 pages        = "373--384",
 doi          = "10.1007/11541868\_24",
)
@inproceedings(ACL2p,
 author       = "David L. Rager",
 year         = "2006",
 title        = "Adding parallelism capabilities to ACL2",
 booktitle    = "Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications",
 series       = "ACL2 '06",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "90--94",
 doi          = "10.1145/1217975.1217994",
)
@inproceedings(Wilding00,
 author       = "Matthew Wilding",
 year         = "2000",
 title        = "Using a Single-Threaded Object to Speed a Verified Graph Pathfinder",
 booktitle    = "ACL2 Workshop 2000",
 note         = "Available as University of Texas Dept. of CS TR 00-29",
)