This dataset consists of four ZIP files containing annotated images used for experiments in the research of formal specification and specification-based testing for image recognition in autonomous driving systems. The dataset has been derived and modified from the KITTI dataset. image1.zip: Contains 349 images. These images are part of the first subset used in the experiments. label1.zip: Contains the 2D bounding box annotations for vehicles corresponding to the images in image1.zip. There are 349 annotation files, and in total, 2,736 vehicles are annotated. image2.zip: Contains 1,300 images. These images are part of the second subset used in the experiments. label2.zip: Contains the 2D bounding box annotations for vehicles corresponding to the images in image2.zip. There are 1,300 annotation files, and in total, 5,644 vehicles are annotated. The dataset was utilized in the research project focused on Bounding Box Specification Language (BBSL), a formal specification language designed for image recognition in autonomous driving systems. This research explores specification-based testing methodologies for object detection systems. The BBSL project and related testing tools can be accessed on GitHub: https://github.com/IOKENTOI/BBSL-test. The original KITTI dataset used for modification can be found at [KITTI dataset source link].If you use this dataset, please cite the original KITTI dataset:@inproceedings{Geiger2012CVPR, author = {Andreas Geiger and Philip Lenz and Raquel Urtasun}, title = {Are we ready for Autonomous Driving? The KITTI Vision Benchmark Suite}, booktitle = {Conference on Computer Vision and Pattern Recognition (CVPR)}, year = {2012}}