Formal Methods

Software used in critical systems must be high assurance, as undetected errors can have severe and debilitating consequences. Our world-class formal methods researchers use innovative, mathematical approaches to verify software.

 

Galois is a world leader in the use of applied formal methods in the development of high assurance software. Formal methods are mathematically based techniques to prove that a system design or code module is correct for all possible inputs, giving assurance that a class of defects has been eliminated. For software used in critical systems, the consequences of incorrect behavior can be extremely serious, and the application of formal methods is a useful technique to generate evidence that the system can be safely deployed.

Galois employs innovative approaches to specify, model, verify, and monitor critical software based on mathematical approaches to software verification. Our techniques address the problems associated with developing high assurance systems through an iterative approach that applies mathematical formalisms across all phases of development. Galois' staff of formal methods experts has extensive experience in using theorem provers, model checkers, rewriters, and other formal methods tools to generate correctness proofs for software.

 

Galois Contacts

Joe Hendrix
Lee Pike

Read More

  • Joe Hendrix, Deepak Kapur, and Jose Meseguer. Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. In Proceedings of Interactive Theorem Proving, First International Conference (ITP 2010), Lecture Notes in Computer Science 6172, Springer 2010.
  • Levent Erkök, Magnus Carlsson, and Adam Wick. Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol. In Formal Methods in Computer Aided Design Conference, FMCAD'09, Austin, TX, November 2009, IEEE.
  • Darren Abramson and Lee Pike: When formal systems kill: computer ethics and formal methods. Submitted (journal article). Comments solicited!
  • Geoffrey M. Brown and Lee Pike: Automated verification and refinement for physical-layer protocols. Submitted (journal article), 2007.
  • Lee Pike, Don Stewart, and John Van Enk: Autonomous Verification and Validation (position paper). CPS Week 2009 Workshop on Mixed Criticality

Collaborate with Us

Licensing - Obtain a license for one of our advanced technologies.

Research & Development - Solve your toughest problems by exploring new approaches with us.

Training - Learn how to use cutting-edge tools to increase trustworthiness in your critical systems.

Let's Work TogetherStart the Conversation >>