Formal Methods
INSTAR's formal methods research addresses one of computing's hardest problems: establishing, through mathematical proof rather than empirical testing, that a system does exactly what its specification requires. We investigate theorem proving, model checking, and type-theoretic frameworks as tools for building software and hardware systems where failure is not an acceptable outcome — safety-critical infrastructure, cryptographic protocols, and high-assurance embedded systems.
Theorem Proving & Verification
INSTAR explores interactive theorem proving with tools such as Coq, Lean, and Isabelle alongside automated SMT solvers — examining how mathematical proof can be applied to operating system kernels, cryptographic protocols, and distributed consensus algorithms. A particular research interest is extending verification to domains where correctness arguments have historically been informal: concurrent systems, probabilistic behavior, and software components that incorporate learned models. These are precisely the domains where the gap between "tested" and "verified" carries real consequences for national infrastructure and public safety.
Programming Language Theory & Type Systems
The choice of programming language and type system shapes what classes of error are even expressible — a design decision with long-term consequences for software reliability. INSTAR investigates type-theoretic approaches that encode safety and security constraints as compile-time invariants, abstract interpretation frameworks for static analysis, and the formal semantics foundations — lambda calculus, category theory, denotational semantics — that give language design a rigorous underpinning rather than an empirical one.
This research connects to INSTAR's broader mission across high-assurance computing, AI safety, and quantum software correctness. Early-career researchers with backgrounds in logic, programming languages, or mathematics are encouraged to explore the 12-month INSTAR Consortium Postdoctoral Fellowship at /fellowship/.
OUR PARTNERS
