Bibliografía y lecturas

Actualizado el 16 de agosto de 2026

Las referencias completas de lo que se cita a lo largo del texto, y las obras de referencia a las que acudir cuando aquí se ha resumido lo que en el original ocupa un capítulo.

E.1 Obras de referencia

Tres tratados cubren el campo entre los tres, y cada uno aporta algo que los otros dos no tienen.

Anders Møller y Michael I. Schwartzbach, Static Program Analysis. Departamento de Ciencias de la Computación, Universidad de Aarhus, 2025, 210 páginas. Licencia Creative Commons BY-NC-ND 4.0. Material docente en revisión continua, disponible en abierto, con una implementación en Scala del lenguaje TIP y de los análisis descritos. Es el más pedagógico de los tres: construye toda la teoría sobre un lenguaje juguete diminuto, lo que permite ver los algoritmos funcionando de principio a fin sin ahogarse en detalles del lenguaje.
Flemming Nielson, Hanne Riis Nielson y Chris Hankin, Principles of Program Analysis. Springer-Verlag, 1999, 452 páginas; segunda impresión corregida, 2005. Es la obra formal de referencia. Su aportación decisiva es demostrar que los cuatro grandes enfoques —análisis de flujo de datos, análisis basado en restricciones, interpretación abstracta y sistemas de tipos y efectos— son cuatro dialectos de una misma cosa. Ahí están el desarrollo completo de los monotone frameworks, los teoremas de corrección, el diseño sistemático de conexiones de Galois y el estudio de la complejidad algorítmica.
Fabrice Rastello (coord.), con Benoît Dupont de Dinechin, Florent Bouchez Tichadou y una veintena de autores más, SSA-based Compiler Design. Springer, 2022; el borrador circuló en abierto desde 2018. Es el único tratamiento completo de la forma SSA en formato libro: construcción, destrucción, propiedades, sabores, extensiones para memoria y arrays, y su uso en generación de código real. Es también la más directamente aplicable al análisis de binarios, porque SSA es la representación intermedia que usan Hex-Rays, Binary Ninja y angr, y sus extensiones para memoria con alias resuelven el problema que plantea un binario, donde toda variable es memoria hasta que se demuestre lo contrario.

Para el lado del compilador, los dos manuales clásicos siguen siendo útiles: Aho, Sethi y Ullman, Compilers: Principles, Techniques, and Tools (1986), y Muchnick, Advanced Compiler Design and Implementation (1997).

E.2 Fundamentos y decidibilidad

A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, 1937.
H. G. Rice, Classes of recursively enumerable sets and their decision problems, Trans. AMS, 1953.
E. W. Dijkstra, Notes on structured programming, 1970.
B. Knaster, Un théorème sur les fonctions d'ensembles, 1928.
A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 1955.
S. C. Kleene, Introduction to Metamathematics, 1952.

E.3 Análisis de flujo de datos

F. E. Allen, Control flow analysis, 1970.
G. A. Kildall, A unified approach to global program optimization, POPL 1973.
M. S. Hecht y J. D. Ullman, Flow graph reducibility, SIAM J. Comput., 1972.
J. B. Kam y J. D. Ullman, Global data flow analysis and iterative algorithms, JACM 1976.
J. B. Kam y J. D. Ullman, Monotone data flow analysis frameworks, Acta Informatica 1977.
M. Sharir y A. Pnueli, Two approaches to interprocedural data flow analysis, 1981.
R. E. Tarjan, Fast algorithms for solving path problems, JACM 1981.
T. Reps, S. Horwitz y M. Sagiv, Precise interprocedural dataflow analysis via graph reachability, POPL 1995.
M. Sagiv, T. Reps y S. Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation, TCS 1996.

E.4 Interpretación abstracta y dominios

P. Cousot y R. Cousot, Abstract interpretation: a unified lattice model…, POPL 1977.
P. Cousot y R. Cousot, Systematic design of program analysis frameworks, POPL 1979.
P. Cousot y R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, 1992.
P. Cousot y N. Halbwachs, Automatic discovery of linear restraints among variables of a program, POPL 1978.
P. Granger, Static analysis of arithmetical congruences, 1989.
F. Bourdoncle, Efficient chaotic iteration strategies with widenings, 1993.
A. Miné, A new numerical abstract domain based on difference-bound matrices, 2001.
A. Miné, The octagon abstract domain, HOSC 2006.
L. Mauborgne y X. Rival, Trace partitioning in abstract interpretation based static analyzers, ESOP 2005.

E.5 Dominadores y estructura del CFG

T. Lengauer y R. E. Tarjan, A fast algorithm for finding dominators in a flowgraph, TOPLAS 1979.
J. Ferrante, K. J. Ottenstein y J. D. Warren, The program dependence graph and its use in optimization, TOPLAS 1987.
K. D. Cooper, T. J. Harvey y K. Kennedy, A simple, fast dominance algorithm, 2001.

E.6 Forma SSA

R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman y F. K. Zadeck, Efficiently computing static single assignment form and the control dependence graph, TOPLAS 1991.
J.-D. Choi, R. Cytron y J. Ferrante, Automatic construction of sparse data flow evaluation graphs, POPL 1991.
M. N. Wegman y F. K. Zadeck, Constant propagation with conditional branches, TOPLAS 1991.
P. Briggs, K. D. Cooper, T. J. Harvey y L. T. Simpson, Practical improvements to the construction and destruction of static single assignment form, SPE 1998.
V. C. Sreedhar, R. D.-C. Ju, D. M. Gillies y V. Santhanam, Translating out of static single assignment form, SAS 1999.
Z. Budimlić et al., Fast copy coalescing and live-range identification, PLDI 2002.
C. S. Ananian, The static single information form, tesis, MIT 1999.
J. Singer, Static program analysis based on virtual register renaming, tesis, Cambridge 2006.
R. Bodik, R. Gupta y V. Sarkar, ABCD: eliminating array bounds checks on demand, PLDI 2000.

E.7 Eliminación de redundancias

E. Morel y C. Renvoise, Global optimization by suppression of partial redundancies, CACM 1979.
B. Alpern, M. N. Wegman y F. K. Zadeck, Detecting equality of variables in programs, POPL 1988.
J. Knoop, O. Rüthing y B. Steffen, Lazy code motion, PLDI 1992.
P. Briggs, K. D. Cooper y L. T. Simpson, Value numbering, SPE 1997.
F. Chow, S. Chan, R. Kennedy, S.-M. Liu, R. Lo y P. Tu, A new algorithm for partial redundancy elimination based on SSA form, PLDI 1997.

E.8 Análisis de punteros y de flujo de control

D. R. Chase, M. Wegman y F. K. Zadeck, Analysis of pointers and structures, PLDI 1990.
O. Shivers, Control-flow analysis of higher-order languages, tesis, CMU 1991.
L. O. Andersen, Program analysis and specialization for the C programming language, tesis, Copenhague 1994.
J. Dean, D. Grove y C. Chambers, Optimization of object-oriented programs using static class hierarchy analysis, ECOOP 1995.
D. F. Bacon y P. F. Sweeney, Fast static analysis of C++ virtual function calls, OOPSLA 1996.
B. Steensgaard, Points-to analysis in almost linear time, POPL 1996.
S. Horwitz, Precise flow-insensitive may-alias analysis is NP-hard, TOPLAS 1997.
V. T. Chakaravarthy, New results on the computability and complexity of points-to analysis, POPL 2003.

E.9 Tipos y efectos

J. R. Hindley, The principal type-scheme of an object in combinatory logic, 1969.
R. Milner, A theory of type polymorphism in programming, JCSS 1978.
L. Damas y R. Milner, Principal type-schemes for functional programs, POPL 1982.
M. Wand, A simple algorithm and proof for type inference, 1987.
M. Tofte y J.-P. Talpin, Region-based memory management, Information and Computation 1997.
B. A. Galler y M. J. Fischer, An improved equivalence algorithm, CACM 1964.

E.10 Generación de código y asignación de registros

A. V. Aho, R. Sethi y J. D. Ullman, Compilers: Principles, Techniques, and Tools, 1986.
L. George y A. W. Appel, Iterated register coalescing, TOPLAS 1996.
S. S. Muchnick, Advanced Compiler Design and Implementation, 1997.
M. Poletto y V. Sarkar, Linear scan register allocation, TOPLAS 1999.
F. Bouchez, A. Darte, C. Guillon y F. Rastello, Register allocation: what does the NP-completeness proof of Chaitin et al. really prove?, 2006.
S. Hack, D. Grund y G. Goos, Register allocation for programs in SSA form, CC 2006.

E.11 Análisis de binarios e ingeniería inversa

C. Cifuentes, Reverse compilation techniques, tesis, Queensland University of Technology, 1994.
J. C. King, Symbolic execution and program testing, CACM 1976.
C. Collberg, C. Thomborson y D. Low, Manufacturing cheap, resilient, and stealthy opaque constructs, POPL 1998.
E. Clarke, O. Grumberg, S. Jha, Y. Lu y H. Veith, Counterexample-guided abstraction refinement, CAV 2000.
G. Balakrishnan y T. Reps, Analyzing memory accesses in x86 executables, CC 2004.
J. Lee, T. Avgerinos y D. Brumley, TIE: Principled reverse engineering of types in binary programs, NDSS 2011.
E. Bodden, Inter-procedural data-flow analysis with IFDS/IDE and Soot, SOAP 2012.
S. Arzt et al., FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps, PLDI 2014.
K. Yakdan, S. Eschweiler, E. Gerhards-Padilla y M. Smith, No more gotos: decompilation using pattern-independent control-flow structuring and semantics-preserving transformations, NDSS 2015.
M. Noonan, A. Loginov y D. Cok, Polymorphic type inference for machine code, PLDI 2016.
Y. Shoshitaishvili et al., SoK: (State of) The art of war: offensive techniques in binary analysis, IEEE S&P 2016.
E. Bauman, Z. Lin y K. W. Hamlen, Superset disassembly: statically rewriting x86 binaries without heuristics, NDSS 2018.

E.12 Documentación de herramientas

Ghidra: la documentación de P-Code y del decompilador forma parte del repositorio del proyecto; el fichero de referencia de las operaciones de P-Code y el documento de arquitectura del decompilador son la mejor descripción pública de un pipeline completo.
VEX: libvex_ir.h en el árbol de Valgrind, y la documentación de pyvex en el proyecto angr.
BAP: documentación de BIL en el repositorio del Binary Analysis Platform de CMU.
Binary Ninja: documentación de la API de LLIL, MLIL, HLIL y de sus formas SSA.