Formal methods research at CCIS explores a fundamental question: How do we reason about computation? Developing new methods and tools for the design, verification, validation and analysis of computational systems, our research is crucial for ensuring the safety and reliability of critical systems where the consequences of errors can be devastating. Formal methods research impacts a broad range of areas, including aerospace, cyber security, software, programming languages, databases, embedded, cyber-physical and safety-critical systems.
Areas of investigation:
- Interactive theorem proving
- Decision procedures
- Model checking
- Formal verification
- Numerical stability of programs
- Correct and secure compilation
- Embedded and cyber-physical systems
CCIS researchers are designing novel formal verification tools and techniques that help achieve the highest level of reliability across many different industries. Our research teams work closely with various government and industry partners including DARPA, NSF, SRC, NASA, IBM and Boeing. PhD and Masters students will partner with our researchers for a hands-on experience solving fundamental problems in a variety of important application areas.
- CCIS researchers developed ACL2s, an interactive theorem prover that enables students and experts to reason about systems.
- The formal methods group developed a method to synthesize architectural models of systems that interact with the physical world in real time, enabling model-based design at the earliest stages of the design process and reducing overall development costs.
- In collaboration with DARPA (Defense Against Research Projects Agency), CCIS has played an essential role in designing new methods that can be used to build systems that are highly resistant to cyber attacks.
- Our researchers developed formalization, inference and consistency checking techniques for a variety of systems, including self-controlling software, wireless communication, self-aware systems, the Unified Modeling Language (UML), the Web Ontology Language (OWL), software component composition, situation awareness, decision making processes, information fusion, and the Reference Model of Open Distributed Processing (RM-ODP).
- CCIS researchers showed how to scale the decades-old proof method known as logical relations to realistic languages—with features like memory allocation and mutation, objects, and concurrency—leading to wide use of the technique, e.g., for verifying fine-grained concurrent data structures, correctness of compiler transformations, and soundness of advanced type systems that guarantee information hiding or differential privacy.
- CCIS developed the first proof architecture for verifying compilers in the presence of inter-language linking of compiled code. To date, it is the only such architecture applicable to compilers for typed high-level (non-C- like) languages.