Related Research Articles
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 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.
Michael Oser Rabin is an Israeli mathematician, computer scientist, and recipient of the Turing Award.
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. Named after Israeli national founder David Ben-Gurion, the university was founded in 1969 and currently has five campuses: three in Beersheba, one in Sede Boqer and one in Eilat.
In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automation. In contrast to automatic programming techniques, specifications in program synthesis are usually non-algorithmic statements in an appropriate logical calculus.
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:
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.
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 Guaita 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.
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 was previously professor of computer science at the University of Washington, and is currently 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
