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

Transparency Dictionaries with Succinct Proofs of Correct Operation

Ioanna Tzialla (New York University), Abhiram Kothapalli (Carnegie Mellon University), Bryan Parno (Carnegie Mellon University), Srinath Setty (Microsoft Research)

Read More

Log4shell: Redefining the Web Attack Surface

Douglas Everson (Clemson University), Long Cheng (Clemson University), and Zhenkai Zhang (Clemson University)

Read More

ScriptChecker: To Tame Third-party Script Execution With Task Capabilities

Wu Luo (Peking University), Xuhua Ding (Singapore Management University), Pengfei Wu (School of Computing, National University of Singapore), Xiaolei Zhang (Peking University), Qingni Shen (Peking University), Zhonghai Wu (Peking University)

Read More

COOPER: Testing the Binding Code of Scripting Languages with...

Peng Xu (TCA/SKLCS, Institute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences), Yanhao Wang (QI-ANXIN Technology Research Institute), Hong Hu (Pennsylvania State University), Purui Su (TCA/SKLCS, Institute of Software, Chinese Academy of Sciences; School of Cyber Security, University of Chinese Academy of Sciences)

Read More