From MinX to MinC: semantics-driven decompilation of recursive datatypes
- Submitting institution
-
The University of Kent
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 9423
- Type
- E - Conference contribution
- DOI
-
10.1145/2837614.2837633
- Title of conference / published proceedings
- Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL 2016
- First page
- 191
- Volume
- -
- Issue
- -
- ISSN
- 0362-1340
- Open access status
- Out of scope for open access requirements
- Month of publication
- January
- Year of publication
- 2016
- URL
-
https://kar.kent.ac.uk/51097/
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper is significant because it describes the world's first certified decompiler. Many researchers have tried to derive types from binaries, but there is no way of telling if these inferred types have any meaning. We show, not only how to infer types using a new form of systematic, semantic constraint solving, but provide a proof certificate that the types are correct. Funded by GCHQ, the Atomic Weapons Establishment are continuing to invest in the work to recover types from binary programs that verify compliance against nuclear weapon non-proliferation treaties.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -