References

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

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org