10th June, 2013, affiliated with CADE-24
The StarExec project is an NSF funded project to design, implement, and operate StarExec, a web service designed for the comparative evaluation of logic solvers (automated theorem provers) on benchmark problems. The $1.85 million budget of the grant is mostly dedicated to purchasing and operating a medium-sized cluster of an anticipated 150 compute nodes, which will be used to run jobs submitted by users of the system. We anticipate users will be members of various logic-solving subcommunities of the broader automated theorem proving community
The StarExec 2013 workshop will bring together logic-solving community leaders, logic solver competition organizers, StarExec power users, and the StarExec organizers, to discuss the current status of the StarExec project. The workshop will have four sessions:
- A status report from the StarExec organizers, and a demonstration of StarExec as it has been developed by the time of the workshop.
- Use of StarExec by the attendees, so they can get a feeling of how well the implementation will meet their solver evaluation needs.
- A feedback session based on the use of StarExec.
- A presentation by the StarExec organizers on the short and medium terms plans for development and use of StarExec.
StarExec 2013 will not invite papers or general attendance. Rather, the workshop will be aimed specifically at the types of researchers described above, to maximize the positive impact on the development and use of StarExec. The NSF grant will provide travel, accomodation, and registration support for 20 participants, 10 from the USA and 10 from overseas.
Organizers
Aaron Stump,
The University of Iowa
Geoff Sutcliffe,
University of Miami
Cesare Tinelli,
The University of Iowa