High-Assurance Systems
Mission-critical computer systems rely on secure information sharing and interoperability—and failure can have disastrous consequences. A world leader in the formal verification of computer systems, SRI develops and offers specifications for high-assurance systems software and hardware platforms.
-
Prototype Verification System: a tool that provides rigorous assurance of correctness for mission-critical systems
-
Yices: a high-assurance software program that decides the satisfiability of propositional formulas containing uninterpreted function symbols
-
Symbolic Analysis Laboratory: an environment that uses transition relations to explore and analyze concurrent systems
