使用严格逻辑学方法对软硬件系统进行规约、分析、验证的研究。软件部分属于 PL 的领域，但是和其它理论 PL 工作（e.g. Type System）的研究理路并不相同。最主要的三个分支领域是：程序分析、程序验证和程序综合。