Ștefan Ciobâcă
Teaching
 Logică pentru Informatică (in Romanian, Winter Semester 2018/2019)
 Logic for Computer Science (English, Winter Semester 2018/2019)
 Logică pentru Informatică (in Romanian, Winter Semester 2017/2018)
 Logic for Computer Science (English, Winter Semester 2017/2018)
Talks
 July 28th, 2018: Presentation on Unification Modulo Builtins at WoLLIC 2018.
 July 14th, 2018: Presentation on A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems at IJCAR 2018 (part of FLOC 2018).
 July 8th, 2018: My coauthor Sebastian Buruiana gave a presentation on Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics at WPTE 2018.
 April, 2018: Presentation on SemanticsParametric Program Equivalence (workinprogress) at Dagstuhl Seminar on Program Equivalence.
 July 8th, 2017: Presentation on Proving reachability modulo theories at FROM 2017.
 May 31st, 2017: Presentation of the short paper Automatically Constructing a Type System from the SmallStep Semantics at TYPES 2017 (additional files) .
 May 15th, 2017: Presentation on RMT: a tool for rewriting modulo theories at INRIA Paris.
 April 11th  April 12th, 2016: Presentation at the Workshop on Program Equivalence.
 April 2nd  April 3rd, 2016: Presentation about proving program equivalence using matching logic at WRLA 2016 as part of the tutorial "Program Verification using Reachability Logic" given by Grigore Roșu, Andrei Ștefănescu and myself.
Publications

Ștefan Ciobâcă, Andrei
Arusoaie, Dorel Lucanu: Unification Modulo
Builtins (WoLLIC 2018).
Combining rewriting modulo an equational theory and SMT solving introduces new challenges in the area of term rewriting. One such challenge is unification of terms in the presence of equations and of uninterpreted and interpreted function symbols. The interpreted function symbols are part of a builtin model which can be reasoned about using an SMT solver. In this article, we formalize this problem, that we call unification modulo builtins. We show that under reasonable assumptions, complete sets of unifiers for unification modulo builtins problems can be effectively computed by reduction to usual Eunification problems and by relying on an oracle for SMT solving.

Ștefan Ciobâcă, Dorel
Lucanu: A Coinductive
Approach to Proving Reachability Properties in Logically Constrained
Term Rewriting Systems (IJCAR 2018; extended technical report).
We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an ordersorted signature modulo builtins. A key feature of the calculus is a circularity proof rule, which allows to obtain finite representations of the infinite coinductive proofs.

Andrei Arusoaie, Ștefan
Ciobâcă, Vlad Crăciun, Dragoș Gavriluț, Dorel Lucanu: A Comparison of Static Analysis Tools
for Vulnerability Detection in C/C++ Code. SYNASC 2017.
Abstract: We describe work that is part of a research project on static code analysis between the Alexandru Ioan Cuza University and Bitdefender. The goal of the project is to develop customized static analysis tools for detecting potential vulnerabilities in C/C++ code. We have so far benchmarked several existing static analysis tools for C/C++ against the Toyota ITC test suite in order to determine which tools are best suited to our purpose. We discuss and compare several quality indicators such as precision, recall and running time of the tools. We analyze which tools perform best for various categories of potential vulnerabilities such as buffer overflows, integer overflow, etc.

Rohit Chadha, Vincent Cheval, Ștefan Ciobâcă, Steve Kremer: Automated Verification of Equivalence Properties of Cryptographic Protocols. ACM Transactions on Computational Logic, 2016. (PDF  technical report  ACM Digital Library)
Abstract: Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryp tographic protocols. As in the applied picalculus, our protocol specification language is parametrized by a firstorder sorted term signature and an equational theory which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under and overapproximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory is generated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into firstorder Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool AKiSs (Active Knowledge in Security Protocols) and has been effec tively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.@article{Chadha:2016:AVE:2996393.2926715, author = {Chadha, Rohit and Cheval, Vincent and Ciob\^{a}c\u{a}, \c{S}tefan and Kremer, Steve}, title = {Automated Verification of Equivalence Properties of Cryptographic Protocols}, journal = {ACM Trans. Comput. Logic}, issue_date = {November 2016}, volume = {17}, number = {4}, month = sep, year = {2016}, issn = {15293785}, pages = {23:123:32}, articleno = {23}, numpages = {32}, url = {http://doi.acm.org/10.1145/2926715}, doi = {10.1145/2926715}, acmid = {2926715}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Applied pi calculus, automated verification, process equivalence, security protocols}, }

Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore
Roșu, A LanguageIndependent Proof System for
Full Program Equivalence. Formal Aspects of Computing,
2016. (SpringerLink)
Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in determin istic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a languageindependent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a statesimilarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known weather the sequence terminates or not; nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).
@Article{CLRRFAOC2016, author="Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Lucanu, Dorel and Rusu, Vlad and Ro{\c{s}}u, Grigore", title="A languageindependent proof system for full program equivalence", journal="Formal Aspects of Computing", year="2016", month="May", day="01", volume="28", number="3", pages="469497", issn="1433299X", doi="10.1007/s0016501603617", url="https://doi.org/10.1007/s0016501603617" }

Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore
Roșu, A Theoretical
Foundation for Programming Languages
Aggregation. WADT 2014 postproceedings, LNCS
9463, 2015. (SpringerLink)
Abstract: Programming languages should be formally specified in order to reason about programs written in them. We show that, given two formally specified programming languages, it is possible to construct the formal semantics of an aggregated language, in which programs consist of pairs of programs from the initial languages. The construction is based on algebraic techniques and it can be used to reduce relational properties (such as equivalence of programs) to reachability properties (in the aggregated language).
@Inbook{CLRRWADT2014, author="Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Lucanu, Dorel and Rusu, Vlad and Ro{\c{s}}u, Grigore", editor="Codescu, Mihai and Diaconescu, R{\u{a}}zvan and Țuțu, Ionuț", title="A Theoretical Foundation for Programming Languages Aggregation", bookTitle="Recent Trends in Algebraic Development Techniques: 22nd International Workshop, WADT 2014, Sinaia, Romania, September 47, 2014, Revised Selected Papers", year="2015", publisher="Springer International Publishing", address="Cham", pages="3047", isbn="9783319281148", doi="10.1007/9783319281148_3", url="https://doi.org/10.1007/9783319281148_3" }

Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A LanguageIndependent Proof System for
Mutual Program Equivalence. ICFEM 2014.
Abstract: Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in determin istic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a languageindependent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a statesimilarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known weather the sequence terminates or not; nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).
@inproceedings{CLRRICFEM2014, author = "Ciobaca, Stefan and Lucanu, Dorel and Rusu, Vlad and Rosu, Grigore", publisher = "Springer", doi = "http://dx.doi.org/10.1007/9783319117379_6", title = "A LanguageIndependent Proof System for Mutual Program Equivalence", series = "LNCS", booktitle = "Proceedings of the 16th International Conference on Formal Engineering Methods (ICFEM'14)", month = "November", volume = "8829", year = "2014", pages = "7590" }
 Andrei Ștefănescu, Ștefan Ciobâcă, Radu Mereuță, Brandon M. Moore, TraianFlorin Serbanuta, Grigore Roșu, AllPath Reachability Logic, RTATLCA 2014.
 Ștefan Ciobâcă, Reducing Partial Equivalence to Partial Correctness. SYNASC 2014.
 Ștefan Ciobâcă, From SmallStep Semantics to BigStep Semantics, Automatically, IFM 2013.
 Grigore Roșu, Andrei Ștefănescu, Ștefan Ciobâcă and Brandon M. Moore, OnePath Reachability Logic, LICS 2013.
 Grigore Roșu, Andrei Ștefănescu, Ștefan Ciobâcă and Brandon M. Moore, Reachability Logic, Technical Report, July 2012. PDF
 Ștefan Ciobâcă, From Smallstep Semantics to Bigstep Semantics, Automatically, Summer School on Language Frameworks 2012, SSLF 2012, Sinaia, Romania.
 Rohit Chadha, Ștefan Ciobâcă, Steve Kremer, Automated Verification of Equivalence Properties of Cryptographic Protocols. ESOP 2012: 108127 PDF
More publications are available on my DBLP profile.
BSc/MSc Projects
I am looking for excellent students who want to work with me on projects like these (pdf version). If you would like to work with me on such a project, please email me your CV together with a short paragraph explaining what project you would like and why you think you are the right person for that project.
PhD Thesis
I defended my PhD thesis on the security of cryptographic protocols at ENS Cachan on December 9th, 2011.
Tools
For my PhD thesis, I worked on a few tools for the verification of security protocols, the most important being AKiSs, a tool for verifying equivalence properties of cryptographic protocols.
I now contribute to the K Tool, a framework for giving executable semantics to programming languages.
Last modified: Tue Nov 13 22:28:35 EET 2018