Ștefan Ciobâcă
Teaching
 (NEW!) Functional Programming (in Romanian, Summer Semester 2023/2024)
News
 I am helping organize WoLLIC 2022, which takes place in Iași, Romania between 2023 September 2022.
 Consider submitting your work to WPTE 2022, the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, associated to FSCD 2022 and FLoC 2022  it takes place in Haifa, Israel, on July 31st, 2022.
 October 8th, 2021: Presentation on Verifying the Conversion into CNF in Dafny at WoLLIC 2021 (online)
 July 18th, 2021: Presentation on Operationallybased Program Equivalence Proofs using LCTRSs at WPTE 2021 (online)
 Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault: An Extended Account of Tracerelating Compiler Correctness and Secure Compilation (ACM TOPLAS, open access). Abstract and BibTeX
 Viorel Iordache, Stefan Ciobaca: Verifying the Conversion into CNF in Dafny (WoLLIC 2021, PDF). Abstract and BibTeX
@article{10.1145/3460860, author = {Abate, Carmine and Blanco, Roberto and Ciob\^{a}c\u{a}, \c{S}tefan and Durier, Adrien and Garg, Deepak and Hri\c{t}cu, C\u{a}t\u{a}lin and Patrignani, Marco and Tanter, \'{E}ric and Thibault, J\'{e}r\'{e}my}, title = {An Extended Account of TraceRelating Compiler Correctness and Secure Compilation}, year = {2021}, issue_date = {December 2021}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {43}, number = {4}, issn = {01640925}, url = {https://doi.org/10.1145/3460860}, doi = {10.1145/3460860}, abstract = {Compiler correctness, in its simplest form, is defined as the inclusion of the set of traces of the compiled program in the set of traces of the original program. This is equivalent to the preservation of all trace properties. Here, traces collect, for instance, the externally observable events of each execution. However, this definition requires the set of traces of the source and target languages to be the same, which is not the case when the languages are far apart or when observations are finegrained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a nontrivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many definitions of secure compilation, which characterize the protection of a compiled program linked against adversarial code.}, journal = {ACM Trans. Program. Lang. Syst.}, month = {nov}, articleno = {14}, numpages = {48}, keywords = {hyperproperties, Trace properties, propertypreserving compilation, compiler correctness, formal languages, programming languages, secure compilation, Galois connection} }
@inproceedings{DBLP:conf/wollic/IordacheC21, author = {Viorel Iordache and {\c{S}}tefan Ciob{\^{a}}c{\u{a}}}, editor = {Alexandra Silva and Renata Wassermann and Ruy J. G. B. de Queiroz}, title = {Verifying the Conversion into {CNF} in Dafny}, booktitle = {Logic, Language, Information, and Computation  27th International Workshop, WoLLIC 2021, Virtual Event, October 58, 2021, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13038}, pages = {150166}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/9783030888534\_10}, doi = {10.1007/9783030888534\_10}, timestamp = {Fri, 08 Oct 2021 08:48:01 +0200}, biburl = {https://dblp.org/rec/conf/wollic/IordacheC21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
Talks
 September 5th, 2019: Presentation on Verifying the DPLL Algorithm in Dafny at the Working Formal Methods Symposium, FROM 2019, Timișoara (authors: CezarConstantin Andrici, Ștefan Ciobâcă)
 July 1st, 2019: Slides and extra material on my ISR 2019 lecture on Logically Constrained Term Rewriting Systems.
 April 6th, 2019: Files for our presentation on SemanticsBased Proofs of Equivalence for Functions with Accumulators (Ștefan Ciobâcă, Dorel Lucanu and Sebastian Buruiană) at PERR 2019 (part of ETAPS 2019).
 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
 CezarConstantin Andrici, Ștefan Ciobâcă: Verifying the DPLL Algorithm in Dafny (FROM 2019). Abstract and BibTeX
 Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault: TraceRelating Compiler Correctness and Secure Compilation (arXiv:1907.05320). Abstract
 Andrei Ștefănescu, Ștefan Ciobâcă, Radu Mereuță, Brandom M. Moore, Grigore Roșu and Traian Florin Șerbănuță: Allpath Reachability Logic (LMCS 2019). Abstract and BibTeX
 AndreiSebastian Buruiană, Ştefan Ciobâcă : Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (WPTE 2018). Abstract and BibTeX
 Ștefan Ciobâcă, Andrei Arusoaie, Dorel Lucanu: Unification Modulo Builtins (WoLLIC 2018).
 Ștefan Ciobâcă, Dorel Lucanu: A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems (IJCAR 2018; extended technical report). Abstract and BibTeX
 Andrei Arusoaie, Ștefan Ciobâcă, Vlad Crăciun, Dragoș Gavriluț, Dorel Lucanu: A Comparison of OpenSource Static Analysis Tools for Vulnerability Detection in C/C++ Code . Postproceedings SYNASC 2017. PDF Abstract and BibTeX

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 and BibTeX
 Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A LanguageIndependent Proof System for Full Program Equivalence. Formal Aspects of Computing, 2016. (SpringerLink) Abstract and BibTeX
 Ș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 and BibTeX
 Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A LanguageIndependent Proof System for Mutual Program Equivalence. ICFEM 2014. Abstract and BibTeX
 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
@Inproceedings{EPTCS303.1, author = {Andrici, CezarConstantin and Ciob\^ac\u{a}, \c{S}tefan}, year = {2019}, title = {Verifying the {DPLL} Algorithm in {D}afny}, editor = {Marin, Mircea and Cr\u{a}ciun, Adrian}, booktitle = {{\rm Proceedings Third Symposium on} Working Formal Methods, {\rm Timi\c{s}oara, Romania, 35 September 2019}}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {303}, publisher = {Open Publishing Association}, pages = {315}, doi = {10.4204/EPTCS.303.1}, }
@article{lmcs:5408 TITLE = {{AllPath Reachability Logic}}, AUTHOR = {Stefanescu, Andrei and Ciobaca, Stefan and Mereuta, Radu and Moore, Brandon and Serbanuta, Traian Florin and Rosu, Grigore}, URL = {https://lmcs.episciences.org/5408}, DOI = {}, JOURNAL = {{Logical Methods in Computer Science}}, VOLUME = {{Volume 15, Issue 2}}, YEAR = {2019}, MONTH = Apr, KEYWORDS = {Computer Science  Programming Languages ; Computer Science  Formal Languages and Automata Theory ; Computer Science  Logic in Computer Science}, }
@Inproceedings{EPTCS289.1, author = {Buruian\u{a}, AndreiSebastian and Ciob\^ac\u{a}, \c{S}tefan}, year = {2019}, title = {Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics}, editor = {Niehren, Joachim and Sabel, David}, booktitle = {{\rm Proceedings Fifth International Workshop on} Rewriting Techniques for Program Transformations and Evaluation, {\rm Oxford, England, 8th July 2018}}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {289}, publisher = {Open Publishing Association}, pages = {116}, doi = {10.4204/EPTCS.289.1}, }
@inproceedings{DBLP:conf/wollic/CiobacaAL18, author = {\c{S}tefan Ciob\^ac\u{a} and Andrei Arusoaie and Dorel Lucanu}, title = {Unification Modulo Builtins}, booktitle = {Logic, Language, Information, and Computation  25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 2427, 2018, Proceedings}, pages = {179195}, year = {2018}, url = {https://doi.org/10.1007/9783662576694\_10}, doi = {10.1007/9783662576694\_10}, timestamp = {Wed, 14 Nov 2018 10:55:35 +0100}, biburl = {https://dblp.org/rec/bib/conf/wollic/CiobacaAL18}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/CiobacaL18, author = {\c{S}tefan Ciob\^ac\u{a} and Dorel Lucanu}, title = {A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems}, booktitle = {Automated Reasoning  9th International Joint Conference, {IJCAR} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 1417, 2018, Proceedings}, pages = {295311}, year = {2018}, url = {https://doi.org/10.1007/9783319942056\_20}, doi = {10.1007/9783319942056\_20}, timestamp = {Mon, 09 Jul 2018 13:01:56 +0200}, biburl = {https://dblp.org/rec/bib/conf/cade/CiobacaL18}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/synasc/ArusoaieCCGL17, author = {Andrei Arusoaie and \c{S}tefan Ciob\^ac\u{a} and Vlad Craciun and Dragos Gavrilut and Dorel Lucanu}, title = {A Comparison of OpenSource Static Analysis Tools for Vulnerability Detection in {C/C++} Code}, booktitle = {19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, {SYNASC} 2017, Timisoara, Romania, September 2124, 2017}, pages = {161168}, year = {2017}, url = {https://doi.org/10.1109/SYNASC.2017.00035}, doi = {10.1109/SYNASC.2017.00035}, timestamp = {Thu, 14 Feb 2019 16:15:01 +0100}, biburl = {https://dblp.org/rec/bib/conf/synasc/ArusoaieCCGL17}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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}, }
@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" }
@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" }
@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" }
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: Thu Feb 23 18:53:19 EET 2023