主条目：静态程序分析

在程序正确性里，静态分析可以在程序的开发阶段就发现漏洞[2]。这些漏洞通常比测试阶段发现的漏洞更容易修复，因为静态分析可以直接发现漏洞的根源。

由于很多静态分析其实无法确切地判定，因此实现静态分析的机制不总返回正确的结果——要么是返回了一个假阴性（返回“没有发现问题”然而程序其实存在问题）或者是返回了一个假阳性，要么它们不返回错误的结果但是有时候不会终止。尽管它们或多或少地存在种种不足，然而前者可能帮助降低漏洞的数量，而后者则在一些时候可以明确确定程序不受某类漏洞的威胁。

不正确的优化是谁都不希望的，所以在程序优化里，有两类策略来处理无法判定的分析情况：

设计一个优化器时，如果认为它应该很快完成它的任务（例如编译器里的优化器），那么可以用一个削减过的分析算法来保证可以在一个有限的时间内完成，并且保证只做正确的优化。

一个第三方的优化器可能会被设计为永远不会输出一个错误的优化，但是有时候可能在找到正确的优化前永远都不会停下来（可能永远也找不到）。这种时候，开发者可能需要关掉这一工具并且避免它再次在要优化的代码上运行（或者也可以修改代码来避免触发这个工具）。

然而，还有第三种策略有时可以用于一些规范不够完整的语言（比如C语言）。一个做优化的编译器在遇到未定义行为时，可以自主选择如何生成这部分代码。生成的代码可以在运行时做任何事情，甚至可以崩溃。

控制流

编辑

主条目：控制流分析

控制流分析的目的是获取在程序执行时一些特定位置可能调用的函数的信息。这些信息由控制流圖（英语：control flow graph，简称CFG）来表示，其中节点表示程序的指令，边表示控制流。

通过识别代码块和循环，CFG常常被编译器当作优化的起始点。

数据流分析

编辑

主条目：数据流分析

数据流分析收集程序运行到不同位置时各个值的信息和它们随时间变化的信息。这一技巧也常被编译器用来优化代码。

一个有名的数据流分析的例子叫做污点检验，它考虑所有的可能被使用者修改的变量（也就是有“污点”、不安全的变量），并阻止这些变量在被“消毒”前被使用。这一技巧常被用来避免SQL注入攻击。污点检验既可以静态完成也可以动态完成。

抽象释义

编辑

主条目：抽象释义

抽象释义允许在不执行程序时提取出某个可能的执行的信息。

这个信息可以让编译器寻找某条可行的优化路径，也可以证明一个程序不会存在某些问题。

类型系统

编辑

主条目：类型系统

类型系统给程序关联上满足特定条件的类型。类型系统的目的是选出一个编程语言编写的程序的一个子集，使这个子集满足特定的性质。

类型检查——验证一个程序是否被类型系统接受

类型检查被用来限制程序中一个对象如何被使用以及一个对象能做什么。类型检查是由编译器或解释器完成的。类型检查也可以帮助避免如将有符号变量赋值给无符号变量所带来的漏洞。

类型检查可以静态完成（在编译期间），也可以动态完成（在运行时），或者结合二者。

静态类型信息（可以通过类型推论，或者由代码明确给出）也可以被用来做优化，例如把封包的数组替换为未封包的数组。

作用系统

编辑

作用系统（英语：Effect systems）是一类用来给出函数或方法的作用的形式化系统。一个作用（英文：effect）规定了做了什么以及对谁做了——通常称之为作用类型（英文：effect kind）以及作用范围（英文：region）。

模型检查

编辑

模型检查（英语：Model checking）指一类严格、形式化并且自动的检查一个模型（在这里指一段代码的形式化模型，但在其他语境下也可以指一个硬件的模型）是否符合给定规范的方法。基于代码内在状态有限这一特点，且规范和代码都可以被转换为逻辑公式，我们有能力用算法来检查一个系统是否违反规范。