Template:Program analysis: Difference between revisions
Content deleted Content added
Siddharthist (talk | contribs) Add runtime verification |
not the catman |
||
| (7 intermediate revisions by 3 users not shown) | |||
| Line 20: | Line 20: | ||
* [[Runtime verification]] |
* [[Runtime verification]] |
||
* [[Safety and liveness properties|Safety and liveness]] |
* [[Safety and liveness properties|Safety and liveness]] |
||
* [[Undefined behavior]] |
|||
| group2 = [[Semantics (computer science)|Semantics]] |
| group2 = [[Semantics (computer science)|Semantics]] |
||
| Line 32: | Line 33: | ||
** [[Big Step Semantics|Big-step]] |
** [[Big Step Semantics|Big-step]] |
||
** [[Small Step Semantics|Small-step]] |
** [[Small Step Semantics|Small-step]] |
||
| group2 = Models |
| group2 = [[Model of computation|Models]] |
||
| list2 = |
| list2 = |
||
<!-- These are alphabetical --> |
<!-- These are alphabetical --> |
||
| Line 54: | Line 55: | ||
* [[Data-flow analysis|Data-flow]] |
* [[Data-flow analysis|Data-flow]] |
||
* [[Dependence analysis|Dependence]] |
* [[Dependence analysis|Dependence]] |
||
* [[Effect system]] |
|||
* [[Escape analysis|Escape]] |
* [[Escape analysis|Escape]] |
||
* [[Model checking]] |
* [[Model checking]] |
||
| Line 67: | Line 69: | ||
* [[Dynamic data-flow analysis|Data-flow]] |
* [[Dynamic data-flow analysis|Data-flow]] |
||
** [[Taint tracking]] |
** [[Taint tracking]] |
||
* [[ |
* [[Concolic execution]] |
||
* [[Fuzzing]] |
* [[Fuzzing]] |
||
* [[Invariant inference]] |
* [[Invariant inference]] |
||
| Line 81: | Line 83: | ||
* [[Loop invariant]] |
* [[Loop invariant]] |
||
* [[Program refinement|Refinement]] |
* [[Program refinement|Refinement]] |
||
* [[Side effect (computer science)|Side effect]] |
|||
* [[Soundness]] and [[Completeness (logic)|completeness]] |
* [[Soundness]] and [[Completeness (logic)|completeness]] |
||
* [[Formal specification|Specification]] |
* [[Formal specification|Specification]] |
||
| Line 106: | Line 109: | ||
| list1 = |
| list1 = |
||
<!-- These are alphabetical --> |
<!-- These are alphabetical --> |
||
* [[Constrained |
* [[Constrained Horn clauses|CHC]] |
||
* [[SAT solver|SAT]] |
* [[SAT solver|SAT]] |
||
* [[SMT solver|SMT]] |
* [[SMT solver|SMT]] |
||
| group2 = Lightweight |
| group2 = [[Formal methods#Lightweight formal methods|Lightweight]] |
||
| list2 = |
| list2 = |
||
<!-- These are alphabetical --> |
<!-- These are alphabetical --> |
||
| Line 119: | Line 122: | ||
* [[ACL2]] |
* [[ACL2]] |
||
* [[Agda (programming language)|Agda]] |
* [[Agda (programming language)|Agda]] |
||
* [[Coq]] |
* [[Coq (software)|Coq]] |
||
* [[F*]] |
* [[F*]] |
||
* [[HOL Light]] |
* [[HOL Light]] |
||
| Line 144: | Line 147: | ||
{{documentation|content= |
{{documentation|content= |
||
{{collapsible option}} |
{{collapsible option}} |
||
[[Category:Computer science templates |
[[Category:Computer science templates]] |
||
[[Category:Computer science navigational boxes |
[[Category:Computer science navigational boxes]] |
||
}} |
}} |
||
</noinclude> |
</noinclude> |
||
Latest revision as of 18:44, 5 December 2024
| Key concepts |  | ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Semantics |
| ||||||||||||||
| Analyses |
| ||||||||||||||
| Formal methods |
| ||||||||||||||
Template documentationThis template's initial visibility currently defaults to autocollapse, meaning that if there is another collapsible item on the page (a navbox, sidebar, or table with the collapsible attribute), it is hidden apart from its title bar; if not, it is fully visible.
To change this template's initial visibility, the |state= parameter may be used:
{{Program analysis|state=collapsed}}will show the template collapsed, i.e. hidden apart from its title bar.{{Program analysis|state=expanded}}will show the template expanded, i.e. fully visible.