13 citations · 22 across the 4 of their papers we have counts for
3 papers · 1 filter
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Andreas Lindner, Karl Palmskog, Scott Constable +3
Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when…
TrABin: Trustworthy Analyses of Binaries
Andreas Lindner, Roberto Guanciale, Roberto Metere
Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analy…
Sound Transpilation from Binary to Machine-Independent Code
Roberto Metere, Andreas Lindner, Roberto Guanciale
In order to handle the complexity and heterogeneity of mod- ern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent interm…