Category:Formal methods

From Freepedia

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.

For more information, see the article about [[{{{1|Formal methods}}}]].

Subcategories

There are 9 subcategories to this category.

F Functional programming L Lambda calculus Logic in computer science

L cont. Logic programming S Safety Security T Theorem provers

T cont. Theoretical computer science Type theory

Articles in category "Formal methods"

There are 82 articles in this category.

Formal methods A ACL2 theorem prover Abstract Machine Notation Abstract interpretation Abstract state machine Abstraction (computer science) Action semantics Actor model Ambient calculus Assertion (computing) Automata theory Automated theorem proving Axiomatic semantics B BLAST model checker Bisimulation C CHIC Calculus of Broadcasting Systems Calculus of Communicating Systems Communicating sequential processes D DAEDALUS Denotational semantics Dependability E ESC/Java Esterel F Finite state machine Formal Formal equivalence checking

F cont. Formal semantics of programming languages Formal system Formal verification G Guard (computing) H HOL theorem prover Hoare logic I Interval temporal logic Invariant (computer science) Isabelle theorem prover L LCF theorem prover Lambda calculus Language Of Temporal Ordering Specification Larch Prover Larch family Life-critical system Logic in computer science Loop invariant M Model checking O OBJ OBJ3 Operational semantics P Paris Metro Line 14 Petri net Pi-calculus Postcondition Precondition Predicate calculus Predicate transformer semantics

P cont. Process calculi Production equipment control Program specification Program verification Programming Research Group Property Specification Language Prototype Verification System R Rabbit Model Checker Refinement Reification (computer science) Rewriting S SPARK programming language SPIN model checker Set theory Specification and Design Language Static code analysis Symbolic Analysis Laboratory Syntactic methods T Temporal logic Temporal logic in finite-state verification Turing machine U Unified Modeling Language Uppaal Model Checker V V&V: Verification and Validation VDM specification language Vienna Development Method Z Z notation