Transalg: a Tool for Translating Procedural Descriptions of Discrete Functions to SAT

TL;DR

Transalg is a system that converts procedural descriptions of discrete functions into SAT encodings using symbolic execution, facilitating applications like cryptography.

Contribution

It introduces Transalg, a novel tool that automates the translation of procedural programs into SAT encodings based on propositional encoding and symbolic execution.

Findings

Successfully generated SAT encodings for cryptographic functions

Demonstrated effectiveness of symbolic execution in translation process

Enabled new applications in cryptanalysis and formal verification

Abstract

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.