In the past few years, there has been a notable shift in the open science landscape as more countries and international agencies release recommendations and implementation guidelines for open scholarship [1][2][3][4][5][6][7].In August 2022, the US White House Office of Science and Technology (OSTP) released a memo [8] with guidance that all federally funded research articles be (1) open access and (2) include sharing of underlying datasets in public repositories.The global open scholarship conversation has shifted from making a case for open science to developing operational workflows to assess, monitor, and enforce open policies that can normalize, simplify, and streamline these processes for use in daily research practice.As various workflows are proposed, there is a need for collective action across funders, institutions, and governments to align on open science policies and practices to reduce the cost and friction of adoption [9][10][11][12].Here, we examine the practices of the Aligning Science Across Parkinson's (ASAP) initiative [13], whose mission is to accelerate the pace of discovery and inform the path to a cure for Parkinson's disease through collaboration, research-enabling resources, and data sharing [14,15].ASAP was conceived through an open-by-design framework from the start.To learn more, please see the ASAP Blueprint for Collaborative Open Science [16], which provides a detailed overview of the ASAP open science policies, templates, and reports.Grantees within the ASAP Collaborative Research Network (CRN), an international, multidisciplinary, and multi-institutional network of collaborating investigators, are already required to be compliant with the recommendations of the OSTP memo by adhering to ASAP's open science policies [17].For example, ASAP requires the posting of a preprint at the time of (or before) article submission, immediate open access for all publications, and a mandatory CC-BY license.Additionally, at the time of publication, all underlying research outputs (protocols, code, datasets) must be posted to a FAIR repository [18,19] and all research outputs from ASAP-funded research must have DOIs or other appropriate identifiers, such as RRIDs for material resources, appropriately linked to the manuscript (see Table 1 for list of identifier types).Here, we evaluate the feasibility, ease, impact, and improvement to our open science policies as they were implemented within the ASAP CRN program and discuss our lessons learned to assist other funders and institutions considering open science implementation.

In this article, we propose a unified framework for designing static analysers based on program synthesis . For this purpose, we identify a fragment of second-order logic with restricted quantification that is expressive enough to model numerous static analysis problems (e.g., safety proving, bug finding, termination and non-termination proving, refactoring). As our focus is on programs that use bit-vectors, we build a decision procedure for this fragment over finite domains in the form of a program synthesiser. We provide instantiations of our framework for solving a diverse range of program verification tasks such as termination, non-termination, safety and bug finding, superoptimisation, and refactoring. Our experimental results show that our program synthesiser compares positively with specialised tools in each area as well as with general-purpose synthesisers.

Acceleration is a technique for summarising loops by computing a closed-form representation of the loop behaviour. The closed form can be turned into an accelerator, which is a code snippet that skips over intermediate states of the loop to the end of the loop in a single step. Program analysers rely on invariant generation techniques to reason about loops. The state-of-the-art invariant generation techniques, in practice, often struggle to find concise loop invariants, and, instead, degrade into unrolling loops, which is ineffective for non-trivial programs. In this paper, we evaluate experimentally whether loop accelerators enable existing program analysis algorithm to discover loop invariants more reliably and more efficiently. This paper is the first comprehensive study on the synergies between acceleration and invariant generation. We report our experience with a collection of safe and unsafe programs drawn from the Software Verification Competition and the literature.

Many software model checkers only detect counterexamples with deep loops after exploring numerous spurious and increasingly longer counterexamples. We propose a technique that aims at eliminating this weakness by constructing auxiliary paths that represent the effect of a range of loop iterations. Unlike acceleration, which captures the exact effect of arbitrarily many loop iterations, these auxiliary paths may under-approximate the behaviour of the loops. In return, the approximation is sound with respect to the bit-vector semantics of programs. Our approach supports arbitrary conditions and assignments to arrays in the loop body, but may as a result introduce quantified conditionals. To reduce the resulting performance penalty, we present two quantifier elimination techniques specially geared towards our application. Loop under-approximation can be combined with a broad range of verification techniques. We paired our techniques with lazy abstraction and bounded model checking, and evaluated the resulting tool on a number of buffer overflow benchmarks, demonstrating its ability to efficiently detect deep counterexamples in C programs that manipulate arrays.