Discover published sets by community

A branching-time logic, distinct from LTL, that can specify branching structures like computation trees. Applied in defining and checking properties of reactive systems.

A theoretical construct that represents a computing machine. Used to understand the limits of what can be computed and serves as a standard for computability.

A method to formally specify abstract data types in a sheer algebraic way. Employed in the stepwise refinement and implementation of software systems.

The act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

A modal temporal logic with modalities referring to time, where formulas always interpret paths (or runs) through a model. Used to specify and reason about the temporal aspects within model checking.

A type of finite automaton modeled for infinite inputs. Used to model and check properties of systems that run indefinitely like operating systems.

A family of approaches for formally modeling concurrent systems. Used as a tool for specifying and verification of high-level descriptions of communications between systems.

A data structure that is used to represent and manipulate Boolean functions efficiently. Used in design and verification of hardware and software, primarily in reducing complexity.

A formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. Used to prove the correctness of algorithms.

A theory that provides a framework for constructing abstract models of computer programs and reasoning about their properties. Used mainly for static program analysis.

An automated technique for verifying finite state concurrent systems. Utilized in hardware and software design to find design errors in systems.