In computational complexity theory, EXPSPACE is the set of all decision problems solvable by a deterministic Turing machine in exponential space, i.e., in space, where is a polynomial function of . Some authors restrict to be a linear function, but most authors instead call the resulting class ESPACE. If we use a nondeterministic machine instead, we get the class NEXPSPACE, which is equal to EXPSPACE by Savitch's theorem.
Dana Stewart Scott is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California. His work on automata theory earned him the Turing Award in 1976, while his collaborative work with Christopher Strachey in the 1970s laid the foundations of modern approaches to the semantics of programming languages. He has worked also on modal logic, topology, and category theory.
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.
A hybrid system is a dynamical system that exhibits both continuous and discrete dynamic behavior – a system that can both flow and jump. Often, the term "hybrid dynamical system" is used, to distinguish over hybrid systems such as those that combine neural nets and fuzzy logic, or electrical and mechanical drivelines. A hybrid system has the benefit of encompassing a larger class of systems within its structure, allowing for more flexibility in modeling dynamic phenomena.
In automata theory, a hybrid automaton is a mathematical model for precisely describing hybrid systems, for instance systems in which digital computational processes interact with analog physical processes. A hybrid automaton is a finite state machine with a finite set of continuous variables whose values are described by a set of ordinary differential equations. This combined specification of discrete and continuous behaviors enables dynamic systems that comprise both digital and analog components to be modeled and analyzed.
The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.
Moshe Ya'akov Vardi is an Israeli mathematician and computer scientist. He is a Professor of Computer Science at Rice University, United States. He is University Professor, the Karen Ostrum George Professor in Computational Engineering, Distinguished Service Professor, and director of the Ken Kennedy Institute for Information Technology. His interests focus on applications of logic to computer science, including database theory, finite model theory, knowledge in multi-agent systems, computer-aided verification and reasoning, and teaching logic across the curriculum. He is an expert in model checking, constraint satisfaction and database theory, common knowledge (logic), and theoretical computer science.
Mihalis Yannakakis is professor of computer science at Columbia University. He is noted for his work in computational complexity, databases, and other related fields. He won the Donald E. Knuth Prize in 2005.
Dexter Campbell Kozen is an American theoretical computer scientist. He is Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. He received his B.A. from Dartmouth College in 1974 and his PhD in computer science in 1977 from Cornell University, where he was advised by Juris Hartmanis. He advised numerous Ph.D. students.
PRISM is a probabilistic model checker, a formal verification software tool for the modelling and analysis of systems that exhibit probabilistic behaviour. One source of such systems is the use of randomization, for example in communication protocols like Bluetooth and FireWire, or in security protocols such as Crowds and Onion routing. Stochastic behaviour also arises in many other computer systems, for example due to equipment failures or unpredictable communication delays. Yet another class of systems amenable to this kind of analysis are biochemical reaction networks.
In computer science, alternating-time temporal logic, or ATL, is a branching-time temporal logic that extends computation tree logic (CTL) to multiple players. ATL naturally describes computations of multi-agent systems and multiplayer video games. Quantification in ATL is over program-paths that are possible outcomes of games. ATL uses alternating-time formulas to construct model-checkers in order to address problems such as receptiveness, realizability, and controllability.
Peter William O'Hearn, formerly a research scientist at Meta, is a Distinguished Engineer at Lacework and a Professor of Computer science at University College London (UCL). He has made significant contributions to formal methods for program correctness. In recent years these advances have been employed in developing industrial software tools that conduct automated analysis of large industrial codebases.
ACM SIGLOG or SIGLOG is the Association for Computing Machinery Special Interest Group on Logic and Computation. It publishes a news magazine, and has the annual ACM-IEEE Symposium on Logic in Computer Science (LICS) as its flagship conference. In addition, it publishes an online newsletter, the SIGLOG Monthly Bulletin, and "maintains close ties" with the related academic journal ACM Transactions on Computational Logic.
Helmut Veith was an Austrian computer scientist who worked on the areas of computer-aided verification, software engineering, computer security, and logic in computer science. He was a Professor of Informatics at the Vienna University of Technology, Austria.
David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.
In model checking, a subfield of computer science, a timed word is an extension of the notion of words, in a formal language, in which each letter is associated with a positive time tag. The sequence of time tag must be non-decreasing, which intuitively means that letters are received. For example, a system receiving a word over a network may associate to each letter the time at which the letter is received. The non-decreasing condition here means that the letters are received in the correct order.
Orna Kupferman is a Professor of Computer Science and former Vice Rector at the Hebrew University of Jerusalem. She was elected to the Academia Europaea in 2016.
