| 1. |
- de Almeida Borges, Ana, et al.
(författare)
-
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
- 2023
-
Ingår i: 14th International Conference on Interactive Theorem Proving, ITP 2023. - : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
-
Konferensbidrag (refereegranskat)abstract
- The Coq Community Survey 2022 was an online public survey of users of the Coq proof assistant conducted during February 2022. Broadly, the survey asked about use of Coq features, user interfaces, libraries, plugins, and tools, views on renaming Coq and Coq improvements, and also demographic data such as education and experience with Coq and other proof assistants and programming languages. The survey received 466 submitted responses, making it the largest survey of users of an interactive theorem prover (ITP) so far. We present the design of the survey, a summary of key results, and analysis of answers relevant to ITP technology development and usage. In particular, we analyze user characteristics associated with adoption of tools and libraries and make comparisons to adjacent software communities. Notably, we find that experience has significant impact on Coq user behavior, including on usage of tools, libraries, and integrated development environments.
|
|
| 2. |
- Martinez, Matias, et al.
(författare)
-
Hyperparameter Optimization for AST Differencing
- 2023
-
Ingår i: IEEE Transactions on Software Engineering. - : Institute of Electrical and Electronics Engineers (IEEE). - 0098-5589 .- 1939-3520. ; 49:10, s. 4814-4828
-
Tidskriftsartikel (refereegranskat)abstract
- Computing the differences between two versions of the same program is an essential task for software development and software evolution research. AST differencing is the most advanced way of doing so, and an active research area. Yet, AST differencing algorithms rely on configuration parameters that may have a strong impact on their effectiveness. In this paper, we present a novel approach named DAT (D iff Auto Tuning) for hyperparameter optimization of AST differencing. We thoroughly state the problem of hyper-configuration for AST differencing. We evaluate our data-driven approach DAT to optimize the edit-scripts generated by the state-of-the-art AST differencing algorithm named GumTree in different scenarios. DAT is able to find a new configuration for GumTree that improves the edit-scripts in 21.8% of the evaluated cases.
|
|
