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

Analyzing and Creating Malicious URLs: A Comparative Study on...

Vincent Drury (IT-Security Research Group, RWTH Aachen University), Rene Roepke (Learning Technologies Research Group, RWTH Aachen University), Ulrik Schroeder (Learning Technologies Research Group, RWTH Aachen University), Ulrike Meyer (IT-Security Research Group, RWTH Aachen University)

Read More

What You See is Not What the Network Infers:...

Yijun Yang (The Chinese University of Hong Kong), Ruiyuan Gao (The Chinese University of Hong Kong), Yu Li (The Chinese University of Hong Kong), Qiuxia Lai (Communication University of China), Qiang Xu (The Chinese University of Hong Kong)

Read More

D-Box: DMA-enabled Compartmentalization for Embedded Applications

Alejandro Mera (Northeastern University), Yi Hui Chen (Northeastern University), Ruimin Sun (Northeastern University), Engin Kirda (Northeastern University), Long Lu (Northeastern University)

Read More

What Storage? An Empirical Analysis of Web Storage in...

Zubair Ahmad (Università Ca’ Foscari Venezia), Samuele Casarin (Università Ca’ Foscari Venezia), and Stefano Calzavara (Università Ca’ Foscari Venezia)

Read More