Transalg: a Tool for Translating Procedural Descriptions of Discrete Functions to SAT
This tool addresses the need for automated SAT encoding in cryptography and formal verification, but it appears incremental as it builds on existing methods for specific functions.
The authors tackled the problem of translating procedural descriptions of discrete functions into SAT encodings by developing the Transalg system, which uses propositional encoding methods and symbolic execution, and they applied it to generate SAT encodings for several cryptographic functions.
In this paper we present the Transalg system, designed to produce SAT encodings for discrete functions, written as programs in a specific language. Translation of such programs to SAT is based on propositional encoding methods for formal computing models and on the concept of symbolic execution. We used the Transalg system to make SAT encodings for a number of cryptographic functions.