What is static analysis?
El análisis estático nos permite razonar sobre todas las posibles ejecuciones de un programa. Se da la seguridad sobre cualquier ejecución, antes del despliegue pero las herramientas comerciales gastar un montón de esfuerzo frente a la confusión desarrollador, los falsos positivos, etc
What are potential gotchas regarding proper and improper usage/application of static analysis?
tema principal es la abstracción. La abstracción nos permite escalar y modelar todas las carreras posibles, pero debe ser conservador, tratando de equilibrar la precisión y la escalabilidad. abstracciones de análisis estático no coinciden limpia abstracciones desarrollador
When should you use it, and when shouldn't it be used?
propósito principal es para la prueba de código y de mantenimiento, ya que encaja bien con intuiciones desarrollador. En la práctica, es la forma más común de detección de errores, pero cada prueba explora solo una posible ejecución del sistema. Los desarrolladores que están en la industria de seguridad usan esto como una herramienta principal para explorar errores de código, exploits, etc.
Aquí hay un ejemplo de análisis estático usando la ejecución simbólica donde la idea clave es generalizar las pruebas utilizando variables simbólicas desconocidas en evaluación donde rastreamos estados simbólicos. Si la ruta de ejecución depende de desconocido, utilizamos el ejecutor simbólico. Durante la ejecución simbólica, estamos tratando de determinar si ciertas fórmulas son satisfactorias (por ejemplo, si un punto del programa es accesible, si el acceso a la matriz es A [i] fuera de límites, etc.).
int a = α, b = β, c = γ;
// symbolic
int x = 0, y = 0, z = 0;
if (a) {
x = -2;
}
if (b < 5) {
if (!a && c) { y = 1; }
z = 2;
}
assert(x+y+z!=3)
y el análisis de este sencillo ejemplo de código: 
Éstos son algunos enlaces útiles para resolver SMT/SAT que se utilizan para el análisis de código estático:
SAT solving, SMT solving and Program Verification
List of tools for Static Code Analysis
Symbolic Execution, SAT solving, SMT solving and Program Verification
Symbolic Execution Harvard CS252r
"pruebas de unidad que (en teoría) demuestran que el código realmente funciona." Para no ser pedante (ah, vale, para ser un pedante), las pruebas unitarias no "prueban" nada, ni siquiera "teóricamente". Las pruebas crean confianza en la corrección, pero no pueden cubrir todos los comportamientos del –
"deben integrarse en el proceso de compilación" acordado. Sin embargo, las versiones de depuración y liberación, o una u otra? –
@ChrisConway Untrue; si utiliza pruebas sistemáticas o condiciones pre/post para reducir una función parcial o total dada, puede usar pruebas unitarias para probar exhaustivamente esos casos (y, por lo tanto, tener una prueba inductiva de que el código hace lo que dice que hace). Si bien esto no es fácil para muchas funciones a gran escala o que valgan la pena, seguramente es posible, tanto teórica como prácticamente. – Alice