Automated program repair (APR) has been gaining ground recently. However, a significant challenge that still remains is test overfitting, in which APR-generated patches plausibly pass the validation test suite but fail to generalize. A common practice to assess the correctness of APR-generated patches is to judge whether they are equivalent to ground truth, i.e., developer-written patches, by either generating additional test cases or employing human manual inspections. The former often requires the generation of at least one test that shows behavioral differences between the APR-patched and developer-patched programs. Searching for this test, however, can be difficult as the search space can be enormous. Meanwhile, the latter is prone to human biases and requires repetitive and expensive manual effort. In this paper, we propose a novel technique,Invalidator, to automatically assess the correctness of APR-generated patches via semantic and syntactic reasoning.Invalidatorleverages program invariants to reason about program semantics while also capturing program syntax through language semantics learned from a large code corpus using a pre-trained language model. Given a buggy program and the developer-patched program,Invalidatorinfers likely invariants on both programs. Then,Invalidatordetermines that an APR-generated patch overfits if: (1) it violates correct specifications or (2) maintains erroneous behaviors from the original buggy program. In case our approach fails to determine an overfitting patch based on invariants,Invalidatorutilizes a trained model from labeled patches to assess patch correctness based on program syntax. The benefit ofInvalidatoris threefold. First,Invalidatorleverages both semantic and syntactic reasoning to enhance its discriminative capability. Second,Invalidatordoes not require new test cases to be generated, but instead only relies on the current test suite and uses invariant inference to generalize program behaviors. Third,Invalidatoris fully automated. We conducted our experiments on a dataset of 885 patches generated on real-world programs in Defects4J. Experiment results show thatInvalidatorcorrectly classified 79% of overfitting patches, accounting for 23% more overfitting patches being detected than the best baseline.Invalidatoralso substantially outperforms the best baselines by 14% and 19% in terms of Accuracy and F-Measure, respectively.

The execution of a software system that runs on top of an Operating System (OS) is usually controlled by the scheduler. Therefore, to accurately verify the system, the scheduling policy needs to be taken into account in the verification. In model checking techniques, the scheduling policy affects the search algorithm to explore the state space to check the behaviors of the system. Existing works try to specify/implement the scheduler(s) along with the set of processes in the specification language(s) used by the model checking tool(s). In reality, many kinds of scheduling policies are used by the OS(s), e.g. round-robin, priority, and first-in-first-out. There are also many variations of these policies, which are usually different from the 'textbook’ ones. That means dealing with the variations of the scheduling policies in model checking is necessary and important. However, because the implementation of the scheduler always starts from scratch, it is error-prone and time-consuming. Therefore, the existing works are difficult to deal with the different scheduling policies. To address this problem, we propose a method that introduces a domain-specific language (DSL) to facilitate the variation of the policies. All necessary information to perform the scheduling tasks is generated automatically from the description of the scheduler. We also introduce a search algorithm using this information to explore the states of the system to verify the behaviors of the system. In this paper, we introduce SSpinJa, a tool in which we implemented this approach. Our tool supports an environment for editing the scheduling policy (in the DSL) and the model checker for verifying the system. The results of our experiments show that a) we can handle different scheduling policies easily, b) we can accurately verify the behaviors of the systems, and c) our approach is also practical.

A concurrent system consists of multiple processes that are run simultaneously. The execution orders of these processes are defined by a scheduler. In model checking techniques, the scheduling policy is closely related to a search algorithm that explores all of system states. To ensure the correctness of the system, the scheduling policy needs to be taken into account during the verification. Current approaches, which use fixed strategies, are only capable of limited kinds of policies and are difficult to extend to handle the variations of the schedulers. To address these problems, we propose a method using a domain-specific language (DSL) for the succinct specification of different scheduling policies. Necessary artifacts are automatically generated from the specification of the policy to analyze the system. We also propose a search algorithm for exploring the system states. Based on this method, we develop a tool to verify the system with different scheduling policies. Our experiments show that we could serve the variations of the schedulers easily and verify systems accurately.