Template:Program analysis
{{Navbox
| name = Program analysis
| title = Program analysis
| bodyclass = hlist
| state = uncollapsed
| image = File:Control flow graph of function with two if else statements.svg
| groupstyle = background:#e5e5ff;
| selected = {{{selected|{{{1|}}}}}}
| group1 = Key
concepts
| list1 =
- Control-flow graph
- Correctness
- Hyperproperties
- Invariants
- Path explosion
- Polyvariance
- Rice's theorem
- Runtime verification
- Safety and liveness
- Undefined behavior
| group2 = Semantics
| list2 ={{Navbox|subgroup
| group1 = Types
| list1 =
| group2 = Models
| list2 =
}}
| group3 = Analyses
| list3 = {{Navbox|subgroup
| group1 = Static
| list1 =
- Abstract interpretation
- Alias
- Control flow
- kCFA
- Data-flow
- Dependence
- Effect system
- Escape
- Model checking
- Pointer
- Shape
- Symbolic execution
- Termination
- Type systems
- Typestate
| group2 = Dynamic
| list2 =
}}
| group4 = Formal
methods
| list4 = {{Navbox|subgroup
| group1 = Concepts
| list1 =
- Curry–Howard correspondence
- Loop invariant
- Refinement
- Side effect
- Soundness and completeness
- Specification
- Languages
- Verification
| group2 = Logics
| list2 =
| group3 = Data structures
| list3 =
| group4 = Tools
| list4 = {{Navbox|subgroup
| group1 = Constraint solvers
| list1 =
| group2 = Lightweight
| list2 =
| group3 = Proof assistants
| list3 =
}}
}}
| belowstyle=font-weight:bold;
| below =
}}
{{Navbox documentation}}
Category:Computer science templates
Category:Computer science navigational boxes
}}