Related Research Articles
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.
Amir Pnueli was an Israeli computer scientist and the 1996 Turing Award recipient.
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.
Ben-Gurion University of the Negev (BGU) is a public research university in Beersheba, Israel. Ben-Gurion University of the Negev has five campuses: the Marcus Family Campus, Beer Sheva; the David Bergmann Campus, Beer Sheva; the David Tuviyahu Campus, Beer Sheva; the Sede Boqer Campus, and Eilat Campus.
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.
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.
Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:
John Charles Reynolds was an American computer scientist.
Dov M. Gabbay is an Israeli logician. He is Augustus De Morgan Professor Emeritus of Logic at the Group of Logic, Language and Computation, Department of Computer Science, King's College London.
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.
Regina Barzilay is an Israeli-American computer scientist. She is a professor at the Massachusetts Institute of Technology and a faculty lead for artificial intelligence at the MIT Jameel Clinic. Her research interests are in natural language processing and applications of deep learning to chemistry and oncology.
Marie-Claude Gaudel is a French computer scientist. She is a professor emerita at the University of Paris-Sud. She helped develop PLUSS language for software specifications and was involved in both theoretical and applied computer science. Gaudel is still active in professional societies.
Grigore Roșu is a computer science professor at the University of Illinois at Urbana-Champaign and a researcher in the Information Trust Institute. He is known for his contributions in runtime verification, the K framework, matching logic, and automated coinduction.
José Meseguer is a Spanish computer scientist, and professor at the University of Illinois at Urbana–Champaign. He leads the university's Formal Methods and Declarative Languages Laboratory.
Patricia Bouyer-Decitre is a French theoretical computer scientist known for her research on timed automata, model checking, and temporal logic. She is a senior researcher for the French National Centre for Scientific Research (CNRS), and director of the Laboratoire Méthodes Formelles of CNRS and the École normale supérieure Paris-Saclay.
Emina Torlak is an American computer scientist and software engineer whose research concerns software verification, program synthesis, and the integration of these techniques into domain-specific languages. She is an associate professor of computer science at the University of Washington, and a senior principal scientist for Amazon Web Services.
Kristin Yvonne Rozier is an American aerospace engineer and computer scientist whose research investigates formal methods including temporal logic and model checking for the formal verification of safety-critical systems, especially those involving air transport, unmanned aerial vehicles, and air traffic control. She is Black & Veatch Associate Professor of Aerospace Engineering, Computer Science, Electrical and Computer Engineering, and Mathematics at Iowa State University, where she heads the Laboratory for Temporal Logic.
Lenore D. Zuck is an Israeli-American computer scientist whose research involves formal methods in software engineering, as well as information privacy. She is a research professor of computer science at the University of Illinois Chicago.
References
- 1 2 3 Dana Fisman: Very short bio , retrieved 2023-03-20
- 1 2 3 4 5 "Dana Fisman", ORCiD, retrieved 2023-03-20
- ↑ Dana Fisman at the Mathematics Genealogy Project
- 1 2 "Invited speaker biographies", LearnAut 2019, retrieved 2023-03-20
- ↑ Computer programming made easier, National Science Foundation, 12 August 2016, retrieved 2023-03-20– via Phys.org
- ↑ Troquard, Nicolas (September 2011), "Learning and practice of the Property Specification Language (review of A Practical Introduction to PSL)", IEEE Design & Test of Computers, 28 (5): 110–111, doi:10.1109/mdt.2011.111, S2CID 19261305
