Exploring how Large Language Models (LLMs) can improve traditional mutation testing techniques by generating more contextually relevant code changes.

Sharing my computer science senior thesis on mutation coverage from Rose-Hulman Institute of Technology.

Generating effective test cases is crucial for thorough software testing. However, creating test cases that capture all potential scenarios can be a complex task. In this blog, I explore the use of Klee symbolic execution engine to create test cases and examine how mutation testing can improve the quality of these cases.

I have been reading and exploring a lot about symbolic execution lately. Very fascinating stuff. Reading about it is one thing, but actually implementing it is another. I decided to build a tiny symbolic executor in Python with less than 70 lines of code to get a better understanding of how it actually works. I will be using the Z3 Theorem Prover to solve the constraints generated by the symbolic execution executor.

Today I will explain Z3 Theorem Prover, a sophisticated theorem prover developed by Microsoft Research. Renowned for its efficacy in software verification and complex problem-solving, Z3 stands out for its accurate solutions and efficient problem-solving algorithms.