/ConcolicTesting

Our project enables Concolic Execution, a powerful testing strategy that efficiently explores program paths by combining symbolic and concrete execution techniques. By targeting LLVM bitcode, it offers versatility for testing various languages and utilizes LLVM passes for comprehensive path exploration.

Primary LanguageTeX

Compilers Final Project - Concolic Testing Engine

This project contains the code used in Will and I's final compilers project. The project uses an LLVM transformation pass to instrument LLVM bit code. The resultant new program outputs the programs symbolic constraints as well as their runtime evaluation. We use these constraints as input to a constraint solver, which computes a test input that will drive new path exploration in the instrumented program. This process can be repeated to explore whole programs efficiently.

Project Sections

  • Constraint Solver - Contains the constraint solver which was used in this project.
  • LLVM Passes - Contains both the static and dynamic LLVM passes, which were used to analyze and instrument code, respectively.
  • Test Programs - Contains the test programs and the results which were used to test this project.
  • Report - Contains the final report for this project.

Report

For more information read our final report:

paper

Authors