Sir Charles Antony Richard Hoare, also known as C. A. R. Hoare, is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and concurrent computing. His work earned him the Turing Award, usually regarded as the highest distinction in computer science, in 1980.
In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, 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 computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language and also influenced the design of programming languages such as Limbo, RaftLib, Erlang, Go, Crystal, and Clojure's core.async.
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.
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 software, a spell checker is a software feature that checks for misspellings in a text. Spell-checking features are often embedded in software or services, such as a word processor, email client, electronic dictionary, or search engine.
The Berkeley Lazy Abstraction Software verification Tool (BLAST) is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces. BLAST employs counterexample-driven automatic abstraction refinement to construct an abstract model that is then model-checked for safety properties. The abstraction is constructed on the fly, and only to the requested precision.
SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field.
Andrew William Roscoe is a Scottish computer scientist. He was Head of the Department of Computer Science, University of Oxford from 2003 to 2014, and was a Professor of Computer Science. He was also Fellow of University College, Oxford until 2024.
Michael David May is a British computer scientist. He is a Professor in the Department of Computer Science at the University of Bristol and founder of XMOS Semiconductor, serving until February 2014 as the chief technology officer.
Michael J. Butler is an Irish computer scientist. As of 2022, he is professor of computer science and Dean of the Faculty of Engineering and Physical Sciences at the University of Southampton, England.
In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state. Otherwise it is said to converge. In domains where computations are expected to be infinite, such as process calculi, a computation is said to diverge if it fails to be productive.
Behavior trees are a formal, graphical modelling language used primarily in systems and software engineering. Behavior trees employ a well-defined notation to unambiguously represent the hundreds or even thousands of natural language requirements that are typically used to express the stakeholder needs for a large-scale software-integrated system.
CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.
Jim Davies is Professor of Software Engineering and current Director of the Software Engineering Programme at the University of Oxford, England.
TAPAs is a tool for specifying and analyzing concurrent systems. Its aim is to support teaching of process algebras. Systems are described as process algebra terms that are then mapped to labeled transition systems (LTSs). Properties can be verified by checking equivalences between concrete and abstract system descriptions or by model checking temporal formulas over the obtained LTS. A key feature of TAPAs that makes it particularly suited for teaching is that it maintains a consistent graphical and textual representation of each system. After a change in the graphic notation, the textual representation is updated immediately; but after textual modifications, the update of the graphical representation has to be manually triggered.
Steve Schneider FBCS, CITP is an English computer scientist and Professor of Security. He is Director of the Surrey Centre for Cyber Security and Associate Dean at the University of Surrey.
Gavin Lowe is a British academic. He is a professor of computer science and tutorial fellow at St Catherine's College, Oxford, a professor at the University of Oxford, and President of the Senior Common Room of St Catherine's College, Oxford. His research interests include computer security, for which he developed the cryptographic protocol analysis tool Casper, and concurrency.
In the context of computer science, the C Bounded Model Checker (CBMC) is a bounded model checker for C programs. It was the first such tool.
