Skip to main navigation Skip to search Skip to main content

Artifact for "Islaris: Verification of Machine Code Against Authoritative ISA Semantics"

  • Michael Sammler (Creator)
  • Angus Hammond (Creator)
  • Rodolphe Lepigre (Creator)
  • Brian Campbell (Creator)
  • Jean Pichon-Pharabod (Creator)
  • Derek Dreyer (Creator)
  • Deepak Garg (Creator)
  • Peter Sewell (Creator)

Dataset

Description

This is the artifact for the PLDI'22 paper "Islaris: Verification of Machine Code Against Authoritative ISA Semantics". It contains the Coq development for the paper.

Data Citation

Sammler, M., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J., Dreyer, D., Garg, D., & Sewell, P. (2022). Artifact for "Islaris: Verification of Machine Code Against Authoritative ISA Semantics". 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '22), San Diego, USA. Zenodo. https://doi.org/10.5281/zenodo.6417959
Date made available1 Mar 2022
PublisherZenodo

Access Dataset

  • 1 Conference contribution

  • Islaris: Verification of Machine Code Against Authoritative ISA Semantics

    Sammler, M., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J., Dreyer, D., Garg, D. & Sewell, P., 9 Jun 2022, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Jhala, R. & Dillig, I. (eds.). ACM, p. 825-840 16 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    File

Cite this