dSPIN: A Dynamic Extension of SPIN. - Claudio Demartini; Radu Iosif; Riccardo Sisto (SPIN, 1999)

A Deadlock Detection Tool for Concurrent Java Programs. - Claudio Demartini; Radu Iosif; Riccardo Sisto (Softw. Pract. Exp., 1999)

Formal verification applied to Java concurrent software. - Radu Iosif (ICSE, 2000)

Using Garbage Collection in Model Checking. - Radu Iosif; Riccardo Sisto (SPIN, 2000)

Exploiting Heap Symmetries in Explicit-State Model Checking of Software. - Radu Iosif (ASE, 2001)

Symmetry Reduction Criteria for Software Model Checking. - Radu Iosif (SPIN, 2002)

Storeless semantics and alias logic. - Marius Bozga; Radu Iosif; Yassine Lakhnech (PEPM, 2003)

Space-Reduction Strategies for Model Checking Dynamic Software. - Robby; Matthew B. Dwyer; John Hatcliff; Radu Iosif (SoftMC@CAV, 2003)

Temporal logic properties of Java objects. - Radu Iosif; Riccardo Sisto (J. Syst. Softw., 2003)

On Logics of Aliasing. - Marius Bozga; Radu Iosif; Yassine Lakhnech (SAS, 2004)

Symmetry reductions for model checking of concurrent dynamic software. - Radu Iosif (Int. J. Softw. Tools Technol. Transf., 2004)

On Decidability Within the Arithmetic of Addition and Divisibility. - Marius Bozga; Radu Iosif (FoSSaCS, 2005)

Translating Java for Multiple Model Checkers: The Bandera Back-End. - Radu Iosif; Matthew B. Dwyer; John Hatcliff (Formal Methods Syst. Des., 2005)

Proving Termination of Tree Manipulating Programs. - Peter Habermehl; Radu Iosif; Adam Rogalewicz; Tomás Vojnar (ATVA, 2007)

On Flat Programs with Lists. - Marius Bozga; Radu Iosif (VMCAI, 2007)

What Else Is Decidable about Integer Arrays?. - Peter Habermehl; Radu Iosif; Tomás Vojnar (FoSSaCS, 2008)

A Logic of Singly Indexed Arrays. - Peter Habermehl; Radu Iosif; Tomás Vojnar (LPAR, 2008)

Automatic Verification of Integer Array Programs. - Marius Bozga; Peter Habermehl; Radu Iosif; Filip Konecný; Tomás Vojnar (CAV, 2009)

Iterating Octagons. - Marius Bozga; Codruta Gîrlea; Radu Iosif (TACAS, 2009)

Flat Parametric Counter Automata. - Marius Bozga; Radu Iosif; Yassine Lakhnech (Fundam. Informaticae, 2009)

Tool Demonstration of the FLATA Counter Automata Toolset. - Marius Bozga; Radu Iosif; Filip Konecný; Tomás Vojnar (WING@ETAPS/IJCAR, 2010)

Fast Acceleration of Ultimately Periodic Relations. - Marius Bozga; Radu Iosif; Filip Konecný (CAV, 2010)

Automata-based verification of programs with tree updates. - Peter Habermehl; Radu Iosif; Tomás Vojnar (Acta Informatica, 2010)

Quantitative Separation Logic and Programs with Lists. - Marius Bozga; Radu Iosif; Swann Perarnau (J. Autom. Reason., 2010)

Programs with lists are counter automata. - Ahmed Bouajjani; Marius Bozga; Peter Habermehl; Radu Iosif; Pierre Moro; Tomás Vojnar (Formal Methods Syst. Des., 2011)

Accelerating Interpolants. - Hossein Hojjat; Radu Iosif; Filip Konecný; Viktor Kuncak; Philipp Rümmer (ATVA, 2012)

A Verification Toolkit for Numerical Transition Systems - Tool Paper. - Hossein Hojjat; Filip Konecný; Florent Garnier; Radu Iosif; Viktor Kuncak; Philipp Rümmer (FM, 2012)

The Tree Width of Separation Logic with Recursive Definitions. - Radu Iosif; Adam Rogalewicz; Jirí Simácek (CADE, 2013)

Automata-Based Termination Proofs. - Radu Iosif; Adam Rogalewicz (Comput. Informatics, 2013)

Deciding Entailments in Inductive Separation Logic with Tree Automata. - Radu Iosif; Adam Rogalewicz; Tomás Vojnar (ATVA, 2014)

Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops. - Marius Bozga; Radu Iosif; Filip Konecný (VMCAI, 2014)

Generating Bounded Languages Using Bounded Control Sets. - Pierre Ganty; Radu Iosif (CoRR, 2014)

Abstraction Refinement for Trace Inclusion of Data Automata. - Radu Iosif; Adam Rogalewicz; Tomás Vojnar (CoRR, 2014)

Deciding Conditional Termination - Marius Bozga; Radu Iosif; Filip Konecný (Log. Methods Comput. Sci., 2014)

Interprocedural Reachability for Flat Integer Programs. - Pierre Ganty; Radu Iosif (FCT, 2015)

How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property? - Radu Iosif; Arnaud Sangnier (ATVA, 2016)

A Decision Procedure for Separation Logic in SMT. - Andrew Reynolds 001; Radu Iosif; Cristina Serban; Tim King 001 (ATVA, 2016)

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. - Radu Iosif; Adam Rogalewicz; Tomás Vojnar (TACAS, 2016)

A Decision Procedure for Separation Logic in SMT. - Andrew Reynolds 001; Radu Iosif; Tim King 001 (CoRR, 2016)

Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic. - Andrew Reynolds 001; Radu Iosif; Cristina Serban (CoRR, 2016)

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. - Andrew Reynolds 001; Radu Iosif; Cristina Serban (VMCAI, 2017)

Complete Cyclic Proof Systems for Inductive Entailments. - Radu Iosif; Cristina Serban (CoRR, 2017)

The Impact of Alternation. - Radu Iosif; Xiao Xu (CoRR, 2017)

Underapproximation of procedure summaries for integer programs. - Pierre Ganty; Radu Iosif; Filip Konecný (Int. J. Softw. Tools Technol. Transf., 2017)

A Complete Cyclic Proof System for Inductive Entailments in First Order Logic. - Radu Iosif; Cristina Serban (LPAR, 2018)

Program Verification with Separation Logic. - Radu Iosif (SPIN, 2018)

Abstraction Refinement for Emptiness Checking of Alternating Data Automata. - Radu Iosif; Xiao Xu (TACAS (2), 2018)

On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CoRR, 2018)

The Complexity of Prenex Separation Logic with One Selector. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CoRR, 2018)

First Order Alternation. - Radu Iosif; Xiao Xu (CoRR, 2018)

An Entailment Checker for Separation Logic with Inductive Definitions. - Cristina Serban; Radu Iosif (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018)

Alternating Automata Modulo First Order Theories. - Radu Iosif; Xiao Xu (CAV (2), 2019)

The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (FoSSaCS, 2019)

Prenex Separation Logic with One Selector Field. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (TABLEAUX, 2019)

SL-COMP: Competition of Solvers for Separation Logic. - Mihaela Sighireanu; Juan Antonio Navarro Pérez; Andrey Rybalchenko; Nikos Gorogiannis; Radu Iosif; Andrew Reynolds 001; Cristina Serban; Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger; Wei-Ngan Chin; et al. (TACAS (3), 2019)

Structural Invariants for Parametric Verification of Systems with Almost Linear Architectures. - Marius Bozga; Radu Iosif; Joseph Sifakis (CoRR, 2019)

Local Reasoning about Parametric and Reconfigurable Component-based Systems. - Marius Bozga; Radu Iosif; Joseph Sifakis (CoRR, 2019)

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (LPAR, 2020)

Structural Invariants for the Verification of Systems with Parameterized Architectures. - Marius Bozga; Javier Esparza; Radu Iosif; Joseph Sifakis; Christoph Welzel (TACAS (1), 2020)

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CoRR, 2020)

Verifying Safety Properties of Inductively Defined Parameterized Systems. - Marius Bozga; Radu Iosif (CoRR, 2020)

Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CoRR, 2020)

Abstraction refinement and antichains for trace inclusion of infinite state systems. - Lukás Holík; Radu Iosif; Adam Rogalewicz; Tomás Vojnar (Formal Methods Syst. Des., 2020)

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (ACM Trans. Comput. Log., 2020)

ostrich. - Christoph Welzel; Marius Bozga; Radu Iosif; Joseph Sifakis; Javier Esparza (Zenodo, 2020)

ostrich. - Christoph Welzel; Marius Bozga; Radu Iosif; Joseph Sifakis; Javier Esparza (Zenodo, 2020)

ostrich. - Christoph Welzel; Marius Bozga; Radu Iosif; Joseph Sifakis; Javier Esparza (Zenodo, 2020)

Unifying Decidable Entailments in Separation Logic with Inductive Definitions. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CADE, 2021)

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CSL, 2021)

Specification and Safety Verification of Parametric Hierarchical Distributed Systems. - Marius Bozga; Radu Iosif (FACS, 2021)

Local Reasoning about Parameterized Reconfigurable Distributed Systems. - Emma Ahrens; Marius Bozga; Radu Iosif; Joost-Pieter Katoen (CoRR, 2021)

Checking deadlock-freedom of parametric component-based systems. - Marius Bozga; Radu Iosif; Joseph Sifakis (J. Log. Algebraic Methods Program., 2021)

Decision Problems in a Logic for Reasoning About Reconfigurable Distributed Systems. - Marius Bozga; Lucas Bueri; Radu Iosif (IJCAR, 2022)

On an Invariance Problem for Parameterized Concurrent Systems. - Marius Bozga; Lucas Bueri; Radu Iosif (CONCUR, 2022)

On the Expressiveness of a Logic of Separated Relations. - Radu Iosif; Florian Zuleger (CoRR, 2022)

Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (Inf. Process. Lett., 2022)

Reasoning about distributed reconfigurable systems. - Emma Ahrens; Marius Bozga; Radu Iosif; Joost-Pieter Katoen (Proc. ACM Program. Lang., 2022)

Expressiveness Results for an Inductive Logic of Separated Relations. - Radu Iosif; Florian Zuleger (CONCUR, 2023)

Characterizations of Definable Context-Free Graphs. - Radu Iosif; Florian Zuleger (CoRR, 2023)

The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations. - Marius Bozga; Lucas Bueri; Radu Iosif; Florian Zuleger (CoRR, 2023)

Verification of component-based systems with recursive architectures. - Marius Bozga; Radu Iosif; Joseph Sifakis (Theor. Comput. Sci., 2023)

Tree-Verifiable Graph Grammars. - Mark Chimes; Radu Iosif; Florian Zuleger (LPAR, 2024)

Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations. - Lucas Bueri; Radu Iosif; Florian Zuleger (CoRR, 2024)

Regular Grammars for Graph Sets of Tree-Width ≤. - Marius Bozga; Radu Iosif; Florian Zuleger (CoRR, 2024)

Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks. - Marius Bozga; Radu Iosif; Arnaud Sangnier; Neven Villani (CAV (3), 2025)

Counting Abstraction for the Verification of Structured Parameterized Networks. - Marius Bozga; Radu Iosif; Arnaud Sangnier; Neven Villani (CoRR, 2025)

Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars. - Radu Iosif; Arnaud Sangnier; Neven Villani (CoRR, 2025)