Related Research Articles
In computer science, static program analysis is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution in the integrated environment.
The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.
Sir Charles Antony Richard Hoare, also known as Tony Hoare or by his initials 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, denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects that describe the meanings of expressions from the languages. Other approaches providing formal semantics of programming languages include axiomatic semantics and operational semantics.
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, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.
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.
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.
In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is functional correctness, which refers to the input-output behavior of the algorithm: for each input it produces an output satisfying the specification.
In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs.
In computing, an effect system is a formal system that describes the computational effects of computer programs, such as side effects. An effect system can be used to provide a compile-time check of the possible effects of the program.
Samson Abramsky is Professor of Computer Science at University College London. He was previously the Christopher Strachey Professor of Computing at Wolfson College, Oxford, from 2000 to 2021.
Clifford "Cliff" B. Jones is a British computer scientist, specializing in research into formal methods. He undertook a late DPhil at the Oxford University Computing Laboratory under Tony Hoare, awarded in 1981. Jones' thesis proposed an extension to Hoare logic for handling concurrent programs, rely/guarantee.
In computer science, an abstract state machine (ASM) is a state machine operating on states that are arbitrary data structures.
Egon Börger is a German-born computer scientist based in Italy.
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.
In computer science, control-flow analysis (CFA) is a static-code-analysis technique for determining the control flow of a program. The control flow is expressed as a control-flow graph (CFG). For both functional programming languages and object-oriented programming languages, the term CFA, and elaborations such as k-CFA, refer to specific algorithms that compute control flow.
In computer science, algebraic semantics is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program specifications in a formal manner.
Ernst-Rüdiger Olderog is a German computer scientist. He is a full professor at the University of Oldenburg in Oldenburg, northern Germany. He heads the Correct Systems Design (CSD) group whose research is focused on programming language theory. Their research goal is methods for the systematic development of correct software for parallel and distributed systems under real-time constraints. In 1994, Olderog was awarded the Leibnitz Prize of the German Research Foundation (DFG) for his work. He authored a number of scientific books and served as editor-in-chief of the journal Acta Informatica and as chairman of the IFIP Working Group 2.2 on Formal Description of Programming Concepts. His work in this Working Group was awarded the IFIP Silver Core in 1998.
In computer science, choreographic programming is a programming paradigm where programs are compositions of interactions among multiple concurrent participants.
References
- 1 2 Probst, Christian W.; Hankin, Chris; Hansen, René Rydhof, eds. (2016), Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, Lecture Notes in Computer Science, vol. 9560, Springer, doi:10.1007/978-3-319-27810-0, ISBN 978-3-319-27810-0
- ↑ Riis, Hanne (1980), "Subclasses of Attribute Grammars", Daimi Report Series (Master's thesis; DAIMI Report Series, 9(114)), 9 (114), Aarhus University, doi: 10.7146/dpb.v9i114.6532
- ↑ Nielson, Hanne Riis (1984), Hoare Logics for Run-Time Analysis of Programs, University of Edinburgh, hdl:1842/15527
- ↑ "Speaker bio sketch: Hanne Riis Nielson", Workshop for Anna´s birthday: Flow Sensitive Security, Icelandic Centre of Excellence in Theoretical Computer Science, Reykjavík University, 17 February 2017, retrieved 2024-08-05
- ↑ Reviews of Principles of Program Analysis:
- Anatoly V.Anisimov, Zbl 0932.68013
- Roberto Giacobazzi (2002), MR 1728440
- ↑ Review of Two-Level Functional Languages: S. Gerber, Zbl 0763.68023
- ↑ Michaelson, Greg (June 2022), "Review of Formal Methods: An Appetizer", Formal Aspects of Computing, 34 (2): 1–2, doi:10.1145/3545181
