A Relation Between Unambiguous Regular Expressions and Abstract Data Types. - Viorel Preoteasa (Fundam. Informaticae, 1999)

Reasoning about Pointers in Refinement Calculus. - Ralph-Johan Back; Xiaocong Fan; Viorel Preoteasa (APSEC, 2003)

Reasoning about recursive procedures with parameters. - Ralph-Johan Back; Viorel Preoteasa (MERLIN, 2003)

An algebraic treatment of procedure refinement to support mechanical verification. - Ralph-Johan Back; Viorel Preoteasa (Formal Aspects Comput., 2005)

Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic. - Viorel Preoteasa (FM, 2006)

Data Refinement of Invariant Based Programs. - Viorel Preoteasa; Ralph-Johan Back (REFINE@FMWeek, 2009)

Frame rule for mutually recursive procedures manipulating pointers. - Viorel Preoteasa (Theor. Comput. Sci., 2009)

Semantics and Data Refinement of Invariant Based Programs. - Viorel Preoteasa; Ralph-Johan Back (Arch. Formal Proofs, 2010)

Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement. - Viorel Preoteasa; Ralph-Johan Back (Arch. Formal Proofs, 2010)

Semantics and proof rules of invariant based programs. - Ralph-Johan Back; Viorel Preoteasa (SAC, 2011)

Pseudo Hoops. - George Georgescu; Laurentiu Leustean; Viorel Preoteasa (Arch. Formal Proofs, 2011)

Lattice Properties. - Viorel Preoteasa (Arch. Formal Proofs, 2011)

Algebra of Monotonic Boolean Transformers. - Viorel Preoteasa (Arch. Formal Proofs, 2011)

Invariant diagrams with data refinement. - Viorel Preoteasa; Ralph-Johan Back (Formal Aspects Comput., 2012)

Refinement calculus of reactive systems. - Viorel Preoteasa; Stavros Tripakis (EMSOFT, 2014)

Formalization of Refinement Calculus for Reactive Systems. - Viorel Preoteasa (Arch. Formal Proofs, 2014)

Refinement algebra with dual operator. - Viorel Preoteasa (Sci. Comput. Program., 2014)

Translating Hierarchical Block Diagrams into Composite Predicate Transformers. - Iulia Dragomir; Viorel Preoteasa; Stavros Tripakis (CoRR, 2015)

Verification and code generation for invariant diagrams in Isabelle. - Viorel Preoteasa; Ralph-Johan Back; Johannes Eriksson (J. Log. Algebraic Methods Program., 2015)

Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle. - Viorel Preoteasa (IFM, 2016)

Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. - Viorel Preoteasa; Stavros Tripakis (LICS, 2016)

Compositional Semantics and Analysis of Hierarchical Block Diagrams. - Iulia Dragomir; Viorel Preoteasa; Stavros Tripakis (SPIN, 2016)

A Nondeterministic and Abstract Algorithm for Translating Hierarchical Block Diagrams. - Viorel Preoteasa; Iulia Dragomir; Stavros Tripakis (CoRR, 2016)

Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. - Viorel Preoteasa; Iulia Dragomir; Stavros Tripakis (FORTE, 2017)

Predictive runtime enforcement. - Srinivas Pinisetty; Viorel Preoteasa; Stavros Tripakis; Thierry Jéron; Yliès Falcone; Hervé Marchand (Formal Methods Syst. Des., 2017)

Predictive runtime verification of timed properties. - Srinivas Pinisetty; Thierry Jéron; Stavros Tripakis; Yliès Falcone; Hervé Marchand; Viorel Preoteasa (J. Syst. Softw., 2017)

Modelling Programmable Logic Controllers in Refinement Calculus of Reactive Systems. - Viorel Preoteasa; Timo Latvala; Kimmo Varpaaniemi (CS&P, 2019)

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations. - Viorel Preoteasa; Iulia Dragomir; Stavros Tripakis (VMCAI, 2019)

The Refinement Calculus of Reactive Systems Toolset. - Iulia Dragomir; Viorel Preoteasa; Stavros Tripakis (Int. J. Softw. Tools Technol. Transf., 2020)

The refinement calculus of reactive systems. - Viorel Preoteasa; Iulia Dragomir; Stavros Tripakis (Inf. Comput., 2022)