Sites Inria

Version française


Marie Collin - 28/09/2010

Verification of complex systems: the PLANETE team wins first prize at the SAT Race 2010 competition

Illustration Codage

CryptoMiniSat, software for verification of software or complex hardware architectures, won first prize at the SAT Race 2010 international competition.

Verifying the reliability or the proper operation of a piece of software, a process, or a physical component is crucial in many industrial applications.

These verifications can be complex when the system has millions of possible parameters or states for all of the various elements comprising it. A technique for verifying these complex systems involves describing the system in the form of operating constraints and properties (CNF description) then verifying the consistency or "satisfiability" of all of these constraints. This means resolving SAT (Satisfiability) problems.

In order to contribute to the research on this topic, the Planète team in Grenoble has developed a verification software: CryptoMiniSat.
This software (a SAT solver) was specially developed for verifications in cryptography, but it is applicable to any SAT problem.
In July 2010, CryptoMiniSat won the "SAT Race 2010", the international challenge organised for the annual international conference dedicated to SAT problems.

Among the 20 industrial or academic software titles participating in the challenge, CryptoMiniSAT obtained the best resolution and speed performance out of a corpus of 100 test applications from the fields of cryptography and hardware and software verification.

With its 10,000 lines of special code, in addition to the core base software of SAT software, CryptoMiniSat takes into account 15 additional mathematical verification criteria, including:

  • XOR clauses for faster treatment of software verification and cryptography problems
  • More elaborate algorithms to force variables to fixed values
  • A more random search tree to find "satisfiable" solutions more quickly
  • A hybrid estimation of value of clauses for a finer approximation of solutions

Keywords: Software Mate Soos Claude Castelluccia Equipe PLANETE Inria Grenoble - Rhône-Alpes Prizes