| 2019 | VMCAI | Mechanically Proving Determinacy of Hierarchical Block Diagram Translations. | Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis |
| 2018 | TACAS | The Refinement Calculus of Reactive Systems Toolset. | Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis |
| 2017 | FORTE | Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. | Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis |
| 2016 | IFM | Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle. | Viorel Preoteasa |
| 2016 | LICS | Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. | Viorel Preoteasa, Stavros Tripakis |
| 2016 | SAC | Predictive runtime enforcement. | Srinivas Pinisetty, Viorel Preoteasa, Stavros Tripakis, Thierry Jron, Ylis Falcone, Herv Marchand |
| 2014 | EMSOFT | Refinement calculus of reactive systems. | Viorel Preoteasa, Stavros Tripakis |
| 2011 | SAC | Semantics and proof rules of invariant based programs. | Ralph-Johan Back, Viorel Preoteasa |
| 2006 | FM | Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic. | Viorel Preoteasa |
| 2003 | APSEC | Reasoning about Pointers in Refinement Calculus. | Ralph-Johan Back, Xiaocong Fan, Viorel Preoteasa |
| 2003 | ICFP | Reasoning about recursive procedures with parameters. | Ralph-Johan Back, Viorel Preoteasa |