Detecting Compile-Time Based Unspecified Behavior in C Using CPAchecker

This artifact accompanies the Bachelor’s thesis “Detecting Compile-Time Based Unspecified Behavior in C Using CPAchecker” submitted in September 2025 at LMU Munich, Institute for Informatics. It provides the complete research artifact including: CPAchecker extension with the UnseqBehaviorAnalysisCPA for detecting unsequenced side-effect conflicts Configuration files used in the evaluation (e.g., unseqBehaviorAnalysis.properties, deterministic-execution-order.spc) Benchmark tasks from SV-Benchmarks related to unspecified compile-time behavior XML benchmark definition files (BenchExec test sets) used to run the experiments Experimental results and log files produced during the evaluation This work was carried out under the supervision of Prof. Dr. Dirk Beyer and with advising support from Daniel Baier.