| NSF Org: |
CNS Division Of Computer and Network Systems |
| Recipient: |
|
| Initial Amendment Date: | May 17, 2017 |
| Latest Amendment Date: | November 14, 2022 |
| Award Number: | 1729603 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Sol Greenspan
CNS Division Of Computer and Network Systems CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2017 |
| End Date: | July 31, 2023 (Estimated) |
| Total Intended Award Amount: | $552,195.00 |
| Total Awarded Amount to Date: | $610,641.00 |
| Funds Obligated to Date: |
FY 2022 = $58,446.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
105 JESSUP HALL IOWA CITY IA US 52242-1316 (319)335-2123 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
IA US 52242-1419 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
CCRI-CISE Cmnty Rsrch Infrstrc, Software & Hardware Foundation |
| Primary Program Source: |
01001718DB NSF RESEARCH & RELATED ACTIVIT |
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
StarExec is a web-accessed compute service that was developed (under a prior NSF grant) as a community resource/infrastructure to support researchers in the field of automatic theorem proving and other research areas that depend on logic-solving methods. Research groups in these areas cannot support their own infrastructure due to the high cost of the hardware and the high degree of specialized expertise needed to run and optimize large-scale solver executions. StarExec users can upload solvers and benchmarks to the system, configure and execute jobs to run selected solvers on selected benchmarks, and collaborate by sharing data and artifacts. The infrastructure was first developed to facilitate solver competitions and now supports a large number of users in many areas of research where logic solvers are used.
This new grant sustains and expands StarExec by providing additional hardware (computing clusters) and human resources at the University of Iowa to meet the growing demand for this infrastructure, as the use of logic solvers expands to new research areas and larger-scale problems. Part of the long-term, sustainability strategy is to create multiple instances of the StarExec software, starting with the University of Miami, which will serve as a demonstration and model for future expansion.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
The StarExec project provides a shared web resource for researchers working in the area of automated theorem proving. In this area, software tools called solvers are used to test whether formulas in different logics or logical theories are valid or not. Logic solving has many applications in different areas of Computer Science, due to the expressive power of logic: problems from diverse fields can be translated into logical formulas, and then solved using solvers.
Research communities have developed around different specific forms of logic or logic-solving problems. StarExec is a resource used by many such communities -- there are currently 16 different ones present on StarExec -- for activities like hosting libraries of benchmark formulas and evaluating solvers on benchmarks. (The "Star" in StarExec indicates that it is for all these communitites, as star in Computer Science is used as a pattern matching everything.) StarExec has a compute cluster of over 275 compute nodes, for running solvers. StarExec users can create jobs to run solvers on benchmark formulas, using these nodes.
For the ten years the project was funded by NSF, across two CRI grants, StarExec hosted over 60 competitions, organized by leaders in the various communities, where solver implementors compete to see whose solver can solve the most formulas the most quickly. The system also averages around 20-40 unique logins per week, handling approximately 500,000 to 750,000 (and sometimes in the millions) solver invocations per week. The system has over 1,300 registered users.
In addition to providing a valuable and heavily used service to the different subcommunities of automated theorem proving, StarExec provided invaluable training opportunities for undergraduates and Master's students at The University of Iowa. Students, at least at The University of Iowa where the system was developed, rarely have the chance to work on a codebase of this size, around 150,000 lines of code in various languages. Also, StarExec is a live running system, with many users. This makes working on it a more real-world coding experience than is usually available to University students. Alumni from the project have gone on to excellent jobs at a variety of companies from Google and Microsoft, to State Farm and John Deere.
Last Modified: 10/02/2023
Modified by: Aaron D Stump
Please report errors in award information by writing to: awardsearch@nsf.gov.
