Template:Program analysis: Difference between revisions
Content deleted Content added
Siddharthist (talk | contribs) Constraint solvers |
not the catman |
||
| (21 intermediate revisions by 3 users not shown) | |||
| Line 11: | Line 11: | ||
| list1 = |
| list1 = |
||
<!-- These are alphabetical --> |
<!-- These are alphabetical --> |
||
* [[Control-flow graph]] |
|||
* [[Correctness (computer science)|Correctness]] |
|||
* [[Hyperproperty|Hyperproperties]] |
* [[Hyperproperty|Hyperproperties]] |
||
* [[Invariant (computer science)|Invariants]] |
|||
| ⚫ | |||
* [[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]] |
||
** [[Categorical semantics]] |
|||
* [[Operational semantics|Operational]] |
* [[Operational semantics|Operational]] |
||
** [[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 30: | Line 50: | ||
<!-- These are alphabetical --> |
<!-- These are alphabetical --> |
||
* [[Abstract interpretation]] |
* [[Abstract interpretation]] |
||
* [[Alias analysis]] |
* [[Alias analysis|Alias]] |
||
* [[ |
* [[Control flow analysis|Control flow]] |
||
* [[ |
** [[kCFA (program analysis)|kCFA]] |
||
* [[Data-flow analysis|Data-flow]] |
|||
* [[Dependence analysis|Dependence]] |
|||
* [[Effect system]] |
|||
* [[Escape analysis|Escape]] |
|||
* [[Model checking]] |
|||
* [[Pointer analysis|Pointer]] |
|||
* [[Shape analysis (program analysis)|Shape]] |
|||
* [[Symbolic execution]] |
|||
* [[Termination analysis|Termination]] |
|||
* [[Type system|Type systems]] |
|||
* [[Typestate analysis|Typestate]] |
|||
| group2 = [[Dynamic program analysis|Dynamic]] |
| group2 = [[Dynamic program analysis|Dynamic]] |
||
| list2 = |
| list2 = |
||
<!-- These are alphabetical --> |
<!-- These are alphabetical --> |
||
* [[Dynamic data-flow analysis]] |
* [[Dynamic data-flow analysis|Data-flow]] |
||
** [[Taint tracking]] |
** [[Taint tracking]] |
||
* [[Concolic execution]] |
|||
* [[Fuzzing]] |
* [[Fuzzing]] |
||
* [[Invariant inference]] |
|||
* [[Program slicing]] |
|||
* [[Software testing|Testing]] |
|||
}} |
}} |
||
| group4 = [[Formal methods]] |
| group4 = [[Formal methods]] |
||
| list4 = {{Navbox|subgroup |
|||
| group1 = Concepts |
|||
| list1 = |
|||
* [[Curry–Howard correspondence]] |
|||
| ⚫ | |||
* [[Program refinement|Refinement]] |
|||
* [[Side effect (computer science)|Side effect]] |
|||
* [[Soundness]] and [[Completeness (logic)|completeness]] |
|||
* [[Formal specification|Specification]] |
|||
** [[Specification language|Languages]] |
|||
* [[Formal verification|Verification]] |
|||
| group2 = Logics |
|||
| 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]] |
|||
* [[Hashcons]] |
|||
* [[Disjoint-set data structure|Union-find]] |
|||
| group4 = Tools |
|||
| list4 = {{Navbox|subgroup |
| 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 59: | Line 122: | ||
* [[ACL2]] |
* [[ACL2]] |
||
* [[Agda (programming language)|Agda]] |
* [[Agda (programming language)|Agda]] |
||
* [[Coq]] |
* [[Coq (software)|Coq]] |
||
* [[F*]] |
* [[F*]] |
||
* [[HOL Light]] |
* [[HOL Light]] |
||
| Line 72: | Line 135: | ||
* [[Prototype Verification System|PVS]] |
* [[Prototype Verification System|PVS]] |
||
* [[Twelf]] |
* [[Twelf]] |
||
}} |
|||
}} |
}} |
||
| Line 81: | 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.