Related Research Articles
David Lee Chaum is an American computer scientist, cryptographer, and inventor. He is known as a pioneer in cryptography and privacy-preserving technologies, and widely recognized as the inventor of digital cash. His 1982 dissertation "Computer Systems Established, Maintained, and Trusted by Mutually Suspicious Groups" is the first known proposal for a blockchain protocol. Complete with the code to implement the protocol, Chaum's dissertation proposed all but one element of the blockchain later detailed in the Bitcoin whitepaper. He has been referred to as "the father of online anonymity", and "the godfather of cryptocurrency".
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.
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. 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.
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.
Secure two-party computation (2PC) a.k.a. Secure function evaluation is sub-problem of secure multi-party computation (MPC) that has received special attention by researchers because of its close relation to many cryptographic tasks. The goal of 2PC is to create a generic protocol that allows two parties to jointly compute an arbitrary function on their inputs without sharing the value of their inputs with the opposing party. One of the most well known examples of 2PC is Yao's Millionaires' problem, in which two parties, Alice and Bob, are millionaires who wish to determine who is wealthier without revealing their wealth. Formally, Alice has wealth , Bob has wealth , and they wish to compute without revealing the values or .
Ian Robert Horrocks is a professor of computer science at the University of Oxford in the UK and a Fellow of Oriel College, Oxford. His research focuses on knowledge representation and reasoning, particularly ontology languages, description logic and optimised tableaux decision procedures.
Ernest Allen Emerson II, better known as E. Allen Emerson, is an American computer scientist and winner of the 2007 Turing Award. He is Professor and Regents Chair Emeritus at the University of Texas at Austin, United States.
ProVerif is a software tool for automated reasoning about the security properties of cryptographic protocols. The tool has been developed by Bruno Blanchet and others.
Donald W. Loveland is a professor emeritus of computer science at Duke University who specializes in artificial intelligence. He is well known for the Davis–Putnam–Logemann–Loveland algorithm.
Matthew Keith "Matt" Franklin is an American cryptographer, and a professor of computer science at the University of California, Davis.
Inductive programming (IP) is a special area of automatic programming, covering research from artificial intelligence and programming, which addresses learning of typically declarative and often recursive programs from incomplete specifications, such as input/output examples or constraints.
Jayadev Misra is an Indian-born computer scientist who has spent most of his professional career in the United States. He is the Schlumberger Centennial Chair Emeritus in computer science and a University Distinguished Teaching Professor Emeritus at the University of Texas at Austin. Professionally he is known for his contributions to the formal aspects of concurrent programming and for jointly spearheading, with Sir Tony Hoare, the project on Verified Software Initiative (VSI).
David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.
The size-change termination principle (SCT) guarantees termination for a computer program by proving that infinite computations always trigger infinite descent in data values that are well-founded. Size-change termination analysis utilizes this principle in order to solve the universal halting problem for a certain class of programs. When applied to general programs, the principle is intended to be used conservatively, which means that if the analysis determines that a program is terminating, the answer is sound, but a negative answer means "don't know". The decision problem for SCT is PSPACE-complete; however, there exists an algorithm that computes an approximation of the decision problem in polynomial time. Size-change analysis is applicable to both first-order and higher-order functional programs, as well as imperative programs and logic programs. The latter application preceded by four years the general formulation of the principle by Lee et al.
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.
In economics, a budget-additive valuation is a kind of a utility function. It corresponds to a person that, when given a set of items, evaluates them in the following way:
Doron A. Peled is a computer science Professor at Bar-Ilan University. His research interests include formal methods, model checking, program synthesis and runtime verification. With Edmund M. Clarke and Orna Grumberg, he is the coauthor of the book Model Checking and the author of the book Software Reliability Methods.
Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.
The LogicBlox system is a commercial, declarative, incremental logic programming language and deductive database inspired by Datalog. The LogiQL programming language extends Datalog with several features, including stratified negation, aggregation, and a module system. LogicBlox has been used to build pointer analyses for Java.
References
- ↑ "Privacy in the Era of Big Data", Discovery Partners Institute, University of Illinois, retrieved 2023-03-21
- ↑ "Lenore Zuck", Profiles, University of Illinois Chicago Computer Science, retrieved 2023-03-21
- ↑ Author biography from Pnueli, Amir; Zuck, Lenore (March 1986), "Verification of multiprocess probabilistic protocols", Distributed Computing, 1 (1): 53–72, doi:10.1007/bf01843570, S2CID 1317942
- 1 2 Graduate handbook: Faculty, Yale Computer Science, 1997–1998, retrieved 2023-03-21
- ↑ Lenore Zuck at the Mathematics Genealogy Project
- ↑ "Lenore Zuck: Microcode Verification", Talk announcement, Carnegie Mellon University, October 21, 2005, retrieved 2023-03-21
