x86 is an instruction set architecture from Intel.
Notes related to x86 architecture
Capstone disassembler, Instruction set architecture, Intel, Remill binary lifting library, reopt binary lifter, SAGE verifier, SecondWrite binary lifter, XED x86 encoding/decoding library, zydis x86 decoder/disassembler library
Papers related to x86 architecture
- A compiler-level intermediate representation based binary analysis and rewriting system [anand:eurosys:2013]
- An in-depth analysis of disassembly on full-scale x86/x64 binaries [andriesse:usenix:2016]
- Specification of Intel IA-32 using an architecture description language [bastian:adl:2005]
- BHive: A benchmark suite and measurement framework for validating x86-64 basic block performance models [chen:iiswc:2019]
- A complete formal semantics of x86-64 user-level instruction set architecture [dasgupta:pldi:2019]
- Scalable validation of binary lifters [dasgupta:pldi:2020]
- Formal specification of the x86 instruction set architecture [degenbaev:phd:2012]
- Abstract stobjs and their application to ISA modeling [goel:acl2:2013]
- Balancing automation and control for formal verification of microprocessors [goel:cav:2021]
- Verifying x86 instruction implementations [goel:cpp:2020]
- Simulation and formal verification of x86 machine-code programs that make system calls [goel:fmcad:2014]
- Engineering a formal, executable x86 ISA simulator for software verification [goel:pcs:2017]
- Formal verification of application and system programs based on a validated x86 ISA model [goel:phd:2016]
- Using x86isa for microcode verification [goel:spisa:2019]
- GeST: An automatic framework for generating CPU stress-tests [hadjilambrou:ispass:2019]
- Stratified synthesis: Automatically learning the x86-64 instruction set [heule:pldi:2016]
- High-level separation logic for low-level code [jensen:popl:2013]
- Towards a formal model of the x86 ISA [kaufmann:utaustin:2012]
- Symbolic trajectory evaluation: The primary validation vehicle for next generation Intel processor graphics FPU [kirankumar:fmcad:2012]
- Zsim: A fast architectural simulator for ISA design-space exploration [lifshitz:wish:2011]
- Path-exploration lifting: Hi-fi tests for lo-fi emulators [martignoni:asplos:2012]
- Vx86: x86 assembler simulated in C powered by automated theorem proving [maus:amast:2008]
- RockSalt: Better, faster, stronger SFI for the x86 [morrisett:pldi:2012]
- TALx86: A realistic typed assembly language [morrisett:wcsss:1999]
- Verified just-in-time compiler on x86 [myreen:popl:2010]
- Verified LISP Implementations on ARM, x86 and PowerPC [myreen:tphols:2009]
- N-version disassembly: Differential testing of x86 disassemblers [paleari:issta:2010]
- MMX technology extension to the Intel architecture [peleg:micro:1996]
- Formally verified big step semantics out of x86-64 binaries [roessle:cpp:2019]
- ZSim: Fast and accurate microarchitectural simulation of thousand-core systems [sanchez:isca:2013]
- The semantics of x86-CC multiprocessor machine code [sarkar:popl:2009]
- x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors [sewell:cacm:2010]
- Data-driven equivalence checking [sharma:oopsla:2012]
- A new verified compiler backend for CakeML [tan:icfp:2016]
- Automatic generation and validation of instruction encoders and decoders [xu:cav:2021]
- Raising binaries to LLVM IR with MCTOLL (WIP paper) [yadavalli:lctes:2019]