Machine learning for executable code in software testing and verification

摘要: Software testing and verification are essential for keeping software systems reliable and safe to use. However, it requires significant manual effort to write and maintain code artifacts needed for testing and verification, ie, tests and proofs. With the pressure for developing software in limited time, developers usually write tests and proofs much later than the code under test/verification, which leaves room for software bugs in unchecked code. Recent advances in machine learning (ML) models, especially large language models (LLMs), can help reduce manual effort for testing and verification. Namely, developers can benefit from ML models’ predictions to write tests and proofs faster. However, existing models understand and generate software code as natural language text, ignoring the unique property of software being executable. Software execution is the process of a computer reading and acting on software code. Our insight is that ML models can greatly benefit from software execution, eg, by inspecting and simulating the execution process, to generate more accurate predictions. Integrating execution with ML models is important for generating tests and proofs because ML models using only syntax-level information do not perform well on these tasks. This dissertation presents the design and implementation of two execution-guided ML models to improve developers’ productivity in writing testing and verification code: TeCo for test completion and Roosterize for lemma naming. First, this dissertation introduces TeCo to aid developers in completing next statements when writing tests, a task we formalized as test completion. TeCo exploits code …