Wed 26 Jun 2019 10:20 - 10:40 at 229AB - Verification II Chair(s): Michael Norrish

We present the most complete and thoroughly tested formal semantics of x86-64 to date. Our semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture. This totals 3155 instruction variants, corresponding to 774 mnemonics. The semantics is fully executable and has been tested against more than 7,000 instruction-level test cases and the GCC torture test suite. This extensive testing paid off, revealing bugs in both the x86-64 reference manual and other existing semantics. We also illustrate potential applications of our semantics in different formal analyses, and discuss how it can be useful for processor verification.

Wed 26 Jun

pldi-2019-papers
10:00 - 11:00: PLDI Research Papers - Verification II at 229AB
Chair(s): Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia
pldi-2019-papers10:00 - 10:20
Talk
Parosh Aziz AbdullaUppsala University, Sweden, Jatin AroraIIT Bombay, India, Mohamed Faouzi AtigUppsala University, Shankaranarayanan KrishnaIIT Bombay, India
pldi-2019-papers10:20 - 10:40
Talk
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Daejun ParkUniversity of Illinois at Urbana-Champaign, Theodoros KasampalisUniversity of Illinois at Urbana-Champaign, USA, Vikram AdveUniversity of Illinois at Urbana-Champaign, Grigore RosuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached
pldi-2019-papers10:40 - 11:00
Talk
Li ZhouDepartment of Computer Science and Technology, Tsinghua University, Nengkun YuUniversity of Technology Sydney, Australia, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University.
Media Attached