Programming languages, formal methods and software engineering | Computing

The increasing complexity and scale of software poses formidable challenges in terms of reliability, security, performance and productivity. Our faculty tackles these problems by developing innovative techniques in the design and semantics of programming languages; techniques and tools for formal verification, software testing and automated debugging; and models and verification techniques for embedded systems that interact with physical entities.

We are known for theoretical advances such as the Actor competition model; the rewrite logic and associated semantic frameworks; concolic tests for generating automated tests; automated logical reasoning; automated inference of specifications and invariants; and theoretical control techniques for the analysis of cyber-physical systems. We have also produced widely used tools and techniques like the Maude Rewrite Engine; the LLVM compiler infrastructure; HPVM and ApproxHPVM systems for the compilation and approximation of programs executed on heterogeneous systems; K frame; Probfuzz, PSense and AxProf systems to test probabilistic and random calculations; the first complete formalizations of C, Java and Javascript; and regression testing techniques.

Gordon K. Morehouse