What is static analysis?
Статический анализ позволяет нам рассуждать обо всех возможных расстрелы программы. Это дает уверенность в любом исполнении, до развертывания, но коммерческие инструменты тратить много усилий дело с замешательства разработчиков, ложных срабатываний и т.д.
What are potential gotchas regarding proper and improper usage/application of static analysis?
Основной проблемой является абстракцией. Абстракция позволяет нам масштабировать и моделировать все возможные прогоны, но они должны быть консервативными, пытаясь сбалансировать точность и масштабируемость. Статические абстракции анализа не чисто соответствуют абстракциям разработчиков
When should you use it, and when shouldn't it be used?
Главной цель для тестирования и обслуживания коды, как это хорошо согласуется с интуицией разработчиков. На практике это наиболее распространенная форма обнаружения ошибок, но каждый тест исследует только одно возможное выполнение системы. Разработчики, работающие в сфере безопасности, используют это как основной инструмент для изучения ошибок кода, эксплойтов и т. Д.
Вот пример статического анализа с использованием символического исполнения, где ключевая идея заключается в обобщении тестирования с использованием неизвестных символических переменных в где мы отслеживаем символические состояния. Если путь выполнения зависит от неизвестного, мы выполняем символический исполнитель. Во время символического выполнения мы пытаемся определить, являются ли определенные формулы выполнимыми (например, какая-то конкретная точка программы достижима, является ли доступ к массиву A [i] за пределы? И т. Д.).
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)
И анализ этого простого примера кода: 
Вот некоторые полезные ссылки для SMT/SAT решателей, которые используются для статического анализа кода:
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
«блок-тесты, которые (теоретически) доказывают, что код действительно работает». Не быть педантом (о, хорошо, быть педантом), модульные тесты не «доказывают» что-либо, даже «теоретически». Тесты укрепляют уверенность в правильности, но они не могут охватить каждое поведение – 2008-09-08 14:16:20
«они должны быть интегрированы в процесс сборки». Однако, отладка и выпуск сборок, или тот или другой? – 2009-09-01 15:23:38
@ChrisConway Untrue; если вы используете систематические доказательства или условия до/после, чтобы сузить данную частичную или общую функцию вниз, вы можете использовать модульные тесты для исчерпывающего доказательства этих случаев (и, следовательно, иметь индуктивное доказательство того, что код выполняет то, что он говорит). Хотя это непросто для многих крупных или стоящих функций, это, безусловно, возможно, как теоретически, так и практически. – Alice 2014-08-11 01:15:40