| Issue |
EPJ Web of Conferences
Volume 68, 2014
ICASCE 2013 – International Conference on Advances Science and Contemporary Engineering
|
|
|---|---|---|
| Article Number | 00016 | |
| Number of page(s) | 5 | |
| DOI | https://doi.org/10.1051/epjconf/20146800016 | |
| Published online | 28 March 2014 | |
https://doi.org/10.1051/epjconf/20146800016
Distributed Online Judge System for Interactive Theorem Provers
1 Department of Computer Science, Tokyo Institute of Technology, Ookayama, Meguro, Tokyo 152-8552, Japan
Published online: 28 March 2014
In this paper, we propose a new software design of an online judge system for interactive theorem proving. The distinctive feature of this architecture is that our online judge system is distributed on the network and especially involves volunteer computing. In volunteers’ computers, network bots (software robots) are executed and donate computational resources to the central host of the online judge system. Our proposed design improves fault tolerance and security. We gave an implementation to two different styles of interactive theorem prover, Coq and ACL2, and evaluated our proposed architecture. From the experiment on the implementation, we concluded that our architecture is efficient enough to be used practically.
© Owned by the authors, published by EDP Sciences, 2014
This is an Open Access article distributed under the terms of the Creative Commons Attribution License 2.0, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.