Difference between revisions of "Recent publications"

From Numerical Transition Systems
Jump to: navigation, search
(30 intermediate revisions by the same user not shown)
Line 3: Line 3:
 
==== Pending ====
 
==== Pending ====
  
* M. Echenim, R. Iosif and N. Peltier. The Complexity of Prenex Separation Logic with One Selector [https://arxiv.org/abs/1804.03556  arXiv:1804.03556]
+
* M. Echenim, R. Iosif, N. Peltier. Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules [https://hal.archives-ouvertes.fr/hal-02951859 hal-02951859]
* M. Echenim, R. Iosif and N. Peltier. On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic [https://arxiv.org/abs/1802.00195 arXiv:1802.00195]
+
* M. Echenim, R. Iosif, N. Peltier. Unifying Decidable Entailments in Separation Logic with Inductive Definitions [https://arxiv.org/abs/2012.14361 arXiv:2012.14361]
* R. Iosif and C. Serban. Complete Cyclic Proof Systems for Inductive Entailments [https://arxiv.org/abs/1707.02415 arXiv:1707.02415]
+
* M. Bozga, R. Iosif. Verifying Safety Properties of Inductively Defined Parameterized Systems. [https://arxiv.org/abs/2008.04160  arXiv:2008.04160]
 +
* 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]
 
* 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 ====
  
 +
* 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)
 
* 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]]
 
* 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
 
* 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
Line 24: Line 28:
 
==== Conferences ====
 
==== Conferences ====
  
* R. Iosif and X. Xu. [[Media:Tacas2018.pdf|Abstraction Refinement for Emptiness Checking of Alternating Data Automata]] TACAS 2018, to appear
+
* 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
 
* 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
 
* 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

Revision as of 10:37, 16 February 2021

Newspapers-stacked.jpg

Pending

  • M. Echenim, R. Iosif, N. Peltier. Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules hal-02951859
  • M. Echenim, R. Iosif, N. Peltier. Unifying Decidable Entailments in Separation Logic with Inductive Definitions arXiv:2012.14361
  • M. Bozga, R. Iosif. Verifying Safety Properties of Inductively Defined Parameterized Systems. arXiv:2008.04160
  • 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