In theoretical computer science and mathematics, the theory of computation is the branch that deals with what problems can be solved on a model of computation, using an algorithm, how efficiently they can be solved or to what degree. The field is divided into three major branches: automata theory and formal languages, computability theory, and computational complexity theory, which are linked by the question: "What are the fundamental capabilities and limitations of computers?".
In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically rigorous techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
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.
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.
In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a modal logic-based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians.
Modal logic is a collection of formal systems originally developed and still widely used to represent statements about necessity and possibility. The basic unary (1-place) modal operators are most often interpreted "□" for "Necessarily" and "◇" for "Possibly".
Programming is a form of music production and performance using electronic devices and computer software, such as sequencers and workstations or hardware synthesizers, sampler and sequencers, to generate sounds of musical instruments . It is also frequently used in "modern" pop and rock music from various regions of the world, and sometimes in jazz and contemporary classical music.
Zohar Manna was an Israeli-American computer scientist who was a professor of computer science at Stanford University.
In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. Subsequently, LTL is sometimes called propositional temporal logic, abbreviated PTL. In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic.
Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of regular expressions and syntactic sugaring. It is widely used in the hardware design and verification industry, where formal verification tools and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design.
In computer science, concurrency is the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or at the same time simultaneously partial order, without affecting the final outcome. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems. In more technical terms, concurrency refers to the decomposability of a program, algorithm, or problem into order-independent or partially-ordered components or units of computation.
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
Duration calculus (DC) is an interval logic for real-time systems. It was originally developed by Zhou Chaochen with the help of Anders P. Ravn and C. A. R. Hoare on the European ESPRIT Basic Research Action (BRA) ProCoS project on Provably Correct Systems.
Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.
SNARK, , is a theorem prover for multi-sorted first-order logic intended for applications in artificial intelligence and software engineering, developed at SRI International.
TLA+ is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify programs, especially concurrent systems and distributed systems. TLA+ has been described as exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems; TLA is an acronym for Temporal Logic of Actions.
Logic is the systematic study of valid rules of inference, i.e. the relations that lead to the acceptance of one proposition on the basis of a set of other propositions (premises). More broadly, logic is the analysis and appraisal of arguments.
Metric temporal logic (MTL) is a special case of temporal logic. It is an extension of temporal logic in which temporal operators are replaced by time-constrained versions like until, next, since and previous operators. It is linear-time logic that assumes both the interleaving and fictitious-clock abstractions. It is defined over a point-based weakly-monotonic integer-time semantics. For MTL, the exact complexity of the satisfiability problems is known and independent of interval-based or point-based, synchronous or asynchronous interpretation: EXPSPACE-complete.
In model checking, a subfield of computer science, a signal or timed state sequence is an extension of the notion of words, in a formal language, in which letters are continuously emitted. While a word is traditionally defined as a function from a set of non-negative integers to letters, a signal is a functions from a set of real number to letters. This allow to use formalism similar to the ones of automata theory to deal with continuous signal.
