Teaching (check again soon)
- 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 Small-Step 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.
- (NEW!) 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.
- Rohit Chadha, Vincent Cheval, Ștefan Ciobâcă, Steve Kremer: Automated Verification of Equivalence Properties of Cryptographic Protocols. ACM Transactions on Computational Logic, 2016.
- Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A language-independent proof system for full program equivalence. Formal Aspects of Computing, 2016.
- Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A Theoretical Foundation for Programming Languages Aggregation. WADT 2014 post-proceedings, LNCS 9463, 2015.
- Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A Language-Independent Proof System for Mutual Program Equivalence. ICFEM 2014.
- Andrei Ștefănescu, Ștefan Ciobâcă, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Roșu, All-Path Reachability Logic, RTA-TLCA 2014.
- Ștefan Ciobâcă, Reducing Partial Equivalence to Partial Correctness. SYNASC 2014.
- Ștefan Ciobâcă, From Small-Step Semantics to Big-Step Semantics, Automatically, IFM 2013.
- Grigore Roșu, Andrei Ștefănescu, Ștefan Ciobâcă and Brandon M. Moore, One-Path Reachability Logic, LICS 2013.
- Grigore Roșu, Andrei Ștefănescu, Ștefan Ciobâcă and Brandon Moore, Reachability Logic, Technical Report, July 2012. PDF
- Ștefan Ciobâcă, From Small-step Semantics to Big-step 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: 108-127 PDF
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.
I defended my PhD thesis on the security of cryptographic protocols at ENS Cachan on December 9th, 2011.
I now contribute to the K Tool, a framework for giving executable semantics to programming languages.
Last modified: Thu Mar 31 08:34:17 EEST 2016