Related Research Articles
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 compiler optimization, register allocation is the process of assigning local automatic variables and expression results to a limited number of processor registers.
In computer programming, undefined behavior (UB) is the result of executing a program whose behavior is prescribed to be unpredictable, in the language specification to which the computer code adheres. This is different from unspecified behavior, for which the language specification does not prescribe a result, and implementation-defined behavior that defers to the documentation of another component of the platform.
The Gödel Prize is an annual prize for outstanding papers in the area of theoretical computer science, given jointly by the European Association for Theoretical Computer Science (EATCS) and the Association for Computing Machinery Special Interest Group on Algorithms and Computational Theory. The award is named in honor of Kurt Gödel. Gödel's connection to theoretical computer science is that he was the first to mention the "P versus NP" question, in a 1956 letter to John von Neumann in which Gödel asked whether a certain NP-complete problem could be solved in quadratic or linear time.
In computer science, instruction selection is the stage of a compiler backend that transforms its middle-level intermediate representation (IR) into a low-level IR. In a typical compiler, instruction selection precedes both instruction scheduling and register allocation; hence its output IR has an infinite set of pseudo-registers and may still be – and typically is – subject to peephole optimization. Otherwise, it closely resembles the target machine code, bytecode, or assembly language.
Luca Andrea Cardelli is an Italian computer scientist who is a research professor at the University of Oxford, UK. Cardelli is well known for his research in type theory and operational semantics. Among other contributions, in programming languages, he helped design the language Modula-3, implemented the first compiler for the (non-pure) functional language ML, defined the concept of typeful programming, and helped develop the experimental language Polyphonic C#.
Superoptimization is the process where a compiler automatically finds the optimal sequence for a loop-free sequence of instructions. Real-world compilers generally cannot produce genuinely optimal code, and while most standard compiler optimizations only improve code partly, a superoptimizer's goal is to find the optimal sequence, the canonical form. Superoptimizers can be used to improve conventional optimizers by highlighting missed opportunities so a human can write additional rules.
Thread Level Speculation (TLS), also known as Speculative Multi-threading, or Speculative Parallelization, is a technique to speculatively execute a section of computer code that is anticipated to be executed later in parallel with the normal execution on a separate independent thread. Such a speculative thread may need to make assumptions about the values of input variables. If these prove to be invalid, then the portions of the speculative thread that rely on these input variables will need to be discarded and squashed. If the assumptions are correct the program can complete in a shorter time provided the thread was able to be scheduled efficiently.
Georg Gottlob FRS is an Austrian-Italian computer scientist who works in the areas of database theory, logic, and artificial intelligence and is Professor of Informatics at the University of Calabria. He was Professor at the University of Oxford.
Hypercube-based NEAT, or HyperNEAT, is a generative encoding that evolves artificial neural networks (ANNs) with the principles of the widely used NeuroEvolution of Augmented Topologies (NEAT) algorithm developed by Kenneth Stanley. It is a novel technique for evolving large-scale neural networks using the geometric regularities of the task domain. It uses Compositional Pattern Producing Networks (CPPNs), which are used to generate the images for Picbreeder.orgArchived 2011-07-25 at the Wayback Machine and shapes for EndlessForms.comArchived 2018-11-14 at the Wayback Machine. HyperNEAT has recently been extended to also evolve plastic ANNs and to evolve the location of every neuron in the network.
In computing, compiler correctness is the branch of computer science that deals with trying to show that a compiler behaves according to its language specification. Techniques include developing the compiler using formal methods and using rigorous testing on an existing compiler.
In type theory, bounded quantification refers to universal or existential quantifiers which are restricted ("bounded") to range only over the subtypes of a particular type. Bounded quantification is an interaction of parametric polymorphism with subtyping. Bounded quantification has traditionally been studied in the functional setting of System F<:, but is available in modern object-oriented languages supporting parametric polymorphism (generics) such as Java, C# and Scala.
Peter A. Wegner was a professor of computer science at Brown University from 1969 to 1999. He made significant contributions to both the theory of object-oriented programming during the 1980s and to the relevance of the Church–Turing thesis for empirical aspects of computer science during the 1990s and present. In 2016, Wegner wrote a brief autobiography for Conduit, the annual Brown University Computer Science department magazine.
Extended static checking (ESC) is a collective name in computer science for a range of techniques for statically checking the correctness of various program constraints. ESC can be thought of as an extended form of type checking. As with type checking, ESC is performed automatically at compile time. This distinguishes it from more general approaches to the formal verification of software, which typically rely on human-generated proofs. Furthermore, it promotes practicality over soundness, in that it aims to dramatically reduce the number of false positives at the cost of introducing some false negatives. ESC can identify a range of errors that are currently outside the scope of a type checker, including division by zero, array out of bounds, integer overflow and null dereferences.
In computer science, a Program Dependence Graph (PDG) is a representation of a program's control and data dependencies. It's a directed graph where nodes represent program statements, and edges represent dependencies between these statements. PDG are useful in various program analysis tasks, including optimizations, debugging, and understanding program behavior. These dependencies are used during dependence analysis in optimizing compilers to make transformations so that multiple cores are used, and parallelism is improved.Nodes and edges in a PDG may have attributes associated with them, representing variables read from or written to, or the type of dependency they represent. PDG are used in data flow analysis, slicing, optimization, debugging, and parallelization, providing insights into how program components interact and aiding in understanding and analyzing program behavior.
Automatic bug-fixing is the automatic repair of software bugs without the intervention of a human programmer. It is also commonly referred to as automatic patch generation, automatic bug repair, or automatic program repair. The typical goal of such techniques is to automatically generate correct patches to eliminate bugs in software programs without causing software regression.
David Bacon is an American computer programmer.
Csmith is a test case generation tool. It can generate random C programs that statically and dynamically conform to the C99 standard. It is used for stress-testing compilers, static analyzers, and other tools that process C code. It is a free, open source, permissively licensed C compiler fuzzer developed by researchers at the University of Utah. It was previously called Randprog.
Richard Vuduc is a tenured professor of computer science at the Georgia Institute of Technology. His research lab, The HPC Garage, studies high-performance computing, scientific computing, parallel algorithms, modeling, and engineering. He is a member of the Association for Computing Machinery (ACM). As of 2022, Vuduc serves as Vice President of the SIAM Activity Group on Supercomputing. He has co-authored over 200 articles in peer-reviewed journals and conferences.
References
- ↑ Dietz, Will; Li, Peng; Regehr, John; Adve, Vikram (2015). "Understanding Integer Overflow in C/C++". ACM Transactions on Software Engineering and Methodology. 25 (1): 1–29. CiteSeerX 10.1.1.224.4377 . doi:10.1145/2743019. ISSN 1049-331X. S2CID 62496398.
- ↑ "Csmith". University of Utah. Retrieved 13 April 2016.
- ↑ Yang, Xuejun; Chen, Yang; Eide, Eric; Regehr, John (2011). "Finding and understanding bugs in C compilers". ACM SIGPLAN Notices. 46 (6): 283. CiteSeerX 10.1.1.434.8805 . doi:10.1145/1993316.1993532. ISSN 0362-1340.
