86 relations: Abstract interpretation, Algebra of Communicating Processes, Algorithm, Alloy (specification language), Amir Pnueli, Artificial intelligence, Automated planning and scheduling, Automated theorem proving, Büchi automaton, Bernhard Steffen (computer scientist), Binary decision diagram, BLAST model checker, Boolean satisfiability problem, Boost (C++ libraries), Cambridge University Press, CHESS model checker, Combinatorial explosion, Communicating sequential processes, Computability theory, Computation tree logic, Computer hardware, Computer science, Construction and Analysis of Distributed Processes, Counterexample, CPAchecker, Crash (computing), Deadlock, Directed graph, Discrete system, Don't-care term, E. Allen Emerson, ECLAIR, Edmund M. Clarke, FDR (software), Finite-state machine, Formal equivalence checking, Formal verification, Gerard J. Holzmann, Glossary of graph theory terms, Hardware description language, Hybrid system, ISP Formal Verification Tool, Iterative deepening depth-first search, Java Pathfinder, Joseph Sifakis, Leslie Lamport, Linear temporal logic, List of model checking tools, Logic, LTSmin, ..., Markov Reward Model Checker, MCRL2, Message Passing Interface, MIT Press, Mutual exclusion, Node (computer science), NuSMV, Orna Grumberg, Partial order reduction, PAT (model checker), Petri net, PRISM model checker, Program analysis, Promela, Propositional calculus, Rabbit Model Checker, Refinement (computing), Romeo Model Checker, Satplan, Software, Software verification, SPIN model checker, State space enumeration, Static program analysis, Structure (mathematical logic), Symbolic execution, Symbolic simulation, Symbolic trajectory evaluation, TAPAAL Model Checker, TAPAs model checker, Temporal logic, TLA+, Turing Award, Uppaal Model Checker, Vereofy, Vertex (graph theory). Expand index (36 more) » « Shrink index
In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices.
The Algebra of Communicating Processes (ACP) is an algebraic approach to reasoning about concurrent systems.
In mathematics and computer science, an algorithm is an unambiguous specification of how to solve a class of problems.
In computer science and software engineering, Alloy is a declarative specification language for expressing complex structural constraints and behavior in a software system.
Amir Pnueli (אמיר פנואלי; April 22, 1941 – November 2, 2009) was an Israeli computer scientist and the 1996 Turing Award recipient.
Artificial intelligence (AI, also machine intelligence, MI) is intelligence demonstrated by machines, in contrast to the natural intelligence (NI) displayed by humans and other animals.
Automated planning and scheduling, sometimes denoted as simply AI Planning, is a branch of artificial intelligence that concerns the realization of strategies or action sequences, typically for execution by intelligent agents, autonomous robots and unmanned vehicles.
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs.
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs.
Bernhard Steffen (born 31 May 1958 in Kiel, West Germany) is a German computer scientist and professor at the TU Dortmund University, Germany.
In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function.
The Berkeley Lazy Abstraction Software Verification Tool (BLAST) is a software model checking tool for C programs.
In computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated as SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula.
Boost is a set of libraries for the C++ programming language that provide support for tasks and structures such as linear algebra, pseudorandom number generation, multithreading, image processing, regular expressions, and unit testing.
Cambridge University Press (CUP) is the publishing business of the University of Cambridge.
CHESS is a software model checker for finding errors/heisenbugs in multithreaded software by systematic exploration of thread schedules.
In mathematics, a combinatorial explosion is the rapid growth of the complexity of a problem due to how the combinatorics of the problem is affected by the input, constraints, and bounds of the problem.
In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.
Computability theory, also known as recursion theory, is a branch of mathematical logic, of computer science, and of the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees.
Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized.
Computer hardware includes the physical parts or components of a computer, such as the central processing unit, monitor, keyboard, computer data storage, graphic card, sound card and motherboard.
Computer science deals with the theoretical foundations of information and computation, together with practical techniques for the implementation and application of these foundations.
CADP (Construction and Analysis of Distributed Processes) is a toolbox for the design of communication protocols and distributed systems.
In logic, and especially in its applications to mathematics and philosophy, a counterexample is an exception to a proposed general rule or law.
CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs.
In computing, a crash (or system crash) occurs when a computer program, such as a software application or an operating system, stops functioning properly and exits.
In concurrent computing, a deadlock is a state in which each member of a group is waiting for some other member to take action, such as sending a message or more commonly releasing a lock.
In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is a set of vertices connected by edges, where the edges have a direction associated with them.
A discrete system is a system with a countable number of states.
In digital logic, a don't-care term for a function is an input-sequence (a series of bits) for which the function output does not matter.
Ernest Allen Emerson (born June 2, 1954) is a computer scientist and endowed professor at the University of Texas, Austin, United States.
ECLAIR is a commercial static code analysis tool developed by BUGSENG, LLC for automatic analysis, verification, testing and transformation of C and C++ programs.
Edmund Melson Clarke, Jr. (born July 27, 1945) is an American retired computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs.
FDR (Failures-Divergences Refinement) and subsequently FDR2 are refinement checking software tools, designed to check formal models expressed in Communicating sequential processes (CSP).
A finite-state machine (FSM) or finite-state automaton (FSA, plural: automata), finite automaton, or simply a state machine, is a mathematical model of computation.
Formal equivalence checking process is a part of electronic design automation (EDA), commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior.
In the context of hardware and software systems, formal verification is 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.
Gerard J. Holzmann (born 1951) is a Dutch-born American computer scientist and researcher at Bell Labs and NASA, best known as the developer of the SPIN model checker.
This is a glossary of graph theory terms.
In computer engineering, a hardware description language (HDL) is a specialized computer language used to describe the structure and behavior of electronic circuits, and most commonly, digital logic circuits.
A hybrid system is a dynamical system that exhibits both continuous and discrete dynamic behavior – a system that can both flow (described by a differential equation) and jump (described by a state machine or automaton).
ISP ("In-situ Partial Order") is a tool for the formal verification of MPI programs developed within the School of Computing at the University of Utah.
In computer science, iterative deepening search or more specifically iterative deepening depth-first search (IDS or IDDFS) is a state space/graph search strategy in which a depth-limited version of depth-first search is run repeatedly with increasing depth limits until the goal is found.
Java Pathfinder (JPF) is a system to verify executable Java bytecode programs.
Joseph Sifakis (Ιωσήφ Σηφάκης) is a Greek computer scientist with French citizenship,, Evangélia Moussouri, in Écarts d'identités n⁰95-96, ISSN 1252-6665, reprinting information from an interview of Joseph Sifakis in Des grecs, les grecs de Grenoble, Musée Dauphinois, laureate of the 2007 Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his work on model checking.
Leslie B. Lamport (born February 7, 1941) is an American computer scientist.
In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time.
This article lists model checking tools and gives a synthetic overview their functionalities.
Logic (from the logikḗ), originally meaning "the word" or "what is spoken", but coming to mean "thought" or "reason", is a subject concerned with the most general laws of truth, and is now generally held to consist of the systematic study of the form of valid inference.
LTSmin (short for “Minimization and Instantiation of Labelled Transition Systems”) is an award-winning tool-set for manipulation and model checking of state transition systems.
The Markov Reward Model Checker (MRMC) is a model checker for discrete-time and continuous-time Markov reward models.
mCRL2 is a specification language for describing concurrent discrete event systems.
Message Passing Interface (MPI) is a standardized and portable message-passing standard designed by a group of researchers from academia and industry to function on a wide variety of parallel computing architectures.
The MIT Press is a university press affiliated with the Massachusetts Institute of Technology (MIT) in Cambridge, Massachusetts (United States).
In computer science, mutual exclusion is a property of concurrency control, which is instituted for the purpose of preventing race conditions; it is the requirement that one thread of execution never enter its critical section at the same time that another concurrent thread of execution enters its own critical section.
A node is a basic unit used in computer science.
NuSMV is a reimplementation and extension of SMV symbolic model checker, the first model checking tool based on Binary Decision Diagrams (BDDs).
Orna Grumberg (ארנה גרימברג; born April 30, 1952) is an Israeli computer scientist and academic, the Leumi Chair of Science at the Technion.
In computer science, partial order reduction is a technique for reducing the size of the state-space to be searched by a model checking or Automated planning and scheduling algorithm.
PAT (Process Analysis Toolkit) is a self-contained framework for composing, simulating and reasoning of concurrent, real-time systems and other possible domains.
A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems.
PRISM is a probabilistic model checker, a formal verification software tool for the modelling and analysis of systems that exhibit probabilistic behaviour.
In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness.
PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann.
Propositional calculus is a branch of logic.
Rabbit is a model checking tool for real-time systems.
Refinement is a generic term of computer science that encompasses various approaches for producing correct computer programs and simplifying existing programs to enable their formal verification.
Roméo is an integrated tool environment for modeling, validation and verification of real-time systems modeled as time Petri Nets or stopwatch Petri Nets, extended with parameters.
Satplan (better known as Planning as Satisfiability) is a method for automated planning.
Computer software, or simply software, is a generic term that refers to a collection of data or computer instructions that tell the computer how to work, in contrast to the physical hardware from which the system is built, that actually performs the work.
Software verification is a discipline of software engineering whose goal is to assure that software fully satisfies all the expected requirements.
SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion.
In computer science, state space enumeration are methods that consider each reachable program state to determine whether a program satisfies a given property.
Static program analysis is the analysis of computer software that is performed without actually executing programs.
In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations that are defined on it.
In computer science, symbolic execution (also symbolic evaluation) is a means of analyzing a program to determine what inputs cause each part of a program to execute.
In computer science, a simulation is a computation of the execution of some appropriately modelled state-transition system.
Symbolic trajectory evaluation (STE) is a lattice-based model checking technology that uses a form of symbolic simulation.
TAPAAL is a tool for modelling, simulation and verification of Timed-Arc Petri nets developed at Department of Computer Science at Aalborg University in Denmark and it is available for Linux, Windows and Mac OS X platforms.
is a tool for specifying and analyzing concurrent systems, its aim is to support teaching of process algebras.
In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time.
TLA+ (pronounced as tee ell a plus) is a formal specification language developed by Leslie Lamport.
The ACM A.M. Turing Award is an annual prize given by the Association for Computing Machinery (ACM) to an individual selected for contributions "of lasting and major technical importance to the computer field".
UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays etc.). The tool has been developed in collaboration between the Design and Analysis of Real-Time Systems group at Uppsala University, Sweden and Basic Research in Computer Science at Aalborg University, Denmark.
Vereofy is a software model checker for component-based systems for operational correctness.
In mathematics, and more specifically in graph theory, a vertex (plural vertices) or node is the fundamental unit of which graphs are formed: an undirected graph consists of a set of vertices and a set of edges (unordered pairs of vertices), while a directed graph consists of a set of vertices and a set of arcs (ordered pairs of vertices).