High-Assurance Systems | SRI International

Toggle Menu

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

Projects

Binary Fission logo

Binary Fission: Crowd-Sourced Software Verification Program

By playing a game, citizen scientists can help increase reliability of mission-critical software systems.

Xylem illustration showing Eugene the explorer

Xylem: Crowd-Sourced Gaming for Formal Verification

Researchers have created a computer game that could transform the problem of proving software correctness.

CTSRD computer system components

CRASH-Worthy, Trustworthy Systems R&D

SRI and the University of Cambridge are designing, prototyping, and analyzing trustworthy computer systems that can be gradually adopted with high reliability, resilience, and assurance, effectively letting system and application developers ‘wipe the slate clean' in incremental steps.