That's more or less it. Some things you can do:

- Dataflow analysis, to get an idea of the types/range of values you're working with

- Pattern matching to try to identify higher level constructs from math to loops to jump tables.

- Compiler-specific pattern matching to identify things like function entry points

- Signature pattern matching common functions (like C standard library calls), along the lines of what's used in High Level Emulation.

My uni runs a systems class that does the SIC/XE architecture linker/loader in forward and reverse depending on the time of year.

FWIK from classmates who made the decompiler, your post is the jist of it.

I don't think this can get you to a meaningful code, but more of assembly-looking C. It would require some sort of machine learning to guess code fragments with proper variable names, properly nested loops, etc.

variable names are almost certainly a lost cause, but IDA pro is pretty good at recovering control flow, which could be turned into C constructs (didn't Dijkstra prove something about expressing any control flow using structured programming constructs?). You'd probably need a bunch of heuristics to tell the difference between a while loop and a for loop. More ambitious would be trying to un-inline functions, which would require liberal use of the de-optimizer and recognizing common sub-structures.

And with any non-trivial amount of optimization, it would lead to horridly looking HLL code. Compilation is a very "lossy" process when optimizations are turned on.

And if the symbols have been stripped, good luck with generating meaningful identifiers.