# Category:Formal methods

Here is a list of articles in the Formal methods category of the Computing portal that unifies foundations of mathematics and computations using computers.

Pages in this category should be moved to subcategories where applicable. This category may require frequent maintenance to avoid becoming too large. It should directly contain very few, if any, pages and should mainly contain subcategories. |

Formal methods are mathematical approaches to software and hardware computer-based system development from requirements, specification and design through to programming and implementation. They form an important theoretical underpinning for software engineering, especially where safety or security is involved. Formal methods are a useful adjunct to software testing since they help avoid errors and can also give a framework for testing. For industrial use, tool support is required.

## Subcategories

This category has the following 5 subcategories, out of 5 total.

### A

### M

### P

### T

## Pages in category "Formal methods"

The following 97 pages are in this category, out of 97 total.

- Formal methods
*(computing)*

### A

- Abstract state machine
*(computing)* - Abstract state machines
*(computing)* - ABZ Conference
*(computing)* - Algebraic semantics (computer science)
*(computing)* - Algebraic specification
*(computing)* - Algorithm characterizations
*(computing)* - And-inverter graph
*(computing)* - Applicative universal grammar
*(computing)* - Assertion (software development)
*(computing)* - Asynchronous system
*(computing)* - Automated theorem proving
*(computing)*

### B

- B-Method
*(computing)* - BHDL
*(computing)* - Bigraph
*(computing)* - Binary moment diagram
*(computing)* - Bisimulation
*(computing)* - Boolean satisfiability problem
*(computing)* - Business process validation
*(computing)*

### C

- Categorical set theory
*(computing)* - CompCert
*(software)* - Computer-assisted proof
*(computing)* - Concurrency semantics
*(computing)* - Construction and Analysis of Distributed Processes
*(software)* - Continued process verification
*(computing)* - Critical process parameters
*(computing)*

### D

- Dependability
*(computing)* - Design space verification
*(computing)* - Direct function
*(computing)* - DREAM
*(software)* - Dynamic timing verification
*(computing)*

### E

- E-LOTOS
*(computing)* - Extended finite-state machine
*(computing)* - Extended static checking
*(computing)*

### F

- Formal equivalence checking
*(computing)* - Formal specification
*(computing)* - Formal verification
*(computing)*

### G

- Gödel logic
*(computing)*

### H

- High- and low-level
*(computing)* - Hindley–Milner type system
*(computing)* - Homotopy type theory
*(computing)*

### I

- Invariant (computer science)
*(computing)* - Invariant-based programming
*(computing)*

### K

- Knowledge Based Software Assistant
*(computing)*

### L

- Lambda calculus
*(computing)* - Liskov substitution principle
*(computing)* - Logic in computer science
*(computing)* - Loop invariant
*(computing)* - Loop variant
*(computing)* - Lustre (programming language)
*(computing)*

### M

- McCarthy 91 function
*(computing)* - Model-based specification
*(computing)* - Mondex
*(computing)*

### O

- Oracle Unified Method
*(computing)*

### P

- PlusCal
*(computing)* - POPLmark challenge
*(computing)* - Postcondition
*(computing)* - Precondition
*(computing)* - Predicate transformer semantics
*(computing)* - Predicative programming
*(computing)* - Prentice Hall International Series in Computer Science
*(computing)* - Process performance qualification protocol
*(computing)* - Process qualification
*(computing)* - Process validation
*(computing)* - Production equipment control
*(computing)* - Proof-carrying code
*(computing)* - Provably Secure Operating System
*(computing)*

### Q

- QED manifesto
*(computing)*

### R

- Rational Unified Process
*(computing)* - RCOS (computer sciences)
*(computing)* - Refinement (computing)
*(computing)* - Refinement calculus
*(computing)* - Regulated rewriting
*(computing)* - Retiming
*(computing)* - Retrenchment (computing)
*(computing)* - Robbins algebra
*(computing)* - Runtime verification
*(computing)*

### S

- Safety-critical system
*(computing)* - Satisfiability modulo theories
*(computing)* - Semantics (computer science)
*(computing)* - Set theory
*(computing)* - SIGNAL (programming language)
*(computing)* - SLAM project
*(computing)* - State space enumeration
*(computing)* - Static timing analysis
*(computing)* - Statistical static timing analysis
*(computing)* - Strict function
*(computing)* - Stuttering equivalence
*(computing)* - Symbolic simulation
*(computing)* - Syntactic methods
*(computing)*

### T

- TLA+
*(computing)* - Turing machine
*(computing)*

### U

- UML state machine
*(computing)*

### V

- Software verification and validation
*(computing)* - Verification and validation of computer simulation models
*(computing)* - Verification condition generator
*(computing)* - Vienna Development Method
*(computing)*