Difference between revisions of "Recent publications"

From Numerical Transition Systems
Jump to: navigation, search
 
(137 intermediate revisions by the same user not shown)
Line 3: Line 3:
 
==== Pending ====
 
==== Pending ====
  
−
* M. Bozga, R. Iosif and F. Konecny. Deciding Conditional Termination, [http://arxiv.org/abs/1302.2762 arXiv:1302.2762] [cs.LO]
+
* Lucas Bueri, Radu Iosif and Florian 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]
 +
* Mark Chimes, Radu Iosif and Florian Zuleger. Tree-Verifiable Graph Grammars. [https://arxiv.org/abs/2402.17015 arXiv:2402.17015]
 +
* 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]
 +
* R. Iosif and F. Zuleger. Characterizations of Definable Context-Free Graphs. [https://arxiv.org/abs/2310.04764 arXiv:2310.04764]
 +
* 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 ====
 
==== Journals ====
  
−
* R. Iosif and A. Rogalewicz. Automata-based termination proofs, Computing and Informatics, No. 4 (2013) (to appear)
+
* 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)
−
* A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro and T. Vojnar. [http://nts.imag.fr/images/1/12/Fmsd10.pdf Programs with Lists are Counter Automata], Formal Methods in System Design, Volume 38(2) (2011) pp 158-192  
+
* 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, S. Perarnau. Quantitative Separation Logic and Programs with Lists,  Journal of Automated Reasoning, Volume 45(2) (2010) pp 131-156
+
* 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)
−
* P. Habermehl, R. Iosif, T. Vojnar. Automata-based Verification of Programs with Tree Updates, Acta Informatica: Volume 47(1) (2010) pp 1-31
+
* 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)
−
* M. Bozga, R. Iosif, Y. Lakhnech. Flat Parametric Counter Automata. Fundamenta Informaticae, Volume 91(2) (2009) pp 275 - 303
+
* 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)
−
* R. Iosif. Symmetry Reductions for Model Checking of Concurrent Dynamic Software. Software Tools for Technology Transfer, Volume 6(4), pp 302 - 319
+
* 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]]
−
* R. Iosif, M. Dwyer, J. Hatcliff. Translating Java for Multiple Model Checkers: the Bandera Back End. Formal Methods in System Design, Volume 26(2) (2005), pp 137-180
+
* 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, R. Sisto. Temporal Logic Properties of Java Objects. Journal of Systems and Software, Volume 68(3) (2003) pp 243-251
+
* R. Iosif and A. Rogalewicz. [[Media:Cai13.pdf|Automata-based termination proofs]] Computing and Informatics, Vol.22 (2013) pp 1001-1035
−
* C. Demartini, R. Iosif, R. Sisto. A Deadlock Detection Tool For Concurrent Java Programs. Software: Practice & Experience, Volume 29(7) (1999), pp 577-603
+
* 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 ====
 
==== Conferences ====
  
−
* R. Iosif, A. Rogalewicz, J. Simácek. The Tree Width of Separation Logic with Recursive Definitions. CADE 2013 (to appear) '''Best Paper Award'''
+
* 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
−
* P. Ganty, R. Iosif, F. Konecny. Underapproximation of Procedure Summaries for Integer Programs. TACAS 2013, pp 245-259
+
* 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
−
* H. Hojjat, R. Iosif, F. Konecny, V. Kuncak, P. Ruemmer. Accelerating Interpolants. ATVA 2012, pp 187-202
+
* 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
−
* H. Hojjat, F. Konecny, F. Garnier, R. Iosif, V. Kuncak, P. Ruemmer. A Verification Toolkit for Numerical Transition Systems - Tool Paper. FM 2012, pp 247-251
+
* 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, F. Konecny. Deciding Conditional Termination. TACAS 2012, pp 252-266
+
* M. Bozga, R. Iosif. [[Media:Facs21.pdf|Verifying Safety Properties of Inductively Defined Parameterized Systems]]. FACS 2021, pp 95-114
−
* M. Bozga, R. Iosif, F. Konecny. Fast Acceleration of Ultimately Periodic Relations. CAV 2010, pp 227-242
+
* 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. Bozga, P. Habermehl, R. Iosif, F. Konecny, T. Vojnar. Automatic Verification of Integer Array Programs. CAV 2009, pp 157-172
+
* 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. Bozga, C. Gîrlea, R. Iosif. Iterating Octagons. TACAS 2009, pp 337-351
+
* 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
−
* R. Iosif, A. Rogalewicz. Automata-Based Termination Proofs. CIAA 2009, pp 165-177
+
* 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
−
* M. Bozga, R. Iosif, S. Perarnau. Quantitative Separation Logic and Programs with Lists. IJCAR 2008, pp 34-49
+
* R. Iosif and X. Xu. [[Media:Cav2019.pdf|Alternating Automata Modulo First Order Theories]], CAV 2019, Part II, pp 43--63
−
* P. Habermehl, R. Iosif, T. Vojnar. What Else Is Decidable about Integer Arrays? FoSSaCS 2008, pp 474-489
+
* 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
−
* P. Habermehl, R. Iosif, T. Vojnar. A Logic of Singly Indexed Arrays. LPAR 2008, pp 558-573
+
* M. Echenim, R. Iosif, N. Peltier. [[Media:Tableaux2019.pdf|Prenex Separation Logic with One Selector Field]]. TABLEAUX 2019, pp 409--427
−
* P. Habermehl, R. Iosif, A. Rogalewicz, T. Vojnar. Proving Termination of Tree Manipulating Programs. ATVA 2007, pp 145-161
+
* 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
−
* M. Bozga, R. Iosif. On Flat Programs with Lists. VMCAI 2007, pp 122-136
+
* 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
−
* A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, T. Vojnar. Programs with Lists Are Counter Automata. CAV 2006, pp 517-531
+
* R. Iosif and X. Xu. [[Media:Tacas2018.pdf|Abstraction Refinement for Emptiness Checking of Alternating Data Automata]] TACAS 2018, pp 93-111
−
* M. Bozga, R. Iosif, Y. Lakhnech. Flat Parametric Counter Automata. ICALP 2006, pp 577-588
+
* 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
−
* P. Habermehl, R. Iosif, T. Vojnar. Automata-Based Verification of Programs with Tree Updates. TACAS 2006, pp 350-364
+
* 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
−
* M. Bozga, R. Iosif. On Decidability Within the Arithmetic of Addition and Divisibility. FoSSaCS 2005, pp 425-439
+
* 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
−
* M. Bozga, R. Iosif, Y. Lakhnech. On Logics of Aliasing. SAS 2004, pp 344-360
+
* 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
−
* M. Bozga, R. Iosif, Y. Lakhnech. Storeless semantics and alias logic. PEPM 2003, pp 55-65
+
* P. Ganty and R. Iosif. [http://arxiv.org/abs/1405.3069 Interprocedural Reachability for Flat Integer Programs] FCT 2015, pp 133-145.
−
* R. Iosif. Symmetry Reduction Criteria for Software Model Checking. SPIN 2002, pp 22-41
+
* R. Iosif, A. Rogalewicz and T. Vojnar. [[Media:Atva14.pdf|Deciding Entailments in Inductive Separation Logic with Tree Automata]] ATVA 2014, pp 201-218
−
* R. Iosif. Exploiting Heap Symmetries in Explicit-State Model Checking of Software. ASE 2001, pp 254-261
+
* 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

Latest revision as of 16:34, 28 February 2024

Newspapers-stacked.jpg

Pending

  • Lucas Bueri, Radu Iosif and Florian Zuleger. Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations arXiv:2402.16150
  • Mark Chimes, Radu Iosif and Florian Zuleger. Tree-Verifiable Graph Grammars. arXiv:2402.17015
  • M. Bozga, L. Bueri, R. Iosif and F. Zuleger. The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations. arXiv:2310.09542
  • R. Iosif and F. Zuleger. Characterizations of Definable Context-Free Graphs. arXiv:2310.04764
  • M. Bozga, R. Iosif and J. Sifakis. Local Reasoning about Parametric and Reconfigurable Component-based Systems. arXiv:1908.11345
  • M. Bozga, R. Iosif and F. Konecny. The Complexity of Reachability Problems for Flat Counter Machines with Periodic Loops arXiv:1307.5321

Journals

Conferences

Retrieved from "http://nts.imag.fr/index.php?title=Recent_publications&oldid=1156"