CBMC-GC is a compiler for C programs in the context of secure two-party computation (STC). It compiles a C program that specifies a secure computation into a circuit which can be read in by an STC platform, which then performs the secure computation between two parties A and B:


At the beginning of the compilation CBMC-GC translates the given C program into an intermediate representation featuring a simplified set of control statements. This program in intermediate representation is then translated into a circuit by symbolically executing the program. In order to perform the symbolic execution CBMC-GC unrolls loops and recursive function calls up to a predetermined bound. This bound is either determined automatically via an internal static analysis of the program or is given by the user in case CBMC-GC is not able to discover the bound. During the symbolic execution each statement gets translated into a subcircuit which represents the semantics of the respective statement, the input wires to these subcircuits thereby represent the current program state and the output wires represent the next program state after the effect of the statement was applied to the current program state. Find more details in “Secure Two-party Computations in ANSI C”.


Martin Franz

Martin Franz
CrypTool Project

Nikolaos P. Karvelas

Nikolaos P. Karvelas
CASED, TU Darmstadt

Stefan Katzenbeisser

Stefan Katzenbeisser
CASED, TU Darmstadt

Mailing List

Register here.


CC’14 Presentation (07. April 2014)
cbmc-gc-v0.9.3.tar.gz (28. March 2014)
cbmc-gc-v0.9.3_upd1.pdf (Updated documentation, includes description of CBMC-GC’s circuit format) (30. November 2014)
cbmc-gc-v0.8.tar.gz (14. May 2013)
cbmc-gc-v0.8.pdf (Documentation) (14. May 2013)
CCS’12 Presentation (18. October 2012)

Workshop: PETShop’13

We co-organized the PETShop’13 workshop at CCS in Berlin: http://forsyte.at/petshop-2013/!


[4] CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith
Compiler Construction - 23rd International Conference, CC 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings (Albert Cohen, ed.), volume 8409 of Lecture Notes in Computer Science, pages 244-249, 2014, Springer.
[bibtex] [pdf] [doi]
[3] Challenges in Compiler Construction for Secure Two-Party Computation
Andreas Holzer, Nikolaos P. Karvelas, Stefan Katzenbeisser, Helmut Veith, Martin Franz
(Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith, eds.), pages 3-6, 2013, ACM.
[bibtex] [pdf] [doi]
[2] The first workshop on language support for privacy-enhancing technologies (PETShop'13)
Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith
ACM Conference on Computer and Communications Security (Ahmad-Reza Sadeghi, Virgil D. Gligor, Moti Yung, eds.), pages 1485-1486, 2013, ACM.
[bibtex] [pdf] [doi]
[1] Secure Two-party Computations in ANSI C
Andreas Holzer, Martin Franz, Stefan Katzenbeisser, Helmut Veith
ACM Conference on Computer and Communications Security, pages 772-783, 2012, ACM Press.
[bibtex] [pdf] [doi]


Logo ARiSE CASED Logo TU Darmstadt Logo TU Wien


Andreas Holzer
Technische Universität Wien
Institut für Informationssysteme 184/4
Favoritenstraße 9–11
1040 Wien

Room: HD 03 13 (how to get there)
Phone: +43 (1) 58801 – 184 67
Email: ta.etysrofnull@rezloh
Web: http://forsyte.at/~holzer/

Latest News

Helmut Veith Stipend

The first recipient of the Helmut Veith Stipend for excellent female master’s students in computer science will be presented on March 14 at the following event: "More female students in computer science. Who cares?" Panel discussion with renowned scientists about diversity in STEM Studies March 14, 5:30pm, TU Wien The Helmut Veith Stipend is dedicated […]

Continue reading

WAIT 2016 in Vienna

The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.

Continue reading

Two papers at POPL’17

Two papers co-authored by researchers from our group have been accepted for POPL’17: “Coming to Terms with Quantified Reasoning” by Simon Robillard, Andrei Voronkov, and Laura Kovacs; and “A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms” by Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder

Continue reading

Helmut Veith Stipend

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

LogicLounge in memoriam Helmut Veith

Will robots take away your job? In memory of Helmut Veith, this year’s Conference on Computer Aided Verification (CAV), which takes place in Toronto, will feature a LogicLounge on the effect of automation and artificial intelligence on our jobs.

Continue reading

Full news archive