Research in the computing foundations division concerns issues that are fundamental to the understanding of computation and to the development of efficient and well-behaved software. Faculty specifically study the design of algorithms and data structures that lead to efficient computations and the methods by which software can be written or shown to be correct and secure.
Scholarly work in this division can be broadly categorized in the five following areas:
- Design and Analysis of Algorithms and Data Structures involves the development of computer algorithms and data organization methods for fundamental, real-world problems. Research in this area focuses on designing solutions that are efficient in their usage of resources such as time and space as well as on exploring computational limits. Of particular interest to the group are search and optimization problems defined over discrete geometric entities (points, lines, polygons, polyhedra, etc.);
- Computational Logic, Type Theory, Foundations of Mechanized Reasoning involves the investigation of computational and mathematical properties of logical formalisms and algebraic theories that provide the foundations for specification and programming languages. Our work further extends to the use of such formalisms and theories in mechanizing reasoning in mathematics and about software;
- Security and Privacy is concerned with the behaviors of software and computing systems when under attacks, along with mechanisms to prevent, detect, or mitigate the impact of attacks. Specific systems and areas of investigation include system software, emulators and virtual machines, mobile code, and privacy and integrity of communication content and metadata. Methods involved include formal analysis of source and executable code, dynamic testing and instrumentation of executables, virtualization and fault isolation techniques, cryptographic protocols and security proofs, and machine learning and AI applications to these problems;
- Programming Languages uses ideas from logic and type theory in supporting high levels of abstraction in programming and we develop methodologies for constructing programming languages in such a way that they can be safely and systematically extended to include domain specific features. At the implementation level, our work also considers the design of virtual machines and compilation techniques to support extensibility and to realize new and sophisticated programming language features; and
- Software Engineering is concerned with the cost effective development of software systems behaving correctly in their intended operating environment. Our work focuses on requirements specification, formal modeling, verification, automated software engineering, software testing, mobile systems, and safety critical systems.
Labs and selected projects
- Abella: An Interactive Theorem Prover for Reasoning About Specifications of Computations Gopalan Nadathur
- CriSys: Critical Systems Research Group Mats Heimdahl
- Flowcheck Stephen McCamant
- MELT: Minnesota Extensible Language Tools Group Eric Van Wyk
- Research on Layered Manufacturing Ravi Janardan
- Teyjus: an efficient implementation of Lambda Prolog Gopalan Nadathur