Shoham Shitrit(University of Rochester) and Sreepathi Pai (University of Rochester)

Formal semantics for instruction sets can be used to validate implementations through formal verification. However, testing is often the only feasible method when checking an artifact such as a hardware processor, a simulator, or a compiler. In this work, we construct a pipeline that can be used to automatically generate a test suite for an instruction set from its executable semantics. Our method mutates the formal semantics, expressed as a C program, to introduce bugs in the semantics. Using a bounded model checker, we then check the mutated semantics to the original for equivalence. Since the mutated and original semantics are usually not equivalent, this yields counterexamples which can be used to construct a test suite. By combining a mutation testing engine with a bounded model checker, we obtain a fully automatic method for constructing test suites for a given formal semantics. We intend to instantiate this on a formal semantics of a portion of NVIDIA’s PTX instruction set for GPUs that we have developed. We will compare to our existing method of testing that uses stratified random sampling and evaluate effectiveness, cost, and feasibility.

View More Papers

NSFuzz: Towards Efficient and State-Aware Network Service Fuzzing

Shisong Qin (Tsinghua University), Fan Hu (State Key Laboratory of Mathematical Engineering and Advanced Computing), Bodong Zhao (Tsinghua University), Tingting Yin (Tsinghua University), Chao Zhang (Tsinghua University)

Read More

Hiding My Real Self! Protecting Intellectual Property in Additive...

Sizhuang Liang (Georgia Institute of Technology), Saman Zonouz (Rutgers University), Raheem Beyah (Georgia Institute of Technology)

Read More

Progressive Scrutiny: Incremental Detection of UBI bugs in the...

Yizhuo Zhai (University of California, Riverside), Yu Hao (University of California, Riverside), Zheng Zhang (University of California, Riverside), Weiteng Chen (University of California, Riverside), Guoren Li (University of California, Riverside), Zhiyun Qian (University of California, Riverside), Chengyu Song (University of California, Riverside), Manu Sridharan (University of California, Riverside), Srikanth V. Krishnamurthy (University of California, Riverside),…

Read More

Clarion: Anonymous Communication from Multiparty Shuffling Protocols

Saba Eskandarian (University of North Carolina at Chapel Hill), Dan Boneh (Stanford University)

Read More