Formal Computing and AI Lab.

Our mission: Make the core computing components reliable and flexible 

Approach: 

• Decomposition: Break down large, complex components into smaller, simpler sub-components.

• Abstraction: Implement universal and simple abstractions for similar computing components.

Methodology and tool: Formal verification

• Formal verification, rooted in programming language and proof theories.

• Employs rigorous formal methods to ensure the correctness and reliability of each component.

• Verifying the consistency between each sub-component and its corresponding abstraction.

What's formal verification?  

• The act of proving the correctness of software with respect to a certain formal specification using mathematics (from Wikipedia)

Our mission is to contribute to a safer world as vulnerabilities in software and neural networks continue to grow. This challenge is expected to become even more pressing with the rise of Software 2.0 and ambient computing environments. As we advance toward a future where ubiquitous smart devices increasingly shape our daily lives, the importance of preventing glitches in software and neural networks becomes paramount. Safeguarding sensitive information across diverse applications and dynamic operational settings is crucial. However, we must avoid overburdening these systems with excessive regulations and rigidities that may hinder their potential. Instead, we need a solution that ensures both reliability and flexibility across all core computing components and AI systems.

In response, we are dedicated to researching and developing theories, methodologies, and proofs aimed at significantly reducing, and ultimately eliminating, the costs associated with software failures, recognizing the imperative of securing our digital landscape in the face of evolving technologies. To achieve this ambitious goal, we are currently working with several collaborators listed here.