ISBN: 978-981-09-5471-0 DOI: 10.18178/wcse.2015.04.048
TRANSALG: A Tool for Translating Procedural Descriptions of Discrete Functions to SAT
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.
Index Terms— SAT encoding, symbolic execution, translator, cryptographic functions.
Ilya Otpuschennikov, Alexander Semenov, Stepan Kochemazov
Institute for System Dynamics and Control Theory SB RAS, RUSSIA
Cite: Ilya Otpuschennikov, Alexander Semenov, Stepan Kochemazov, "TRANSALG: A Tool for Translating Procedural Descriptions of Discrete Functions to SAT," 2015 The 5th International Workshop on Computer Science and Engineering-Information Processing and Control Engineering (WCSE 2015-IPCE), pp. 289-294, Moscow, Russia, April 15-17, 2015.