Template:Program analysis: Difference between revisions
Content deleted Content added
Siddharthist (talk | contribs) More links! |
not the catman |
||
| (19 intermediate revisions by 3 users not shown) | |||
| Line 17: | Line 17: | ||
* [[Path explosion]] |
* [[Path explosion]] |
||
* [[Polyvariance]] |
* [[Polyvariance]] |
||
* [[Rice's theorem]] |
|||
* [[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]] |
||
| list2 = |
| list2 ={{Navbox|subgroup |
||
| group1 = Types |
|||
| list1 = |
|||
<!-- These are alphabetical --> |
|||
* [[Axiomatic semantics|Axiomatic]] |
* [[Axiomatic semantics|Axiomatic]] |
||
* [[Denotational semantics|Denotational]] |
* [[Denotational semantics|Denotational]] |
||
| Line 27: | Line 33: | ||
** [[Big Step Semantics|Big-step]] |
** [[Big Step Semantics|Big-step]] |
||
** [[Small Step Semantics|Small-step]] |
** [[Small Step Semantics|Small-step]] |
||
| group2 = [[Model of computation|Models]] |
|||
| list2 = |
|||
<!-- These are alphabetical --> |
|||
* [[Lambda calculus]] |
|||
* [[Petri net]] |
|||
* [[Process calculus]] |
|||
* [[Abstract rewriting system|Rewriting system]] |
|||
* [[State Machine|State machine]] |
|||
* [[Turing machine]] |
|||
}} |
|||
| group3 = Analyses |
| group3 = Analyses |
||
| Line 38: | Line 54: | ||
** [[kCFA (program analysis)|kCFA]] |
** [[kCFA (program analysis)|kCFA]] |
||
* [[Data-flow analysis|Data-flow]] |
* [[Data-flow analysis|Data-flow]] |
||
* [[Dependence analysis|Dependence]] |
|||
* [[Effect system]] |
|||
* [[Escape analysis|Escape]] |
|||
* [[Model checking]] |
* [[Model checking]] |
||
* [[Pointer analysis|Pointer]] |
* [[Pointer analysis|Pointer]] |
||
* [[Shape analysis (program analysis)|Shape]] |
|||
* [[Symbolic execution]] |
* [[Symbolic execution]] |
||
* [[Termination analysis|Termination]] |
* [[Termination analysis|Termination]] |
||
* [[Type system|Type systems]] |
|||
* [[Typestate analysis|Typestate]] |
|||
| group2 = [[Dynamic program analysis|Dynamic]] |
| group2 = [[Dynamic program analysis|Dynamic]] |
||
| list2 = |
| list2 = |
||
| Line 47: | 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 58: | Line 80: | ||
| group1 = Concepts |
| group1 = Concepts |
||
| list1 = |
| list1 = |
||
* [[Curry–Howard correspondence]] |
|||
* [[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]] |
|||
** [[Specification language|Languages]] |
|||
* [[Formal verification|Verification]] |
* [[Formal verification|Verification]] |
||
| group2 = |
| group2 = Logics |
||
| list2 = |
| list2 = |
||
* [[Hoare logic|Hoare]] |
|||
| ⚫ | |||
* [[Incorrectness logic|Incorrectness]] |
|||
* [[Linear logic|Linear]] |
|||
* [[Separation logic|Separation]] |
|||
* [[Temporal logic|Temporal]] |
|||
| group3 = Data structures |
|||
| list3 = |
|||
* [[Binary decision diagram|BDD]] |
|||
* [[E-graph]] |
* [[E-graph]] |
||
* [[Hashcons]] |
* [[Hashcons]] |
||
| ⚫ | |||
| |
| group4 = Tools |
||
| |
| list4 = {{Navbox|subgroup |
||
| group1 = [[Constraint solver|Constraint solvers]] |
| group1 = [[Constraint solver|Constraint solvers]] |
||
| 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 87: | Line 122: | ||
* [[ACL2]] |
* [[ACL2]] |
||
* [[Agda (programming language)|Agda]] |
* [[Agda (programming language)|Agda]] |
||
* [[Coq]] |
* [[Coq (software)|Coq]] |
||
* [[F*]] |
* [[F*]] |
||
* [[HOL Light]] |
* [[HOL Light]] |
||
| Line 110: | Line 145: | ||
}}<noinclude> |
}}<noinclude> |
||
{{documentation|content= |
|||
{{Documentation|}} |
|||
{{collapsible option}} |
|||
[[Category:Computer science templates]] |
|||
[[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.