Publications of Arnaud Sangnier

2016

• G. Delzanno, A. Sangnier, R. Traverso. Adding Data Registers to Parameterized Networks with Broadcast. Fundamenta Informaticae 143(3-4), pages 287-316.2016.
  [PDF|bibtex] Erratum : Lemma 4.8 and Theorem 4.2 are false. Cov (*, 1) seems to not be in PSPACE.


• P. Abulla, G. Delzanno, O. Rezine, A. Sangnier, R. Traverso. Parameterized verification of time-sensitive models of ad hoc network protocols. Theoretical Computer Science 612, pages 1--22. Elsevier Science Publishers, 2016.
  [PDF|bibtex]

2015

• S. Demri, A. K. Dhar, A. Sangnier. Taming past LTL and flat counter systems. Information and Computation 242, pages 306-339. Elsevier Science Publishers, 2015.
  [PDF|bibtex]

2010

• S. Demri, R. Lazic, A. Sangnier. Model checking memoryful linear-time logics over one-counter automata. Theoretical Computer Science 411 (22-24), pages 2298-2316. Elsevier Science Publishers, 2010.
  [PDF|bibtex]

2021

• B. Bollig , O. Stietel, A. Sangnier. Local First-Order Logic with Two Data Values. . In FSTTCS'21, LIPIcs , pages . Leibniz-Zentrum für Informatik, 2021.
  [PDF|Long version]
• B. Bollig , F. Ryabinin, A. Sangnier. Reachability in Distributed Memory Automata. . In CSL'21, LIPIcs 183, pages 13:1--13:16. Leibniz-Zentrum für Informatik, 2021.
  [PDF]

2020

• F. Horn, A. Sangnier. Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks. In CONCUR'20, LIPIcs 171, pages 46:1-46:16. Leibniz-Zentrum für Informatik, 2020.
  [PDF|Long version]

2019

• C. Delporte-Gallet, H. Fauconnier, Y. Jurski, F. Laroussinie, A. Sangnier. Towards Synthesis of Distributed Algorithms with SMT Solvers. In NETYS'19, LNCS 11704, pages 200-216. Springer, 2019.
  [PDF|bibtex]

2017

• B. Bollig, K. Quaas, A. Sangnier . The Complexity of Flat Freeze LTL. In CONCUR'17, LIPIcs 85, pages 33:1-33:16. Leibniz-Zentrum für Informatik, 2017.
  [PDF|Long version|bibtex]
• N. Decker, P. Habermehl, M. Leucker, A. Sangnier, D. Thoma . Model-checking Counting Temporal Logics on Flat Structures. In CONCUR'17, LIPIcs 85, pages 29:1-29:17. Leibniz-Zentrum für Informatik, 2017.
  [PDF|Long version|bibtex]
• A. Sangnier, N. Sznajder, M. Potop-Butucaru, S. Tixeuil. Parameterized verification of algorithms for oblivious robots on a ring. In FMCAD'17, IEEE.
  [PDF|bibtex]

2016

• R. Iosif, A. Sangnier. How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?.In ATVA'16, LNCS 9938, pages 89-105. Springer, 2016.
  [PDF|Long version|bibtex]
• P. Bouyer, N. Markey, M. Randour, A. Sangnier, D. Stan. Reachability in Networks of Register Protocols under Stochastic Schedulers.In ICALP'16, LIPIcs 55, pages 106:1-106:14 Leibniz-Zentrum für Informatik, 2016.
  [PDF|Long version|bibtex]


• P. A. Abdulla, R. Ciobanu, R. Mayr, A. Sangnier, J. Sproston. Qualitative Analysis of VASS-Induced MDPs.In FoSSaCS'16, LNCS 9634, pages 319-334. Springer, 2016.
  [PDF|Long version|bibtex]

2015

• F. Laroussinie, N. Markey, A. Sangnier. ATLsc with partial observation. In GANDALF'15, EPTCS 193, pages 43-57. 2015.
  [PDF|Long version|bibtex]
• N. Bertrand, P. Fournier, A. Sangnier. Distributed Local Strategies in Broadcast Networks. In CONCUR'15, LIPIcs 42, pages 44-57. Leibniz-Zentrum für Informatik, 2015.
  [PDF|Long version|bibtex]

2014

• S. Demri, A. K. Dhar, A. Sangnier. Equivalence between model-checking flat counter systems and Presburger arithmetic. In RP'14, LNCS 8762, pages 85-97. Springer, 2014.
  [PDF|Long version|bibtex]
• N. Bertrand, P. Fournier, A. Sangnier. Playing with probabilities in Reconfigurable Broadcast Networks. In FoSSaCS'14, LNCS 8412, pages 134-148. Springer, 2014.
  [PDF|Long version|bibtex]

2013

• G. Delzanno, A. Sangnier, R. Traverso. Parameterized Verification of Broadcast Networks of Register Automata. In RP'13, LNCS 8169, pages 109-121. Springer, 2013.
  [PDF|bibtex] Erratum : Theorem 2 is false. Cov (*, 1) seems to not be in PSPACE.
• P. A. Abdulla, R. Mayr, A. Sangnier, J. Sproston. Solving Parity Games on Integer Vectors. In CONCUR'13, LNCS 8052, pages 106-120. Springer, 2013.
  [PDF|Long version|bibtex]
• S. Demri, A. K. Dhar, A. Sangnier. On the Complexity of Verifying Regular Properties on Flat Counter Systems. In ICALP'13 (2), LNCS 7966, pages 162-173. Springer, 2013.
  [PDF|Long version|bibtex]

2012

• G. Delzanno, A. Sangnier, R. Traverso, G. Zavattaro. On the Complexity of Parameterized Reachability in Reconfigurable Broadcast Networks. In FSTTCS'12, LIPIcs 18, pages 289-300. Leibniz-Zentrum für Informatik, 2012.
  [PDF|PDF (long version)|bibtex]
• S. Demri, A. K. Dhar, A. Sangnier. Taming Past LTL and Flat Counter Systems. In IJCAR'12, LNAI 7634, pages 179-193. Springer, 2012.
  [PDF|PDF (long version)|bibtex]
• G. Delzanno, A. Sangnier, G. Zavattaro. Verification of Ad Hoc Networks with Node and Communication Failures. In FMOODS/FORTE'12, LNCS 7273, pages 235-250. Springer, 2012.
  [PDF|bibtex]
• N. Bertrand, B. König, G. Delzanno, A. Sangnier, J. Stückrath. On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. In RTA'12, LIPIcs 15, pages 101-116. Leibniz-Zentrum für Informatik, 2012.
  [PDF|PDF (long version)|bibtex]

2011

• P. Abulla, G. Delzanno, O. Rezine, A. Sangnier, R. Traverso. On the Verification of Timed Ad Hoc Networks. In FORMATS'11, LNCS 6919, pages 256-270. Springer, 2011.
  [PDF|PDF (long version)|bibtex]
• G. Delzanno, A. Sangnier, G. Zavattaro. On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks. In FoSSaCS'11, LNCS 6604, pages 441-455. Springer, 2011.
  [PDF|PDF (long version)|bibtex]

2010

• S. Labbé, A. Sangnier. Formal verification of industrial software with dynamic memory management. In PRDC'10. IEEE Computer Society, 2010.
  [PDF|bibtex]
• G. Delzanno, A. Sangnier, G. Zavattaro. Parameterized Verification of Ad Hoc Networks. In CONCUR'10, LNCS 6269, pages 313-327. Springer, 2010.
  [PDF|PDF (long version)|bibtex]
• S. Demri, A. Sangnier. When Model-Checking Freeze LTL over Counter Machines Becomes Decidable. In FOSSACS'10, LNCS 6014, pages 176-190. Springer, 2010.
  [PDF|PDF (long version)|bibtex]
• A. Finkel, A. Sangnier. Mixing coverability and reachability to analyze VASS with one zero-test. In SOFSEM'10, LNCS 5901, pages 394-406. Springer, 2010.
  [PDF|PDF (long version)|bibtex]

2009

• P.-A. Reynier, A. Sangnier. Weak Time Petri Nets strike back!. In CONCUR'09, LNCS 5710, pages 557-571. Springer, 2009.
  [PDF|Long version|bibtex]
• A. Finkel, E. Lozes, A. Sangnier. Towards Model-Checking Programs with Lists. In Infinity in Logic anc Computation, LNAI 5489, pages 56-86. Springer 2009.
  [PDF|bibtex]
• F. Bouchy, A. Finkel, A. Sangnier. Reachability in Timed Counter Systems. In Joint Proceedings of INFINITY'06,'07,'08, ENTCS 239, pages 167-178. Elsevier Science Publishers, 2009.
  [PDF|bibtex]

2008

• A. Finkel, A. Sangnier. Reversal-bounded Counter Machines Revisited. In MFCS'08, LNCS 5162, pages 323-334. Springer, 2008.
  [PDF|PDF (long version)|bibtex]
• S. Demri, R. Lazic, A. Sangnier. Model checking freeze LTL over one-counter automata. In FoSSaCS'08, LNCS 4962, pages 490-504. Springer, 2008.
  [PDF|PDF (long version)|bibtex]

2007

• D. D'Aprile, S. Donatelli, A. Sangnier, J. Sproston. From Time Petri Nets to Timed Automata: An Untimed Approach.In TACAS'07, LNCS 4424, pages 216-230. Springer, 2007.
  [PDF|bibtex]

2008

• A. Sangnier. Vérification de systèmes avec compteurs et pointeurs. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2008.
  [PDF|bibtex]

2005

• A. Sangnier. Toward Verification of Time Coloured Petri Nets. Rapport de Master 2 Recherche, Master Systèmes et Applications Réparties, Paris 6, France, September 2005.
  [PDF|bibtex]

2007

• A. Finkel, E. Lozes, A. Sangnier. Towards Model Checking Pointer Systems. In ILC'07. 2007.
  [PDF|bibtex]

2006

• S. Bardin, A. Finkel, E. Lozes, A. Sangnier. From Pointer Systems to Counter Systems Using Shape Analysis. In AVIS'06. 2006.
  [PDF|bibtex]