Ștefan Ciobâcă
Teaching
 Programare Funcțională (in Romanian, Summer Semester 2019/2020)
Talks
 (NEW!) 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ă)
 (NEW!) 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
 (NEW!) CezarConstantin Andrici, Ștefan Ciobâcă: Verifying the DPLL Algorithm in Dafny (FROM 2019). Abstract and BibTeX
 (NEW!) 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: Mon Feb 17 17:19:58 EET 2020