Numerical Transition Systems - User contributions [en]

Recent publications

2026-04-28T09:02:13Z

Radu iosif:

[[File:Newspapers-stacked.jpg|right|top]]

==== Pending ====

* M. Bozga, R. Iosif and F. Zuleger. Regular Grammars as Effective Representations of Recognizable Sets of Series-Parallel Graphs. [https://arxiv.org/abs/2604.24151 arXiv:2604.24151]
* L. Bueri, R. Iosif and F. Zuleger. Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations [https://arxiv.org/abs/2402.16150 arXiv:2402.16150]
* M. Bozga, L. Bueri, R. Iosif and F. Zuleger. The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations. [https://arxiv.org/abs/2310.09542 arXiv:2310.09542]
* M. Bozga, R. Iosif and J. Sifakis. Local Reasoning about Parametric and Reconfigurable Component-based Systems. [https://arxiv.org/abs/1908.11345 arXiv:1908.11345]
* M. Bozga, R. Iosif and F. Konecny. The Complexity of Reachability Problems for Flat Counter Machines with Periodic Loops [http://arxiv.org/abs/1307.5321 arXiv:1307.5321]

==== Journals ====

* R. Iosif and F. Zuleger. [https://lmcs.episciences.org/17687 Characterizations of Monadic Second Order Definable Context-free Sets of Graphs]. Logical Methods in Computer Science (LMCS) Volume 22, Issue 1, 2026, pp. 22:1–22:30
* M. Bozga, R. Iosif, J. Sifakis. [https://doi.org/10.1016/j.tcs.2022.10.022 Verification of component-based systems with recursive architectures]. Theoretical Computer Science (TCS) Volume 940 pp 146-175 (2023)
* M. Echenim, R. Iosif, N. Peltier. [https://www.sciencedirect.com/science/article/pii/S0020019021000843?dgcid=coauthor Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules]. Information Processing Letters (IPL) Volume 173 (2022)
* M. Bozga, R. Iosif and J. Sifakis. [https://www.sciencedirect.com/science/article/pii/S2352220820301061 Checking Deadlock Freedom of Parametric Component-based Systems]. Journal of Logical and Algebraic Methods in Programming (JLAMP) Volume 119 (2021)
* M. Echenim, R. Iosif and N. Peltier. [https://hal.archives-ouvertes.fr/hal-02388326 The Bernays-Schoenfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates]. ACM Transactions on Computational Logic (TOCL) 21(3): 19:1-19:46 (2020)
* L. Holik, R. Iosif, A. Rogalewicz and T. Vojnar. [https://doi.org/10.1007/s10703-020-00345-1 Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems]. Formal Methods in System Design (FMSD) Volume 55, pages 137–170 (2020)
* P. Ganty, R. Iosif and F. Konecny. [http://link.springer.com/article/10.1007%2Fs10009-016-0420-7 Underapproximation of Procedure Summaries for Integer Programs] Software Tools for Technology Transfer, pp 1-20 [[http://arxiv.org/abs/1210.4289 arXiv:1210.4289]]
* M. Bozga, R. Iosif and F. Konecny. [http://arxiv.org/abs/1302.2762 Deciding Conditional Termination] Logical Methods in Computer Science, Vol. 10(3:8) 2014 pp 1-61
* R. Iosif and A. Rogalewicz. [[Media:Cai13.pdf|Automata-based termination proofs]] Computing and Informatics, Vol.22 (2013) pp 1001-1035
* A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro and T. Vojnar. [[Media:Fmsd10.pdf|Programs with Lists are Counter Automata]] Formal Methods in System Design, Vol. 38(2) (2011) pp 158-192
* M. Bozga, R. Iosif, S. Perarnau. [[Media:Qsl-jar.pdf|Quantitative Separation Logic and Programs with Lists]] Journal of Automated Reasoning, Vol. 45(2) (2010) pp 131-156
* P. Habermehl, R. Iosif, T. Vojnar. [[Media:Redblackjournal09.pdf|Automata-based Verification of Programs with Tree Updates]] Acta Informatica: Vol. 47(1) (2010) pp 1-31
* M. Bozga, R. Iosif, Y. Lakhnech. [[Media:Fundamenta09.pdf|Flat Parametric Counter Automata]] Fundamenta Informaticae, Vol. 91(2) (2009) pp 275 - 303
* R. Iosif. [[Media:Sttt.pdf|Symmetry Reductions for Model Checking of Concurrent Dynamic Software]] Software Tools for Technology Transfer, Vol. 6(4), pp 302 - 319
* R. Iosif, M. Dwyer, J. Hatcliff. [[Media:Fmsd05.pdf|Translating Java for Multiple Model Checkers: the Bandera Back End]] Formal Methods in System Design, Vol. 26(2) (2005), pp 137-180
* R. Iosif, R. Sisto. [[Media:JSS.pdf|Temporal Logic Properties of Java Objects]] Journal of Systems and Software, Vol. 68(3) (2003) pp 243-251
* C. Demartini, R. Iosif, R. Sisto. A Deadlock Detection Tool For Concurrent Java Programs. Software: Practice & Experience, Vol. 29(7) (1999), pp 577-603

==== Conferences ====

* Marius Bozga, Radu Iosif, Florian Zuleger. [https://arxiv.org/abs/2510.06019 Iterating Non-Aggregative Structure Compositions]. FSTTCS 2025, pp 18:1-18:18
* Marius Bozga, Radu Iosif, Arnaud Sangnier, Neven Villani. [https://dl.acm.org/doi/10.1007/978-3-031-98682-6_13 Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks] CAV 2025, pp 238-262
* Marius Bozga, Radu Iosif, Florian Zuleger. [https://www.computer.org/csdl/proceedings-article/lics/2025/790000a704/2aFJRkxJDmE Regular Grammars for Sets of Graphs of Tree-Width 2]. LICS 2025, pp 704-717
* Radu Iosif, Arnaud Sangnier, Neven Villani. [https://dl.acm.org/doi/10.1007/978-3-032-00347-8_4 Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars]. NETYS 2025, pp 57-80
* Mark Chimes, Radu Iosif and Florian Zuleger. [https://easychair.org/publications/paper/8LGS Tree-Verifiable Graph Grammars]. LPAR 2024, pp 165-180
* Radu Iosif, Florian Zuleger. [https://drops.dagstuhl.de/opus/volltexte/2023/19014/ Expressiveness Results for an Inductive Logic of Separated Relations]. CONCUR 2023, pp 20:1-20:20
* Marius Bozga, Lucas Bueri, Radu Iosif. [https://drops.dagstuhl.de/opus/volltexte/2022/17087/ On an Invariance Problem for Parameterized Concurrent Systems]. CONCUR 2022, pp 24:1-24:16
* Marius Bozga, Lucas Bueri, Radu Iosif. [https://arxiv.org/abs/2202.09637 Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems]. IJCAR 2022, pp 691-711
* Emma Ahrens, Marius Bozga, Radu Iosif, Joost-Pieter Katoen. [https://dl.acm.org/doi/10.1145/3563293 Reasoning about Distributed Reconfigurable Systems]. OOPSLA 2022, pp 145–174
* M. Bozga, R. Iosif. [[Media:Facs21.pdf|Verifying Safety Properties of Inductively Defined Parameterized Systems]]. FACS 2021, pp 95-114
* M. Echenim, R. Iosif, N. Peltier. [[Media:CADE_2021_final_version.pdf|Unifying Decidable Entailments in Separation Logic with Inductive Definitions]]. CADE 2021, pp 183-199
* M. Echenim, R. Iosif, N. Peltier. [https://drops.dagstuhl.de/opus/volltexte/2021/13454/ Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems.] CSL 2021, pp 1--18
* M. Echenim, R. Iosif, N. Peltier. [https://easychair.org/publications/paper/DdNg Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard.] LPAR 2020, pp 191--211
* M. Bozga, J. Esparza, R. Iosif, J. Sifakis and C. Welzel. [https://arxiv.org/abs/2002.07672 Structural Invariants for the Verification of Systems with Parameterized Architectures.] TACAS (1) 2020, pp 228--246
* R. Iosif and X. Xu. [[Media:Cav2019.pdf|Alternating Automata Modulo First Order Theories]], CAV 2019, Part II, pp 43--63
* M. Echenim, R. Iosif and N. Peltier. [[Media:Fossacs2019.pdf|The Bernays-Schoenfinkel-Ramsey Class of Separation Logic on Arbitrary Domains]], FOSSACS 2019, pp 242--259
* M. Echenim, R. Iosif, N. Peltier. [[Media:Tableaux2019.pdf|Prenex Separation Logic with One Selector Field]]. TABLEAUX 2019, pp 409--427
* M. Bozga, R. Iosif and J. Sifakis. [[Media:Tacas2019.pdf|Checking Deadlock-Freedom of Parametric Component-Based Systems]]. TACAS 2019, Part II, pp 3-20
* R. Iosif and C. Serban. [[Media:Lpar2018.pdf|A Complete Cyclic Proof System for Inductive Entailments in First Order Logic]]. LPAR 2018, pp 435--453
* R. Iosif and X. Xu. [[Media:Tacas2018.pdf|Abstraction Refinement for Emptiness Checking of Alternating Data Automata]] TACAS 2018, pp 93-111
* A. Reynolds, R. Iosif and C. Serban. [[Media:Vmcai2017.pdf|Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic]] VMCAI 2017, pp 462-482
* R. Iosif, A. Sangnier. [[Media:Atva2016-1.pdf|How hard is it to verify flat affine counter systems with the finite monoid property ?]] ATVA 2016, pp 89-105
* A. Reynolds, R. Iosif, C. Serban and T. King. [[Media:Atva2016-2.pdf|A Decision Procedure for Separation Logic in SMT]] ATVA 2016, pp 244-261
* R. Iosif, A. Rogalewicz and T. Vojnar. [http://arxiv.org/pdf/1410.5056.pdf Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems] TACAS 2016 pp 71-89
* P. Ganty and R. Iosif. [http://arxiv.org/abs/1405.3069 Interprocedural Reachability for Flat Integer Programs] FCT 2015, pp 133-145.
* R. Iosif, A. Rogalewicz and T. Vojnar. [[Media:Atva14.pdf|Deciding Entailments in Inductive Separation Logic with Tree Automata]] ATVA 2014, pp 201-218
* M. Bozga, R. Iosif and F. Konecny. [http://arxiv.org/abs/1307.5321 Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops] VMCAI 2014 pp 242-261
* R. Iosif, A. Rogalewicz, J. Simacek. [[Media:Cade13.pdf|The Tree Width of Separation Logic with Recursive Definitions]] CADE 2013, pp 21-38 ('''Best Paper Award''')
* P. Ganty, R. Iosif, F. Konecny. [[Media:Tacas13.pdf|Underapproximation of Procedure Summaries for Integer Programs]] TACAS 2013, pp 245-259
* H. Hojjat, R. Iosif, F. Konecny, V. Kuncak, P. Ruemmer. [[Media:Atva12.pdf|Accelerating Interpolants]] ATVA 2012, pp 187-202
* H. Hojjat, F. Konecny, F. Garnier, R. Iosif, V. Kuncak, P. Ruemmer. [[Media:Fm12.pdf|A Verification Toolkit for Numerical Transition Systems]] (Tool Paper). FM 2012, pp 247-251
* M. Bozga, R. Iosif, F. Konecny. [[Media:Tacas12.pdf|Deciding Conditional Termination]] TACAS 2012, pp 252-266
* M. Bozga, R. Iosif, F. Konecny. [[Media:Cav10.pdf|Fast Acceleration of Ultimately Periodic Relations]] CAV 2010, pp 227-242
* M. Bozga, P. Habermehl, R. Iosif, F. Konecny, T. Vojnar. [[Media:Cav09.pdf|Automatic Verification of Integer Array Programs]] CAV 2009, pp 157-172
* M. Bozga, C. Gîrlea, R. Iosif. [[Media:Tacas09.pdf|Iterating Octagons]] TACAS 2009, pp 337-351
* R. Iosif, A. Rogalewicz. [[Media:Ciaa09.pdf|Automata-Based Termination Proofs]] CIAA 2009, pp 165-177
* M. Bozga, R. Iosif, S. Perarnau. [[Media:Ijcar2008.pdf|Quantitative Separation Logic and Programs with Lists]] IJCAR 2008, pp 34-49
* P. Habermehl, R. Iosif, T. Vojnar. [[Media:Fossacs08.pdf|What Else Is Decidable about Integer Arrays?]] FoSSaCS 2008, pp 474-489
* P. Habermehl, R. Iosif, T. Vojnar. [[Media:Lpar08.pdf|A Logic of Singly Indexed Arrays]] LPAR 2008, pp 558-573
* P. Habermehl, R. Iosif, A. Rogalewicz, T. Vojnar. [[Media:Atva07.pdf|Proving Termination of Tree Manipulating Programs]] ATVA 2007, pp 145-161
* M. Bozga, R. Iosif. [[Media:Vmcai07.pdf|On Flat Programs with Lists]] VMCAI 2007, pp 122-136
* A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, T. Vojnar. [[Media:Cav06.pdf|Programs with Lists Are Counter Automata]] CAV 2006, pp 517-531
* M. Bozga, R. Iosif, Y. Lakhnech. [[Media:Icalp06.pdf|Flat Parametric Counter Automata]] ICALP 2006, pp 577-588
* P. Habermehl, R. Iosif, T. Vojnar. [[Media:Tacas06.pdf|Automata-Based Verification of Programs with Tree Updates]] TACAS 2006, pp 350-364
* M. Bozga, R. Iosif. [[Media:Fossacs05.pdf|On Decidability Within the Arithmetic of Addition and Divisibility]] FoSSaCS 2005, pp 425-439
* M. Bozga, R. Iosif, Y. Lakhnech. [[Media:Sas04.pdf|On Logics of Aliasing]] SAS 2004, pp 344-360
* M. Bozga, R. Iosif, Y. Lakhnech. [[Media:Pepm04.pdf|Storeless semantics and alias logic]] PEPM 2003, pp 55-65
* R. Iosif. [[Media:Spin02.pdf|Symmetry Reduction Criteria for Software Model Checking]] SPIN 2002, pp 22-41
* R. Iosif. [[Media:Ase01.pdf|Exploiting Heap Symmetries in Explicit-State Model Checking of Software]] ASE 2001, pp 254-261

Radu Iosif

2026-03-15T11:11:15Z

Radu iosif: Radu iosif uploaded a new version of File:Lecture1.pdf

File:Lecture1.pdf

2026-03-15T11:03:52Z

Radu iosif: Radu iosif uploaded a new version of File:Lecture1.pdf

Flt25

2026-03-11T15:44:09Z

Radu iosif:

'''Lecturer''': [http://nts.imag.fr/index.php/Radu_Iosif Radu Iosif]

'''Contents''': Formal language theory studies the finite representation of infinite sets of objects (e.g., words, trees, graphs). These representations can
be either descriptive, specifying logical properties of their members (e.g. planar or hamiltonian graphs), or constructive, describing how the members of the set are built.
In particular, constructive representations come with algebras that fix the class of objects and the operations considered. Then, recognizable sets are defined in terms of
congruence relations over the algebra, with a finite number of equivalence classes.

The goal of this course is to introduce the student to the connection between logical definability (using first-order and monadic second-order logics)
and recognisability (by automata, semigroups and algebras). This connection is the cornerstone of formal language theory, because it provides
robust characterisations of the classes of sets that can be represented finitely on a computer.

'''Prerequisites''': basic notions of boolean logic and discrete mathematics (sets, relations, orders, functions); see [https://drive.google.com/file/d/1JnKNGHq_J8IM4U2m1FV2ci6G7OtKJzOn/view?usp=sharing preliminaries] for an introduction to the basic notions required by this course. Basic notions of automata theory and first/second-order logic could be useful and can be found [https://nts.imag.fr/index.php/Lat24 here]

'''Level''': PhD and Master 1-2

'''Schedule''': Wednesdays between 14h00 and 16h00 (Paris time, GMT+1) in Room 206 (2nd floor of [https://www.openstreetmap.org/?mlat=45.19056&mlon=5.76728#map=19/45.190560/5.767280 IMAG building])

* Mar 11, 2026 02:00 PM [https://nts.imag.fr/images/5/5a/Lecture1.pdf slides]
* Mar 18, 2026 02:00 PM
* Mar 25, 2026 02:00 PM
* Apr 01, 2026 02:00 PM

'''Bibliography''':

Mikołaj Bojańczyk. [https://arxiv.org/pdf/2008.11635 Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic]

Jean-Éric Pin. [https://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf Mathematical Foundations of Automata Theory]

Bruno Courcelle. [https://www.sciencedirect.com/science/article/pii/089054019090043H The monadic second-order logic of graphs. I. Recognizable sets of finite graphs]

Bruno Courcelle. [https://www.labri.fr/perso/courcell/Textes1/MSOL05(1991).pdf The monadic second-order logic of graphs V: on closing the gap between definability and recognizability]

Bruno Courcelle and Joost Engelfriet. [https://www.researchgate.net/publication/220544439_A_Logical_Characterization_of_the_Sets_of_Hypergraphs_Defined_by_Hyperedge_Replacement_Grammars A Logical Characterization of the Sets of Hypergraphs Defined by Hyperedge Replacement Grammars]

2025-04-09T14:39:21Z

Radu iosif:

Flt25

2025-04-02T14:39:18Z

Phd and internship subjects

2024-12-08T19:27:30Z

Radu iosif:

== Internship subjects ==

* [http://nts.imag.fr/images/b/b1/TW2REG.pdf A Toolbox for Handling Infinite Sets of Graphs]

The goal of this internship is an implementation of a toolbox that
handles sets of graphs described as regular grammars. Ideally, such a
toolbox should support the boolean operations of union, intersection
and complement and decide the problems of membership and inclusion, by
building finite recognizer algebras from the syntactic description of
sets, as regular grammars.

* [http://nts.imag.fr/images/5/5e/InfiniteAlphabetAutomata.pdf Verifying Concurrent Systems with Automata over Infinite Alphabets]

The goal of this internship is to study extensions of finite-state automata over infinite alphabets and apply them to the verification of concurrent and distributed systems with unbounded numbers of threads. The internship comprises theoretical as well as implementation work, and will explore orthogonal domains, such as logic, automata theory and concurrency.

Phd and internship subjects

2024-12-08T19:27:05Z

Radu iosif:

== PhD subjects ==

* [https://nts.imag.fr/images/6/6f/Phd-pavedys.pdf Formal Modeling and Verification of Parameterized and Distributed Systems]

Applications of distributed systems are omnipresent, allowing to share resources and coordinate activities between geographically distributed parties. Designing, understanding, and validating distributed systems is challenging because of the huge number of interactions between components, some potentially leading to unpredictable scenarios. Mechanizing the analysis and verification of distributed systems is notoriusly difficult. Recently, there has been a notable trend to apply interactive theorem provers, i.e., using proof assistants, to the task. We propose to develop a complementary set of verification methods based, on generalizations of the more mechanized methods from the model-checking and automated theorem proving communities

== Internship subjects ==

* [http://nts.imag.fr/images/b/b1/TW2REG.pdf A Toolbox for Handling Infinite Sets of Graphs]

The goal of this internship is an implementation of a toolbox that
handles sets of graphs described as regular grammars. Ideally, such a
toolbox should support the boolean operations of union, intersection
and complement and decide the problems of membership and inclusion, by
building finite recognizer algebras from the syntactic description of
sets, as regular grammars.

* [http://nts.imag.fr/images/5/5e/InfiniteAlphabetAutomata.pdf Verifying Concurrent Systems with Automata over Infinite Alphabets]

The goal of this internship is to study extensions of finite-state automata over infinite alphabets and apply them to the verification of concurrent and distributed systems with unbounded numbers of threads. The internship comprises theoretical as well as implementation work, and will explore orthogonal domains, such as logic, automata theory and concurrency.

Phd and internship subjects

2024-12-08T18:00:13Z

Radu iosif:

File:TW2REG.pdf

2024-12-08T17:59:21Z

Radu iosif:

Radu Iosif

2024-09-12T14:48:08Z

Radu iosif:

[[File:Photo on 08-09-2022 at 15.38.jpg|left]]

[http://www.cnrs.fr CNRS] Research Director 
Co-head of the [https://www-verimag.imag.fr/Mohytos.html?lang=en MOHYTOS] group 

[http://www-verimag.imag.fr/ VERIMAG] laboratory, 
Office 208, [https://batiment.imag.fr/ IMAG building], 
Université Grenoble Alpes, 
CS 40700, 38058 GRENOBLE CEDEX 9 

Tel: +33 (0)4 57 42 22 21 

Email: ''Radu [dot] Iosif [at] univ-grenoble-alpes [dot] fr''

=== Research ===

* Looking for PhD students and interns: click here for a description of [[Phd and internship subjects]] [[File:new.jpg]]
* [[Recent publications]] ([https://dblp.org/pid/81/5510.html DBLP])
* [[Software|Contributed software]]
* Habilitation thesis [http://nts.imag.fr/images/6/6c/Hdr.pdf "Automata and Logics for Program Verification"] ([http://newstream.imag.fr/2016-09-29_Infinite-Systems-4.mp4 video])

=== Projects ===

* [https://raduiosif.github.io/PAVEDYS/ PAVEDYS] (2024-2028)
* [https://narco2022.github.io/ NARCO] (2022-2026)
* [http://vecolib.imag.fr/index.php/Main_Page VECOLIB] (2014-2018)
* [https://sites.google.com/site/veridyc/ VERIDYC] (2009-2013)
* [http://www.lsv.ens-cachan.fr/Projects/rntl-averiles/ AVERILES] (2006-2009)
* [http://www-verimag.imag.fr/~iosif/projects/ACI/aci-dynamo.html DYNAMO] (2003-2006)

=== Teaching ===

* [[Lat24|Logic and Automata Theory]]

=== PhD Students/Alumni ===

* Neven Villani (2024 --) "Automated Verification of Complex Reconfigurable Distributed Systems"
* Lucas Bueri (2021 -- 2024) "Logics for Reasoning about the Correctness of Reconfigurable Distributed Systems"
* Xiao Xu (2015 -- 2020) [https://hal.archives-ouvertes.fr/tel-02915498 "Generalisation of Alternating Automata over Infinite Alphabets"]
* Cristina Serban (2014 -- 2018) [https://tel.archives-ouvertes.fr/tel-01856199v1 "Automated Reasoning in Separation Logic with Inductive Definitions"]
* Filip Konecny (2009 -- 2012) [https://tel.archives-ouvertes.fr/tel-00805599/ "Relational Verification of Programs with Integer Data"]
* Jiri Simacek (2009 -- 2012) [https://tel.archives-ouvertes.fr/tel-00805794/ "Harnessing Forest Automata for Verification of Heap Manipulating Programs"]

=== Events ===

* An [https://www.ins2i.cnrs.fr/en/node/3457 article] from the CNRS [https://www.ins2i.cnrs.fr/en Information Science Institute] website (in French) [[File:new.jpg]]
* [https://cadeinc.org/Skolem-Award Skolem Award] for our 2013 CADE-24 paper [https://nts.imag.fr/images/f/f3/Cade13.pdf The Tree Width of Separation Logic with Recursive Definitions]
* [https://asl-workshop.github.io/asl22/ Advances in Separation Logics (ASL 2022)] Haifa, Israel, July 31st, 2022
* [https://easychair.org/cfp/IJCAR-2022 International Joint Conference on Automated Reasoning (IJCAR 2022)] Haifa, Israel, August 7-12, 2022
* [http://projects-verimag.imag.fr/movep2020/ 14th Summer School on Modelling and Verification of Parallel Processes (MOVEP 2020)] June 22-26, 2020, Grenoble
* [https://popl20.sigplan.org/home/adsl-2020#program Second Workshop on Automated Deduction for Separation Logics] January 20th, 2020, New Orleans, LA (affiliated with [https://popl20.sigplan.org/ POPL 2020])
* [http://gt-verif.loria.fr/Wiki.jsp?page=JA-2018 Journées GT Verif] 28, 29, 30 May 2018, Grenoble
* [http://adsl.univ-grenoble-alpes.fr/ First Workshop on Automated Deduction for Separation Logics] July 13th 2018, Oxford, UK (affiliated with [http://lics.siglog.org/lics18/ LICS 2018])
* [[Infinite Systems Verification Day]] September 29th 2016, Grenoble
* [http://cs.nyu.edu/ijcar2014/ IJCAR 2014] July 19-22 2014, Vienna
* [[AVM_2014|Alpine Verification Meeting 2014]]

Radu Iosif

2024-09-12T14:47:45Z

Radu iosif:

[[File:Photo on 08-09-2022 at 15.38.jpg|left]]

[http://www.cnrs.fr CNRS] Research Director 
Co-head of the [https://www-verimag.imag.fr/Mohytos.html?lang=en MOHYTOS] group 

[http://www-verimag.imag.fr/ VERIMAG] laboratory, 
Office 208, [https://batiment.imag.fr/ IMAG building], 
Université Grenoble Alpes, 
CS 40700, 38058 GRENOBLE CEDEX 9 

Tel: +33 (0)4 57 42 22 21 

Email: ''Radu [dot] Iosif [at] univ-grenoble-alpes [dot] fr''

=== Research ===

* Looking for PhD students and interns: click here for a description of [[Phd and internship subjects]] [[File:new.jpg]]
* [[Recent publications]] ([https://dblp.org/pid/81/5510.html DBLP])
* [[Software|Contributed software]]
* Habilitation thesis [http://nts.imag.fr/images/6/6c/Hdr.pdf "Automata and Logics for Program Verification"] ([http://newstream.imag.fr/2016-09-29_Infinite-Systems-4.mp4 video])

=== Projects ===

* [https://raduiosif.github.io/PAVEDYS/ PAVEDYS] (2024-2028)
* [https://narco2022.github.io/ NARCO] (2022-2026)
* [http://vecolib.imag.fr/index.php/Main_Page VECOLIB] (2014-2018)
* [https://sites.google.com/site/veridyc/ VERIDYC] (2009-2013)
* [http://www.lsv.ens-cachan.fr/Projects/rntl-averiles/ AVERILES] (2006-2009)
* [http://www-verimag.imag.fr/~iosif/projects/ACI/aci-dynamo.html DYNAMO] (2003-2006)

=== Teaching ===

* [[Lat24|Logic and Automata Theory]]

=== PhD Students/Alumni ===

* Neven Villani (2024-) "Automated Verification of Complex Reconfigurable Distributed Systems"
* Lucas Bueri (2021-2024) "Logics for Reasoning about the Correctness of Reconfigurable Distributed Systems"
* Xiao Xu (2015 -- 2020) [https://hal.archives-ouvertes.fr/tel-02915498 "Generalisation of Alternating Automata over Infinite Alphabets"]
* Cristina Serban (2014 -- 2018) [https://tel.archives-ouvertes.fr/tel-01856199v1 "Automated Reasoning in Separation Logic with Inductive Definitions"]
* Filip Konecny (2009 -- 2012) [https://tel.archives-ouvertes.fr/tel-00805599/ "Relational Verification of Programs with Integer Data"]
* Jiri Simacek (2009 -- 2012) [https://tel.archives-ouvertes.fr/tel-00805794/ "Harnessing Forest Automata for Verification of Heap Manipulating Programs"]

=== Events ===

* An [https://www.ins2i.cnrs.fr/en/node/3457 article] from the CNRS [https://www.ins2i.cnrs.fr/en Information Science Institute] website (in French) [[File:new.jpg]]
* [https://cadeinc.org/Skolem-Award Skolem Award] for our 2013 CADE-24 paper [https://nts.imag.fr/images/f/f3/Cade13.pdf The Tree Width of Separation Logic with Recursive Definitions]
* [https://asl-workshop.github.io/asl22/ Advances in Separation Logics (ASL 2022)] Haifa, Israel, July 31st, 2022
* [https://easychair.org/cfp/IJCAR-2022 International Joint Conference on Automated Reasoning (IJCAR 2022)] Haifa, Israel, August 7-12, 2022
* [http://projects-verimag.imag.fr/movep2020/ 14th Summer School on Modelling and Verification of Parallel Processes (MOVEP 2020)] June 22-26, 2020, Grenoble
* [https://popl20.sigplan.org/home/adsl-2020#program Second Workshop on Automated Deduction for Separation Logics] January 20th, 2020, New Orleans, LA (affiliated with [https://popl20.sigplan.org/ POPL 2020])
* [http://gt-verif.loria.fr/Wiki.jsp?page=JA-2018 Journées GT Verif] 28, 29, 30 May 2018, Grenoble
* [http://adsl.univ-grenoble-alpes.fr/ First Workshop on Automated Deduction for Separation Logics] July 13th 2018, Oxford, UK (affiliated with [http://lics.siglog.org/lics18/ LICS 2018])
* [[Infinite Systems Verification Day]] September 29th 2016, Grenoble
* [http://cs.nyu.edu/ijcar2014/ IJCAR 2014] July 19-22 2014, Vienna
* [[AVM_2014|Alpine Verification Meeting 2014]]