- author = "Jay Bosamiya and Sydney Gibson and Yao Li and Bryan Parno and Chris Hawblitzel",
- title = "Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language",
- booktitle = "Software Verification - 12th International Conference, {VSTTE} 2020, and 13th International Workshop, {NSV} 2020",
- year = "2020",
- editor = "Maria Christakis and Nadia Polikarpova and Parasara Sridhar Duggirala and Peter Schrammel",
- volume = "12549",
- series = "Lecture Notes in Computer Science",
- pages = "106--123",
- address = "Los Angeles, CA, USA",
- month = jul # " 20-21",
- publisher = "Springer",
- note = "Revised Selected Papers",
- keywords = "genetic algorithms, genetic programming, genetic improvement, Hoare Logic",
- isbn13 = "978-3-030-63618-0",
- timestamp = "Mon, 04 Jan 2021 16:36:23 +0100",
-
biburl = "
https://dblp.org/rec/conf/vstte/BosamiyaGLPH20.bib",
- bibsource = "dblp computer science bibliography, https://dblp.org",
-
DOI = "
10.1007/978-3-030-63618-0_7",
- size = "18 pages",
- abstract = "Hand-optimized assembly language code is often difficult to formally verify. This paper combines Hoare logic with verified code transformations to make it easier to verify such code. This approach greatly simplifies existing proofs of highly optimized OpenSSL-based AES-GCM cryptographic code. Furthermore, applying various verified transformations to the AES-GCM code enables additional platform-specific performance improvements.",
-
notes = "p119 'we developed a genetic algorithm to search for
faster instruction orderings on a given
processor'
cited by \cite{Chuengsatiansup:2022:GI}",
