Publications : INFINI

[GH21]
S. Göller and M. Hilaire. Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete. In Proceedings of the 38th Annual Symposium on Theoretical Aspects of Computer Science (STACS'21), volume 187 of Leibniz International Proceedings in Informatics, Saarbrücken, Germany, March 2021. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.STACS.2021.36.
BibTex | DOI | Web page | PDF ]
[DLM21a]
S. Demri, É. Lozes, and A. Mansutti. A Complete Axiomatisation for Quantifier-Free Separation Logic. Research Report 2006.05156v2, Computing Research Repository, February 2021. 63 pages.
BibTex | Web page | PDF ]
[DFM21]
S. Demri, R. Fervari, and A. Mansutti. Internal proof calculi for modal logics with separating conjunction. Journal of Logic and Computation, 2021. Accepted for publication to the Special issue of JLC on External and Internal Calculi for Non Classical Logics.
BibTex | Web page | PDF ]
[DLM21b]
S. Demri, É. Lozes, and A. Mansutti. The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic. ACM Transactions on Computational Logic, 2021. To appear.
BibTex | Web page | PDF ]
[Lop21]
A. Lopez. Preservation Theorems Through the Lens of Topology. In Proceedings of the 29th Annual EACSL Conference on Computer Science Logic (CSL'21), Leibniz International Proceedings in Informatics, pages 32:1--32:17, Ljubljana, Slovenia, January 2021. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2021.32.
BibTex | DOI | Web page | PDF ]
[Sch21]
Ph. Schnoebelen. On flat lossy channel machines. In Proceedings of the 29th Annual EACSL Conference on Computer Science Logic (CSL'21), Leibniz International Proceedings in Informatics, pages 37:1--37:22, Ljubljana, Slovenia, January 2021. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2021.37.
BibTex | DOI | Web page | PDF ]
[Man20b]
A. Mansutti. Reasoning with Separation Logics: Complexity, Expressive Power, Proof Systems. Thèse de doctorat, École Normale Supérieure Paris-Saclay, France, December 2020.
BibTex | Web page | PDF ]
[FP20]
A. Finkel and M. Praveen. Verification of Flat FIFO Systems. Logical Methods in Computer Science, 20(4), October 2020.
doi: 10.23638/LMCS-16(4:4)2020.
BibTex | DOI | Web page ]
[BFS20]
B. Bollig, A. Finkel, and A. Suresh. Bounded Reachability Problems are Decidable in FIFO Machines. In Proceedings of the 31st International Conference on Concurrency Theory (CONCUR'20), volume 171 of Leibniz International Proceedings in Informatics, pages 49:1--49:17, Vienna, Austria, September 2020. Leibniz-Zentrum für Informatik.
BibTex | Web page ]
[BD20]
F. Belardinelli and S. Demri. Reasoning with a Bounded Number of Resources in ATL+. In Proceedings of the 24th European Conference on Artificial Intelligence (ECAI'20), pages 624--631, Santiago de Compostela, Spain, September 2020. IOS Press.
doi: 10.3233/FAIA200147.
BibTex | DOI | Web page | PDF ]
[BDFM20]
B. Bednarczyk, S. Demri, R. Fervari, and A. Mansutti. Modal Logics with Composition on Finite Forests: Expressivity and Complexity. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'20), pages 167--180, Saarbrucken, Germany, July 2020. IEEE Press.
doi: https://dl.acm.org/doi/10.1145/3373718.3394787.
BibTex | DOI | PDF ]
[BDM20]
B. Bednarczyk, S. Demri, and A. Mansutti. A Framework for Reasoning about Dynamic Axioms in Description Logics. In Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI'20). IJCAI organization, July 2020.
BibTex | Web page ]
[Man20a]
A. Mansutti. An auxiliary logic on trees: on the Tower-hardness of logics featuring reachability and submodel reasoning. In Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20), Lecture Notes in Computer Science, pages 462--481, Dublin, Ireland, April 2020. Springer.
doi: 10.1007/978-3-030-45231-5_24.
BibTex | DOI ]
[FHK20b]
A. Finkel, S. Haddad, and I. Khmelnitsky. Minimal coverability tree construction made complete and efficient. In Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20), Lecture Notes in Computer Science, pages 237--256, Dublin, Ireland, April 2020. Springer.
doi: 10.1007/978-3-030-45231-5_13.
BibTex | DOI ]
[ADL20]
N. Alechina, S. Demri, and B. Logan. Parameterised Resource-Bounded ATL. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI'20), pages 7040--7046. AAAI Press, February 2020.
doi: https://doi.org/10.1609/aaai.v34i05.6189.
BibTex | DOI | Web page ]
[DLM20]
S. Demri, É. Lozes, and A. Mansutti. Internal Calculi for Separation Logics. In Proceedings of the 28th Annual EACSL Conference on Computer Science Logic (CSL'20), Leibniz International Proceedings in Informatics, Barcelona, Spain, January 2020. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2020.19.
BibTex | DOI | Web page ]
[Lop20]
A. Lopez. Preservation Theorems Through the Lens of Topology. Research Report 2007.07879, Computing Research Repository, 2020.
BibTex | Web page | PDF ]
[Fin20]
A. Finkel. From Well Structured Transition Systems to Program Verification. In Proceedings of 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis (VPT/HCVS@ETAPS 2020), pages 44--49, Dublin, Ireland, 2020. Electronic Proceedings in Theoretical Computer Science.
doi: 10.4204/EPTCS.320.3.
BibTex | DOI | Web page | PDF ]
[GMG20]
P. Gastin, A. Manuel, and R. Govind. Reversible Regular Languages: Logical and Algebraic Characterisations. Fundamenta Informaticae, 2020. To appear.
BibTex ]
[FHK20a]
A. Finkel, S. Haddad, and I. Khmelnitsky. Commodification of accelerations for the Karp and Miller Construction. Discrete Event Dynamic Systems: Theory and Applications, 2020.
doi: 10.1007/s10626-020-00331-z.
BibTex | DOI | Web page ]
[FG20]
A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part I: completions. Mathematical Structures in Computer Science, 30(7):752--832, 2020.
doi: 10.1017/S0960129520000195.
BibTex | DOI | Web page | PDF ]
[BFG20]
M. Blondin, A. Finkel, and J. Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. Logical Methods in Computer Science, 16(2), 2020.
doi: 10.23638/LMCS-16(2:13)2020.
BibTex | DOI | Web page ]
[GHK+20]
J. Goubault-Larrecq, S. Halfon, P. Karandikar, K. Narayan Kumar, and Ph. Schnoebelen. The Ideal Approach to Computing Closed Subsets in Well-Quasi-Orderings. In Well-Quasi Orders in Computation, Logic, Language and Reasoning, volume 53 of Trends In Logic, pages 55--105. Springer, 2020.
doi: 10.1007/978-3-030-30229-0_3.
BibTex | DOI ]
[DSS20]
M. Džamonja, S. Schmitz, and Ph. Schnoebelen. On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders. In Well-Quasi Orders in Computation, Logic, Language and Reasoning, volume 53 of Trends In Logic, pages 2--54. Springer, 2020.
doi: 10.1007/978-3-030-30229-0_2.
BibTex | DOI ]
[GF19]
E. Gupta and A. Finkel. The well structured problem for Presburger counter machines. In Proceedings of the 39th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'19), Leibniz International Proceedings in Informatics, pages 41:1--41:15, Bombay, India, December 2019. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2019.41.
BibTex | DOI | Web page | PDF ]
[FHK19b]
A. Finkel, S. Haddad, and I. Khmelnitsky. Réification des accélérations pour la construction de Karp et Miller. In Actes du 12ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'19), Angers, France, November 2019. HAL.
BibTex | Web page | PDF ]
[SZ19]
S. Schmitz and G. Zetzsche. Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets. In Proceedings of the 13th Workshop on Reachability Problems in Computational Models (RP'19), volume 11674 of Lecture Notes in Computer Science, pages 193--201, Brussels, Belgium, September 2019. Springer.
doi: 10.1007/978-3-030-30806-3_15.
BibTex | DOI | Web page | PDF ]
[Lop19]
A. Lopez. Théorèmes de préservation. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2019.
BibTex ]
[Sur19]
A. Suresh. Termination, boundedness and reachability for input-bounded FIFO Machines. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2019.
BibTex ]
[FP19]
A. Finkel and M. Praveen. Verification of Flat FIFO Systems. In Proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19), volume 140 of Leibniz International Proceedings in Informatics, pages 12:1--12:17, Amsterdam, The Netherlands, August 2019. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CONCUR.2019.12.
BibTex | DOI | Web page | PDF ]
[Sch19]
S. Schmitz. The Parametric Complexity of Lossy Counter Machines. In Proceedings of the 46th International Colloquium on Automata, Languages and Programming (ICALP'19), volume 132 of Leibniz International Proceedings in Informatics, pages 129:1--129:15, Patras, Greece, July 2019. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.ICALP.2019.129.
BibTex | DOI | Web page | PDF ]
[Lic19]
A. Lick. XPath-like Query Logics: Proof Systems and Real-World Applicability. Thèse de doctorat, École Normale Supérieure Paris-Saclay, France, July 2019.
BibTex | Web page | PDF ]
[BLS19]
D. Baelde, A. Lick, and S. Schmitz. Decidable XPath Fragments in the Real World. In Proceedings of the 38th Annual ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS'19), pages 285--302, Amsterdam, Netherlands, June-July 2019. ACM Press.
doi: 10.1145/3294052.3319685.
BibTex | DOI | Web page ]
[BD19b]
F. Belardinelli and S. Demri. Resource-bounded ATL: the Quest for Tractable Fragments. In Proceedings of the 18th International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS'19), pages 206--214, Montreal, Canada, June 2019. ACM Press.
BibTex | Web page | PDF ]
[DFM19]
S. Demri, R. Fervari, and A. Mansutti. Axiomatising logics with separating conjunctions and modalities. In Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA'19), volume 11468 of Lecture Notes in Artificial Intelligence, pages 692--708, Rende, Italy, June 2019. Springer.
doi: 10.1007/978-3-030-19570-0_45.
BibTex | DOI | Web page | PDF ]
[FHK19a]
A. Finkel, S. Haddad, and I. Khmelnitsky. Coverability and Termination in Recursive Petri Nets. In Proceedings of the 40th International Conference on Applications and Theory of Petri Nets (PETRI NETS'19), volume 11522 of Lecture Notes in Computer Science, pages 429--448, Aachen, Germany, June 2019. Springer.
doi: 10.1007/978-3-030-21571-2_23.
BibTex | DOI | Web page | PDF ]
[BD19a]
B. Bednarczyk and S. Demri. Why propositional quantification makes modal logics on trees robustly hard ? In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'19), pages 1--13, Vancouver, Canada, June 2019. IEEE Press.
doi: 10.1109/LICS.2019.8785656.
BibTex | DOI | PDF ]
[LS19b]
J. Leroux and S. Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'19), pages 1--13, Vancouver, Canada, June 2019. IEEE Press.
doi: 10.1109/LICS.2019.8785796.
BibTex | DOI | Web page ]
[JS19]
P. Jančar and S. Schmitz. Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'19), pages 1--12, Vancouver, Canada, June 2019. IEEE Press.
doi: 10.1109/LICS.2019.8785848.
BibTex | DOI | Web page ]
[KS19]
P. Karandikar and Ph. Schnoebelen. The height of piecewise-testable languages and the complexity of the logic of subwords. Logical Methods in Computer Science, 15(2):6:1--6:27, April 2019.
BibTex | Web page | PDF ]
[DF19]
S. Demri and R. Fervari. The power of modal separation logics. Journal of Logic and Computation, 29(8):1139--1184, 2019.
BibTex | PDF ]
[HS19]
S. Halfon and Ph. Schnoebelen. On shuffle products, acyclic automata and piecewise-testable languages. Information Processing Letters, 145:68--73, 2019.
doi: 10.1016/j.ipl.2019.01.012.
BibTex | DOI ]
[LS19a]
R. Lazić and S. Schmitz. The Ideal View on Rackoff's Coverability Technique. Information and Computation, 2019. To appear.
BibTex | Web page ]
[LPSS19]
J. Leroux, M. Praveen, G. Sutre, and Ph. Schnoebelen. On Functions Weakly Computable by Pushdown Petri Nets and Related Systems. Logical Methods in Computer Science, 15(4), 2019.
doi: 10.23638/LMCS-15(4:15)2019.
BibTex | DOI | PDF ]
[Man18]
A. Mansutti. Extending propositional separation logic for robustness properties. In Proceedings of the 38th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'18), volume 122 of Leibniz International Proceedings in Informatics, pages 42:1--42:23, Ahmedabad, India, December 2018. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2018.42.
BibTex | DOI | Web page | PDF ]
[FLS18]
A. Finkel, J. Leroux, and G. Sutre. Reachability for Two-Counter Machines with One Test and One Reset. In Proceedings of the 38th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'18), volume 122 of Leibniz International Proceedings in Informatics, pages 31:1--31:14, Ahmedabad, India, December 2018. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2018.31.
BibTex | DOI | Web page | PDF ]
[BLS18b]
D. Baelde, A. Lick, and S. Schmitz. A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. In Proceedings of the 38th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'18), volume 122 of Leibniz International Proceedings in Informatics, pages 15:1--15:19, Ahmedabad, India, December 2018. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2018.15.
BibTex | DOI | Web page | PDF ]
[Dem18a]
S. Demri. On temporal and separation logics. In Proceedings of the 25th International Symposium on Temporal Representation and Reasoning (TIME'18), Leibniz International Proceedings in Informatics, pages 1:1--1:4, Warsaw, Poland, October 2018. Leibniz-Zentrum für Informatik.
BibTex | Web page ]
[Hil18]
M. Hilaire. Complexity of the reachability problem for parametric timed automata. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2018.
BibTex | PDF ]
[BLS18a]
D. Baelde, A. Lick, and S. Schmitz. A Hypersequent Calculus with Clusters for Linear Frames. In Proceedings of the 10th Conference on Advances in Modal Logics (AiML'18), pages 36--55, Bern, Switzerland, August 2018. College Publications.
BibTex | Web page ]
[DF18]
S. Demri and R. Fervari. On the complexity of modal separation logics. In Proceedings of the 10th Conference on Advances in Modal Logics (AiML'18), pages 179--198, Bern, Switzerland, August 2018. College Publications.
BibTex | Web page | PDF ]
[Hal18]
S. Halfon. On Effective Representations of Well Quasi-Orderings. Thèse de doctorat, École Normale Supérieure Paris-Saclay, France, June 2018.
BibTex | Web page | PDF ]
[DLM18]
S. Demri, É. Lozes, and A. Mansutti. The Effects of Adding Reachability Predicates in Propositional Separation Logic. In Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'18), volume 10803 of Lecture Notes in Computer Science, pages 476--493, Thessaloniki, Greece, April 2018. Springer.
BibTex | PDF ]
[GKLZ18]
M. Ganardi, D. König, M. Lohrey, and G. Zetzsche. Knapsack problems for wreath products. In Proceedings of the 35th Annual Symposium on Theoretical Aspects of Computer Science (STACS'18), volume 96 of Leibniz International Proceedings in Informatics, pages 32:1--32:13, Caen, France, February 2018. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.STACS.2018.32.
BibTex | DOI | Web page | PDF ]
[BFM18]
M. Blondin, A. Finkel, and P. McKenzie. Handling Infinitely Branching Well-structured Transition Systems. Information and Computation, 258:28--49, 2018.
doi: 10.1016/j.ic.2017.11.001.
BibTex | DOI ]
[BGH18]
B. Bollig, M.-L. Grindei, and P. Habermehl. Realizability of Concurrent Recursive Programs. Formal Methods in System Design, 53(3):339--362, 2018.
doi: 10.1007/s10703-017-0282-y.
BibTex | DOI ]
[Dem18b]
S. Demri. Reasoning about reversal-bounded counter machines. In Ewa Orlowska on Relational Methods in Logic and Computer Science, volume 17 of Outstanding Contributions to Logic, pages 441--479. Springer, 2018.
BibTex | Web page | PDF ]
[CYFFMF18]
R. Chane-Yack-Fa, M. Frappier, A. Mammar, and A. Finkel. Parameterized Verification of Monotone Information Systems. Formal Aspects of Computing, 30(3-4):463--489, 2018.
doi: 10.1007/s00165-018-0460-8.
BibTex | DOI | Web page ]
[Zet18]
G. Zetzsche. The Emptiness Problem for Valence Automata over Graph Monoids. Information and Computation, 2018. To appear.
BibTex ]
[LZ18]
M. Lohrey and G. Zetzsche. Knapsack in Graph Groups. Theory of Computing Systems, 62(1):192--246, January 2018.
doi: 10.1007/s00224-017-9808-3.
BibTex | DOI ]
[BHSS18]
B. Bérard, S. Haar, S. Schmitz, and S. Schwoon. The Complexity of Diagnosability and Opacity Verification for Petri Nets. Fundamenta Informaticae, 161(4):317--349, 2018.
doi: 10.3233/FI-2018-1706.
BibTex | DOI | Web page ]
[ABDL18]
N. Alechina, N. Bulling, S. Demri, and B. Logan. On the Complexity of Resource-Bounded Logics. Theoretical Computer Science, 750:69--100, 2018.
doi: 10.1016/j.tcs.2018.01.019.
BibTex | DOI | PDF ]
[CMvR+17]
W. Czerwiński, W. Martens, L. van Rooijen, M. Zeitoun, and G. Zetzsche. A Characterization for Decidable Separability by Piecewise Testable Languages. Discrete Mathematics & Theoretical Computer Science, 19(4), December 2017.
doi: 10.23638/DMTCS-19-4-1.
BibTex | DOI | Web page | PDF ]
[HKZ17]
M. Huschenbett, D. Kuske, and G. Zetzsche. The Monoid of Queue Actions. Semigroup Forum, 95(3):475--508, December 2017.
doi: 10.1007/s00233-016-9835-4.
BibTex | DOI ]
[BFG17]
M. Blondin, A. Finkel, and J. Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. In Proceedings of the 37th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'17), volume 93 of Leibniz International Proceedings in Informatics, pages 16:1--16:15, Kanpur, India, December 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2017.16.
BibTex | DOI | Web page | PDF ]
[DLL17]
S. Demri, É. Lozes, and D. Lugiez. On Symbolic Heaps Modulo Permission Theories. In Proceedings of the 37th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'17), volume 93 of Leibniz International Proceedings in Informatics, pages 25:1--25:14, Kanpur, India, December 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2017.25.
BibTex | DOI | Web page | PDF ]
[Sch17a]
S. Schmitz. Algorithmic Complexity of Well-Quasi-Orders. Mémoire d'habilitation, École Normale Supérieure Paris-Saclay, France, November 2017.
BibTex | Web page ]
[BFM17]
M. Blondin, A. Finkel, and P. McKenzie. Well Behaved Transition Systems. Logical Methods in Computer Science, 13(3):1--19, September 2017.
doi: 10.23638/LMCS-13(3:24)2017.
BibTex | DOI | Web page ]
[BLL17]
F. Bruse, M. Lange, and É. Lozes. Space-Efficient Fragments of Higher-Order Fixpoint Logic. In Proceedings of the 11th Workshop on Reachability Problems in Computational Models (RP'17), volume 10506 of Lecture Notes in Computer Science, pages 26--41, London, UK, September 2017. Springer.
doi: 10.1007/978-3-319-67089-8_3.
BibTex | DOI | Web page ]
[Rie17]
M. Riesner. Regularity of deterministic pushdown automata. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, August 2017.
BibTex ]
[Sch17b]
Ph. Schnoebelen. Ideal-Based Algorithms for the Symbolic Verification of Well-Structured Systems (Invited Talk). In Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS'17), volume 83 of Leibniz International Proceedings in Informatics, pages 85:1--85:4, Aalborg, Denmark, August 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.MFCS.2017.85.
BibTex | DOI | Web page | PDF ]
[FL17]
A. Finkel and É. Lozes. Synchronizability of Communicating Finite State Machines is not Decidable. In Proceedings of the 44th International Colloquium on Automata, Languages and Programming (ICALP'17), volume 80 of Leibniz International Proceedings in Informatics, pages 122:1--122:14, Warsaw, Poland, July 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.ICALP.2017.122.
BibTex | DOI | Web page | PDF ]
[HSZ17]
S. Halfon, Ph. Schnoebelen, and G. Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'17), pages 1--12, Reykjavik, Iceland, June 2017. IEEE Press.
doi: 10.1109/LICS.2017.8005141.
BibTex | DOI | Web page ]
[CJLS17]
Th. Colcombet, M. Jurdziński, R. Lazić, and S. Schmitz. Perfect Half Space Games. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'17), pages 1--11, Reykjavik, Iceland, June 2017. IEEE Press.
doi: 10.1109/LICS.2017.8005105.
BibTex | DOI | Web page ]
[BHSS17]
B. Bérard, S. Haar, S. Schmitz, and S. Schwoon. The Complexity of Diagnosability and Opacity Verification for Petri Nets. In Proceedings of the 38th International Conference on Applications and Theory of Petri Nets (PETRI NETS'17), volume 10258 of Lecture Notes in Computer Science, pages 200--220, Zaragoza, Spain, June 2017. Springer.
doi: 10.1007/978-3-319-57861-3_13.
BibTex | DOI | Web page ]
[BHM+17]
P. Bouyer, P. Hofman, N. Markey, M. Randour, and M. Zimmermann. Bounding Average-energy Games. In Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'17), Lecture Notes in Computer Science, pages 179--195, Uppsala, Sweden, April 2017. Springer.
doi: 10.1007/978-3-662-54458-7_11.
BibTex | DOI | Web page | PDF ]
[ZKL17]
G. Zetzsche, D. Kuske, and M. Lohrey. On Boolean closed full trios and rational Kripke frames. Theory of Computing Systems, 60(3):438--472, April 2017.
doi: 10.1007/s00224-016-9694-0.
BibTex | DOI ]
[BGHH17]
S. Böhm, S. Göller, S. Halfon, and P. Hofman. On Büchi one-counter automata. In Proceedings of the 34th Annual Symposium on Theoretical Aspects of Computer Science (STACS'17), Leibniz International Proceedings in Informatics, pages 14:1--14:13, Hannover, Germany, March 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.STACS.2017.14.
BibTex | DOI | Web page | PDF ]
[CG17]
A. Carayol and S. Göller. On long words avoiding Zimin patterns. In Proceedings of the 34th Annual Symposium on Theoretical Aspects of Computer Science (STACS'17), Leibniz International Proceedings in Informatics, pages 19:1--19:13, Hannover, Germany, March 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.STACS.2017.19.
BibTex | DOI | Web page | PDF ]
[LZ17]
M. Lohrey and G. Zetzsche. The Complexity of Knapsack in Graph Groups. In Proceedings of the 34th Annual Symposium on Theoretical Aspects of Computer Science (STACS'17), Leibniz International Proceedings in Informatics, pages 52:1--52:14, Hannover, Germany, March 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.STACS.2017.52.
BibTex | DOI ]
[DGLWM17]
S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Mery. Separation Logic with One Quantified Variable. Theory of Computing Systems, 61(2):371--461, 2017.
doi: 10.1007/s00224-016-9713-1.
BibTex | DOI | Web page | PDF ]
[DDS17]
S. Demri, A. Dhar, and A. Sangnier. Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic. Theoretical Computer Science, 735:2--23, 2017.
BibTex | PDF ]
[BFHH17]
M. Blondin, A. Finkel, C. Haase, and S. Haddad. The Logical View on Continuous Petri Nets. ACM Transactions on Computational Logic, 18(3):24:1--24:28, 2017.
doi: 10.1145/3105908.
BibTex | DOI | Web page | PDF ]
[DKW17]
S. Demri, D. Kapur, and C. Weidenbach. Special Issue of Selected Extended Papers of IJCAR 2014. Journal of Automated Reasoning, 58(1), 2017.
BibTex | Web page ]
[BKM16]
M. Blondin, A. Krebs, and P. McKenzie. The Complexity of Intersecting Finite Automata Having Few Final States. Computational Complexity, 25(4):775--814, December 2016. To appear.
doi: 10.1007/s00037-014-0089-9.
BibTex | DOI | Web page | PDF ]
[DGL16]
S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science, volume 58 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, October 2016.
BibTex | Web page ]
[HHK+16a]
M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, and É. Lozes. Multi-Buffer Simulations for Trace Language Inclusion. In Proceedings of the 7th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF'16), volume 226 of Electronic Proceedings in Theoretical Computer Science, pages 213--227, Catania, Italy, September 2016.
doi: 10.4204/EPTCS.226.15.
BibTex | DOI | Web page | PDF ]
[BDM16]
L. Beklemishev, S. Demri, and A. Maté, editors. Proceedings of the 11th Conference on Advances in Modal Logic (AiML'16), Budapest, Hungary, September 2016. College Publications.
BibTex | Web page ]
[Fin16]
A. Finkel. The Ideal Theory for WSTS. In Proceedings of the 10th Workshop on Reachability Problems in Computational Models (RP'16), volume 9899 of Lecture Notes in Computer Science, pages 1--22, Aalborg, Denmark, September 2016. Springer.
doi: 10.1007/978-3-319-45994-3_1.
BibTex | DOI | Web page | PDF ]
[ABDL16]
N. Alechina, N. Bulling, S. Demri, and B. Logan. On the Complexity of Resource-Bounded Logics. In Proceedings of the 10th Workshop on Reachability Problems in Computational Models (RP'16), volume 9899 of Lecture Notes in Computer Science, pages 36--50, Aalborg, Denmark, September 2016. Springer.
doi: 10.1007/978-3-319-45994-3_3.
BibTex | DOI | Web page | PDF ]
[KS16]
P. Karandikar and Ph. Schnoebelen. The height of piecewise-testable languages with applications in logical complexity. In Proceedings of the 25th Annual EACSL Conference on Computer Science Logic (CSL'16), volume 62 of Leibniz International Proceedings in Informatics, pages 37:1--37:22, Marseille, France, September 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2016.37.
BibTex | DOI | Web page | PDF ]
[GGL16]
M. Ganardi, S. Göller, and M. Lohrey. On the Parallel Complexity of Bisimulation over Finite Systems. In Proceedings of the 25th Annual EACSL Conference on Computer Science Logic (CSL'16), volume 62 of Leibniz International Proceedings in Informatics, pages 12:1--12:17, Marseille, France, September 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2016.12.
BibTex | DOI ]
[BFM16]
M. Blondin, A. Finkel, and P. McKenzie. Well Behaved Transition Systems. Research Report 1608.02636, Computing Research Repository, August 2016. 18 pages.
BibTex | Web page | PDF ]
[DFP16]
S. Demri, D. Figueira, and M. Praveen. Reasoning about Data Repetitions with Counter Systems. Logical Methods in Computer Science, 12(3):1:1--1:55, August 2016.
doi: 10.2168/LMCS-12(3:1)2016.
BibTex | DOI | Web page | PDF ]
[CH16]
D. Chistikov and C. Haase. The Taming of the Semi-Linear Set. In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP'16), volume 55 of Leibniz International Proceedings in Informatics, pages 128:1--128:14, Rome, Italy, July 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.ICALP.2016.128.
BibTex | DOI | Web page | PDF ]
[Zet16]
G. Zetzsche. The complexity of downward closure comparisons. In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP'16), volume 55 of Leibniz International Proceedings in Informatics, pages 123:1--123:14, Rome, Italy, July 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.ICALP.2016.123.
BibTex | DOI | Web page | PDF ]
[GS16]
J. Goubault-Larrecq and S. Schmitz. Deciding Piecewise Testable Separability for Regular Tree Languages. In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP'16), volume 55 of Leibniz International Proceedings in Informatics, pages 97:1--97:15, Rome, Italy, July 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.ICALP.2016.97.
BibTex | DOI | Web page ]
[GHLT16]
S. Göller, C. Haase, R. Lazić, and P. Totzke. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP'16), volume 55 of Leibniz International Proceedings in Informatics, pages 105:1--105:13, Rome, Italy, July 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.ICALP.2016.105.
BibTex | DOI | Web page ]
[LS16a]
R. Lazić and S. Schmitz. The Complexity of Coverability in ν-Petri Nets. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'16), pages 467--476, New York City, USA, July 2016. ACM Press.
doi: 10.1145/2933575.2933593.
BibTex | DOI | Web page ]
[CG16]
Th. Colcombet and S. Göller. Games with bound guess actions. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'16), pages 257--266, New York City, USA, July 2016. ACM Press.
doi: 10.1145/2933575.2934502.
BibTex | DOI | Web page | PDF ]
[DMZ16]
E. D'Osualdo, R. Meyer, and G. Zetzsche. First-order logic with reachability for infinite-state systems. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'16), pages 457--466, New York City, USA, July 2016. ACM Press.
doi: 10.1145/2933575.2934552.
BibTex | DOI | Web page | PDF ]
[ACH+16]
M. F. Atig, D. Chistikov, P. Hofman, K. N. Kumar, P. Saivasan, and G. Zetzsche. Complexity of regular abstractions of one-counter languages. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'16), pages 207--216, New York City, USA, July 2016. ACM Press.
doi: 10.1145/2933575.2934561.
BibTex | DOI | Web page | PDF ]
[CFS16]
P. Chambart, A. Finkel, and S. Schmitz. Forward Analysis and Model Checking for Trace Bounded WSTS. Theoretical Computer Science, 637:1--29, July 2016.
doi: 10.1016/j.tcs.2016.04.020.
BibTex | DOI | Web page ]
[Sch16c]
S. Schmitz. Implicational Relevance Logic is 2-ExpTime-Complete. Journal of Symbolic Logic, 81(2):641--661, June 2016.
doi: 10.1017/jsl.2015.7.
BibTex | DOI | Web page | PDF ]
[Blo16]
M. Blondin. Algorithmique et complexité des systèmes à compteurs. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France and Université de Montréal, June 2016.
BibTex | Web page ]
[BCEZ16]
T. Brough, L. Ciobanu, M. Elder, and G. Zetzsche. Permutations of context-free, ET0L and indexed languages. Discrete Mathematics & Theoretical Computer Science, 17(3):167--178, May 2016.
BibTex | Web page | PDF ]
[HHK+16b]
M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, and É. Lozes. Two-Buffer Simulation Games. In Proceedings of the Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd International Workshop on Synthesis of Complex Parameters (Cassting/SYNCOP'16), volume 220 of Electronic Proceedings in Theoretical Computer Science, pages 213--227, Eindhoven, The Netherlands, April 2016.
doi: 10.4204/EPTCS.220.3.
BibTex | DOI | Web page | PDF ]
[CCH+16]
D. Chistikov, W. Czerwiński, P. Hofman, M. Pilipczuk, and M. Wehar. Shortest paths in one-counter systems. In Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16), volume 9634 of Lecture Notes in Computer Science, pages 462--478, Eindhoven, The Netherlands, April 2016. Springer.
doi: 10.1007/978-3-662-49630-5_27.
BibTex | DOI | Web page | PDF ]
[HLL+16]
P. Hofman, S. Lasota, R. Lazić, J. Leroux, S. Schmitz, and P. Totzke. Coverability Trees for Petri Nets with Unordered Data. In Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16), volume 9634 of Lecture Notes in Computer Science, pages 445--461, Eindhoven, The Netherlands, April 2016. Springer.
doi: 10.1007/978-3-662-49630-5_26.
BibTex | DOI | Web page ]
[BFHH16a]
M. Blondin, A. Finkel, C. Haase, and S. Haddad. Approaching the Coverability Problem Continuously. In Proceedings of the 22th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'16), volume 9636 of Lecture Notes in Computer Science, pages 480--496, Eindhoven, The Netherlands, April 2016. Springer.
doi: 10.1007/978-3-662-49674-9_28.
BibTex | DOI | Web page | PDF ]
[DD16a]
S. Demri and M. Deters. Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction. ACM Transactions on Computational Logic, 17(2):12:1--12:44, March 2016.
doi: 10.1145/2835490.
BibTex | DOI | Web page | PDF ]
[HK16]
C. Haase and S. Kiefer. The Complexity of the Kth Largest Subset Problem and Related Problems. Information Processing Letters, 116(2):111--115, February 2016.
doi: 10.1016/j.ipl.2015.09.015.
BibTex | DOI | Web page | PDF ]
[LS16b]
J. Leroux and S. Schmitz. Ideal Decompositions for Vector Addition Systems. In Proceedings of the 33rd Annual Symposium on Theoretical Aspects of Computer Science (STACS'16), volume 47 of Leibniz International Proceedings in Informatics, pages 1:1--1:13, Orléans, France, February 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.STACS.2016.1.
BibTex | DOI | Web page ]
[Sch16b]
S. Schmitz. Complexity Hierarchies Beyond Elementary. ACM Transactions on Computation Theory, 8(1:3), February 2016.
doi: 10.1145/2858784.
BibTex | DOI | Web page ]
[HH16]
C. Haase and P. Hofman. Tightening the Complexity of Equivalence Problems for Commutative Grammars. In Proceedings of the 33rd Annual Symposium on Theoretical Aspects of Computer Science (STACS'16), volume 47 of Leibniz International Proceedings in Informatics, pages 41:1--14, Orléans, France, February 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.STACS.2016.41.
BibTex | DOI | Web page | PDF ]
[KNS16]
P. Karandikar, M. Niewerth, and Ph. Schnoebelen. On the state complexity of closures and interiors of regular languages with subwords and superwords. Theoretical Computer Science, 610(A):91--107, January 2016.
doi: 10.1016/j.tcs.2015.09.028.
BibTex | DOI | Web page | PDF ]
[DD16b]
S. Demri and M. Deters. Temporal Logics on Strings with Prefix Relation. Journal of Logic and Computation, 26(3):989--1017, 2016.
doi: 10.1093/logcom/exv028.
BibTex | DOI | Web page | PDF ]
[BFHH16b]
M. Blondin, A. Finkel, C. Haase, and S. Haddad. QCover: an efficient coverability verifier for discrete and continuous Petri nets, 2016.
BibTex | Web page ]
[ADF+16]
P. A. Abdulla, S. Demri, A. Finkel, J. Leroux, and I. Potapov. Selected papers of Reachability Problems Workshop 2012 (Bordeaux) and 2013 (Uppsala). Fundamenta Informaticae, 143(3--4), 2016.
BibTex | Web page ]
[Sch16a]
S. Schmitz. Automata column: The complexity of reachability in vector addition systems. SIGLOG News, 3(1):3--21, January 2016.
doi: 10.1145/2893582.2893585.
BibTex | DOI | Web page ]
[HOW16]
C. Haase, J. Ouaknine, and J. Worrell. Relating Reachability Problems in Timed and Counter Automata. Fundamenta Informaticae, 143(3-4):317--338, January 2016.
doi: 10.3233/FI-2016-1316.
BibTex | DOI | Web page | PDF ]
[KS15a]
P. Karandikar and Ph. Schnoebelen. Decidability in the logic of subsequences and supersequences. In Proceedings of the 35th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'15), volume 45 of Leibniz International Proceedings in Informatics, pages 84--97, Bangalore, India, December 2015. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2015.84.
BibTex | DOI | Web page | PDF ]
[CHH15]
D. Chistikov, C. Haase, and S. Halfon. Context-Free Commutative Grammars with Integer Counters and Resets. Research Report 1511-04893, Computing Research Repository, November 2015. 31 pages.
BibTex | Web page | PDF ]
[Loz15]
É. Lozes. A Type-Directed Negation Elimination. In Proceedings of the 10th Workshop on Fixed Points in Computer Science (FICS'15), volume 191 of Electronic Proceedings in Theoretical Computer Science, pages 132--142, Berlin, Germany, September 2015.
doi: 10.4204/EPTCS.191.12.
BibTex | DOI | Web page | PDF ]
[LS15a]
R. Lazić and S. Schmitz. The Ideal View on Rackoff's Coverability Technique. In Proceedings of the 9th Workshop on Reachability Problems in Computational Models (RP'15), volume 9328 of Lecture Notes in Computer Science, pages 76--88, Warsaw, Poland, September 2015. Springer.
doi: 10.1007/978-3-319-24537-9_8.
BibTex | DOI | Web page | PDF ]
[LL15]
M. Lange and É. Lozes. Conjunctive Visibly-Pushdown Path Queries. In Proceedings of the 20th International Symposium on Fundamentals of Computation Theory (FCT'15), volume 9210 of Lecture Notes in Computer Science, pages 327--338, Gdańsk, Poland, August 2015. Springer.
doi: 10.1007/978-3-319-22177-9_25.
BibTex | DOI | Web page | PDF ]
[JLS15]
M. Jurdziński, R. Lazić, and S. Schmitz. Fixed-Dimensional Energy Games are in Pseudo Polynomial Time. In Proceedings of the 42nd International Colloquium on Automata, Languages and Programming (ICALP'15) -- Part II, volume 9135 of Lecture Notes in Computer Science, pages 260--272, Kyoto, Japan, July 2015. Springer.
doi: 10.1007/978-3-662-47666-6_21.
BibTex | DOI | Web page | PDF ]
[HK15]
C. Haase and S. Kiefer. The Odds of Staying on Budget. In Proceedings of the 42nd International Colloquium on Automata, Languages and Programming (ICALP'15) -- Part II, volume 9135 of Lecture Notes in Computer Science, pages 234--246, Kyoto, Japan, July 2015. Springer.
doi: 10.1007/978-3-662-47666-6_19.
BibTex | DOI | Web page | PDF ]
[LS15c]
J. Leroux and S. Schmitz. Demystifying Reachability in Vector Addition Systems. In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'15), pages 56--67, Kyoto, Japan, July 2015. IEEE Press.
doi: 10.1109/LICS.2015.1.
BibTex | DOI | Web page | PDF ]
[BFG+15]
M. Blondin, A. Finkel, S. Göller, C. Haase, and P. McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-Complete. In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'15), pages 32--43, Kyoto, Japan, July 2015. IEEE Press.
doi: 10.1109/LICS.2015.14.
BibTex | DOI | Web page | PDF ]
[LS15b]
R. Lazić and S. Schmitz. Non-Elementary Complexities for Branching VASS, MELL, and Extensions. ACM Transactions on Computational Logic, 16(3:20), July 2015.
doi: 10.1145/2733375.
BibTex | DOI | Web page | PDF ]
[DDS15]
S. Demri, A. K. Dhar, and A. Sangnier. Taming Past LTL and Flat Counter Systems. Information and Computation, 242:306--339, June 2015.
doi: 10.1016/j.ic.2015.03.007.
BibTex | DOI | Web page | PDF ]
[FL15]
A. Finkel and J. Leroux. Recent and simple algorithms for Petri nets. Software & System Modeling, 14(2):719--725, May 2015.
doi: 10.1007/s10270-014-0426-0.
BibTex | DOI | Web page | PDF ]
[KS15b]
P. Karandikar and Ph. Schnoebelen. Generalized Post Embedding Problems. Theory of Computing Systems, 56(4):697--716, May 2015.
doi: 10.1007/s00224-014-9561-9.
BibTex | DOI | Web page | PDF ]
[JKS15]
P. Jancar, P. Karandikar, and Ph. Schnoebelen. On Reachability for Unidirectional Channel Systems Extended with Regular Tests. Logical Methods in Computer Science, 11(2:2), April 2015.
doi: 10.2168/LMCS-11(2:2)2015.
BibTex | DOI | Web page | PDF ]
[KKS15]
P. Karandikar, M. Kufleitner, and Ph. Schnoebelen. On the index of Simon's congruence for piecewise testability. Information Processing Letters, 15(4):515--519, April 2015.
doi: 10.1016/j.ipl.2014.11.008.
BibTex | DOI | Web page | PDF ]
[LV15]
É. Lozes and J. Villard. Shared contract-obedient channels. Science of Computer Programming, 100:28--60, March 2015.
doi: 10.1016/j.scico.2014.09.008.
BibTex | DOI | Web page | PDF ]
[DD15b]
S. Demri and M. Deters. Two-variable separation logic and its inner circle. ACM Transactions on Computational Logic, 16(2:15), March 2015.
doi: 10.1145/2724711.
BibTex | DOI | Web page | PDF ]
[Kar15]
P. Karandikar. Subwords: automata, embedding problems, and verification. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France and Chennai Mathematical Institute, India, February 2015.
BibTex | Web page | PDF ]
[DD15a]
S. Demri and M. Deters. Separation Logics and Modalities: A Survey. Journal of Applied Non-Classical Logics, 25(1):50--99, 2015.
doi: 10.1080/11663081.2015.1018801.
BibTex | DOI | Web page | PDF ]
[LLV14]
M. Lange, É. Lozes, and M. Vargas Guzmán. Model-checking process equivalences. Theoretical Computer Science, 560(3):326--347, December 2014.
doi: 10.1016/j.tcs.2014.08.020.
BibTex | DOI | Web page | PDF ]
[HSS14]
C. Haase, S. Schmitz, and Ph. Schnoebelen. The Power of Priority Channel Systems. Logical Methods in Computer Science, 10(4:4), December 2014.
doi: 10.2168/LMCS-10(4:4)2014.
BibTex | DOI | Web page | PDF ]
[GPPS14]
C. Gardent, G. Perrier, Y. Parmentier, and S. Schmitz. Lexical Disambiguation in LTAG using Left Context. In Proceedings of the 5th Language & Technology Conference (LTC'11), volume 8387 of Lecture Notes in Artificial Intelligence, Poznań, Poland, November 2014. Springer.
BibTex | Web page ]
[KNS14]
P. Karandikar, M. Niewerth, and Ph. Schnoebelen. On the state complexity of closures and interiors of regular languages with subwords. Research Report 1406.0690, Computing Research Repository, November 2014. 24 pages.
BibTex | Web page | PDF ]
[Hal14]
S. Halfon. Non Primitive Recursive Complexity Classes. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2014. 21 pages.
BibTex | Web page | PDF ]
[Sch14a]
S. Schmitz. Complexity Bounds for Ordinal-Based Termination. In Proceedings of the 8th Workshop on Reachability Problems in Computational Models (RP'14), volume 8762 of Lecture Notes in Computer Science, pages 1--19, Oxford, UK, September 2014. Springer.
doi: 10.1007/978-3-319-11439-2_1.
BibTex | DOI | Web page | PDF ]
[LS14b]
J. Leroux and Ph. Schnoebelen. On Functions Weakly Computable by Petri Nets and Vector Addition Systems. In Proceedings of the 8th Workshop on Reachability Problems in Computational Models (RP'14), volume 8762 of Lecture Notes in Computer Science, pages 190--202, Oxford, UK, September 2014. Springer.
doi: 10.1007/978-3-319-11439-2_15.
BibTex | DOI | Web page | PDF ]
[HH14]
C. Haase and S. Halfon. Integer Vector Addition Systems with States. In Proceedings of the 8th Workshop on Reachability Problems in Computational Models (RP'14), volume 8762 of Lecture Notes in Computer Science, pages 112--124, Oxford, UK, September 2014. Springer.
doi: 10.1007/978-3-319-11439-2_9.
BibTex | DOI | Web page | PDF ]
[CS14]
J.-B. Courtois and S. Schmitz. Alternating Vector Addition Systems with States. In Proceedings of the 39th International Symposium on Mathematical Foundations of Computer Science (MFCS'14) -- Part I, volume 8634 of Lecture Notes in Computer Science, pages 220--231, Budapest, Hungary, August 2014. Springer.
doi: 10.1007/978-3-662-44522-8_19.
BibTex | DOI | Web page | PDF ]
[KS14]
P. Karandikar and Ph. Schnoebelen. On the state complexity of closures and interiors of regular languages with subwords. In Proceedings of the 16th Workshop on Descriptional Complexity of Formal Systems (DCFS'14), volume 8614 of Lecture Notes in Computer Science, pages 234--245, Turku, Finland, August 2014. Springer-Verlag.
doi: 10.1007/978-3-319-09704-6_21.
BibTex | DOI | Web page | PDF ]
[DD14a]
S. Demri and M. Deters. The effects of modalities in separation logics (extended abstract). In Proceedings of the 10th Conference on Advances in Modal Logics (AiML'14), pages 134--138, Groningen, The Netherlands, August 2014. College Publications.
BibTex | Web page | PDF ]
[CKM14]
M. Cadilhac, A. Krebs, and P. McKenzie. Extremely uniform branching programs. In Proceedings of the 6th Workshop on Non-Classical Models of Automata and Applications (NCMA'14), volume 304 of books@ocg.at, pages 73--83, Kassel, Germany, July 2014. Austrian Computer Society.
BibTex | Web page | PDF ]
[BFS14]
F. Bouchy, A. Finkel, and P. San Pietro. Dense-choice Counter Machines Revisited. Theoretical Computer Science, 542:17--31, July 2014.
doi: 10.1016/j.tcs.2014.04.029.
BibTex | DOI | Web page | PDF ]
[BFM14]
M. Blondin, A. Finkel, and P. McKenzie. Handling Infinitely Branching WSTS. In Proceedings of the 41st International Colloquium on Automata, Languages and Programming (ICALP'14) -- Part II, volume 8573 of Lecture Notes in Computer Science, pages 13--25, Copenhagen, Denmark, July 2014. Springer.
doi: 10.1007/978-3-662-43951-7_2.
BibTex | DOI | Web page | PDF ]
[DD14b]
S. Demri and M. Deters. Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction. In Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/ IEEE Symposium on Logic In Computer Science (CSL/LICS'14), Vienna, Austria, July 2014. ACM Press.
doi: 10.1145/2603088.2603142.
BibTex | DOI | Web page | PDF ]
[Haa14]
C. Haase. Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy. In Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/ IEEE Symposium on Logic In Computer Science (CSL/LICS'14), Vienna, Austria, July 2014. ACM Press.
doi: 10.1145/2603088.2603092.
BibTex | DOI | Web page | PDF ]
[Sch14b]
S. Schmitz. Implicational Relevance Logic is 2-ExpTime-Complete. In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda-Calculi and Applications (RTA/ TLCA'14), volume 8560 of Lecture Notes in Computer Science, pages 395--409, Vienna, Austria, July 2014. Springer.
doi: 10.1007/978-3-319-08918-8_27.
BibTex | DOI | Web page | PDF ]
[LS14a]
R. Lazić and S. Schmitz. Non-Elementary Complexities for Branching VASS, MELL, and Extensions. In Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/ IEEE Symposium on Logic In Computer Science (CSL/LICS'14), Vienna, Austria, July 2014. ACM Press.
doi: 10.1145/2603088.2603129.
BibTex | DOI | Web page | PDF ]
[FL14]
A. Finkel and J. Leroux. Neue, einfache Algorithmen für Petrinetze. Informatik Spektrum, 37(3):229--236, June 2014.
doi: 10.1007/s00287-013-0753-5.
BibTex | DOI | Web page | PDF ]
[DGLWM14]
S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Méry. Separation Logic with One Quantified Variable. In Proceedings of the 9th International Computer Science Symposium in Russia (CSR'14), volume 8476 of Lecture Notes in Computer Science, pages 125--138, Moscow, Russia, June 2014. Springer.
doi: 10.1007/978-3-319-06686-8_10.
BibTex | DOI | Web page | PDF ]
[AGH+14]
T. Antonopoulos, N. Gorogiannis, C. Haase, M. Kanovich, and J. Ouaknine. Foundations for Decision Problems in Separation Logic with General Inductive Predicates. In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14), volume 8412 of Lecture Notes in Computer Science, pages 411--425, Grenoble, France, April 2014. Springer.
doi: 10.1007/978-3-642-54830-7_27.
BibTex | DOI | Web page | PDF ]
[EM14]
Y. Elias and P. McKenzie. On Generalized Addition Chains. INTEGERS -- Electronic Journal of Combinatorial Number Theory, 14(A16), March 2014.
BibTex | Web page | PDF ]
[Fin14]
A. Finkel. REACHARD -- Compte-rendu intermédiaire. Deliverable D3 Reachard (ANR-11-BS02-001), February 2014. 18 pages.
BibTex ]
[BS13a]
N. Bertrand and Ph. Schnoebelen. Computable fixpoints in well-structured symbolic model checking. Formal Methods in System Design, 43(2):233--267, October 2013.
doi: 10.1007/s10703-012-0168-y.
BibTex | DOI | Web page | PDF ]
[BDG+13]
Th. Brihaye, L. Doyen, G. Geeraerts, J. Ouaknine, J.-F. Raskin, and J. Worrell. Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), volume 8172 of Lecture Notes in Computer Science, pages 55--70, Hanoi, Vietnam, October 2013. Springer.
doi: 10.1007/978-3-319-02444-8_6.
BibTex | DOI | Web page | PDF ]
[CDRR13]
K. Chatterjee, L. Doyen, M. Randour, and J.-F. Raskin. Looking at Mean-Payoff and Total-Payoff through Windows. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), volume 8172 of Lecture Notes in Computer Science, pages 118--132, Hanoi, Vietnam, October 2013. Springer.
doi: 10.1007/978-3-319-02444-8_10.
BibTex | DOI | Web page | PDF ]
[CDH13]
K. Chatterjee, L. Doyen, and Th. A. Henzinger. A survey of partial-observation stochastic parity games. Formal Methods in System Design, 43(2):268--284, October 2013.
doi: 10.1007/s10703-012-0164-2.
BibTex | DOI | Web page | PDF ]
[BCMV13]
R. Bonnet, R. Chadha, P. Madhusudan, and M. Viswanathan. Reachability under contextual locking. Logical Methods in Computer Science, 9(3:21), September 2013.
doi: 10.2168/LMCS-9(3:21)2013.
BibTex | DOI | Web page | PDF ]
[Bro13]
R. Brochenin. Separation Logic: Expressiveness, Complexity, Temporal Extension. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2013.
BibTex | Web page | PDF ]
[Rei13]
J. Reichert. On The Complexity of Counter Reachability Games. In Proceedings of the 7th Workshop on Reachability Problems in Computational Models (RP'13), volume 8169 of Lecture Notes in Computer Science, pages 196--208, Uppsala, Sweden, September 2013. Springer.
doi: 10.1007/978-3-642-41036-9_18.
BibTex | DOI | Web page | PDF ]
[BDD13]
C. Barrett, S. Demri, and M. Deters. Witness runs for counter machines. In Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS'13), volume 8152 of Lecture Notes in Artificial Intelligence, pages 120--150, Nancy, France, September 2013. Springer.
doi: 10.1007/978-3-642-40885-4_9.
BibTex | DOI | Web page | PDF ]
[SS13]
S. Schmitz and Ph. Schnoebelen. The Power of Well-Structured Systems. In Proceedings of the 24th International Conference on Concurrency Theory (CONCUR'13), volume 8052 of Lecture Notes in Computer Science, pages 5--24, Buenos Aires, Argentina, August 2013. Springer.
doi: 10.1007/978-3-642-40184-8_2.
BibTex | DOI | Web page | PDF ]
[HSS13]
C. Haase, S. Schmitz, and Ph. Schnoebelen. The Power of Priority Channel Systems. In Proceedings of the 24th International Conference on Concurrency Theory (CONCUR'13), volume 8052 of Lecture Notes in Computer Science, pages 319--333, Buenos Aires, Argentina, August 2013. Springer.
doi: 10.1007/978-3-642-40184-8_23.
BibTex | DOI | Web page | PDF ]
[FGH13]
A. Finkel, S. Göller, and C. Haase. Reachability in Register Machines with Polynomial Updates. In Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13), volume 8087 of Lecture Notes in Computer Science, pages 409--420, Klosterneuburg, Austria, August 2013. Springer.
doi: 10.1007/978-3-642-40313-2_37.
BibTex | DOI | Web page | PS | PDF ]
[Dem13]
S. Demri. On selective unboundedness of VASS. Journal of Computer and System Sciences, 79(5):689--713, August 2013.
doi: 10.1016/j.jcss.2013.01.014.
BibTex | DOI | Web page | PDF ]
[DDS13]
S. Demri, A. K. Dhar, and A. Sangnier. On the Complexity of Verifying Regular Properties on Flat Counter Systems. In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP'13) -- Part II, volume 7966 of Lecture Notes in Computer Science, pages 162--173, Riga, Latvia, July 2013. Springer.
doi: 10.1007/978-3-642-39212-2_17.
BibTex | DOI | Web page | PDF ]
[McK13]
P. McKenzie. Can chimps go it alone? In Proceedings of the 15th Workshop on Descriptional Complexity of Formal Systems (DCFS'13), volume 8031 of Lecture Notes in Computer Science, page 17, London, Ontario, Canada, July 2013. Springer-Verlag.
doi: 10.1007/978-3-642-39310-5_3.
BibTex | DOI | Web page | PDF ]
[HIOP13]
C. Haase, S. Ishtiaq, J. Ouaknine, and M. Parkinson. SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13), volume 8044 of Lecture Notes in Computer Science, pages 790--795, Saint Petersburg, Russia, July 2013. Springer.
doi: 10.1007/978-3-642-39799-8_55.
BibTex | DOI | Web page | PDF ]
[BD13]
K. Bansal and S. Demri. Model-checking bounded multi-pushdown systems. In Proceedings of the 8th International Computer Science Symposium in Russia (CSR'13), volume 7913 of Lecture Notes in Computer Science, pages 405--417, Ekaterinburg, Russia, June 2013. Springer.
doi: 10.1007/978-3-642-38536-0_35.
BibTex | DOI | Web page | PDF ]
[GHPR13]
G. Geeraerts, A. Heußner, M. Praveen, and J.-F. Raskin. ω-Petri nets. In Proceedings of the 34th International Conference on Applications and Theory of Petri Nets (PETRI NETS'13), volume 7927 of Lecture Notes in Computer Science, pages 49--69, Milano, Italy, June 2013. Springer.
doi: 10.1007/978-3-642-38697-8_4.
BibTex | DOI | Web page | PDF ]
[DFP13]
S. Demri, D. Figueira, and M. Praveen. Reasoning about Data Repetitions with Counter Systems. In Proceedings of the 28th Annual IEEE Symposium on Logic in Computer Science (LICS'13), pages 33--42, New-Orleans, Louisiana, USA, June 2013. IEEE Computer Society Press.
doi: 10.1109/LICS.2013.8.
BibTex | DOI | Web page | PDF ]
[BS13c]
A. Boral and S. Schmitz. Model Checking Parse Trees. In Proceedings of the 28th Annual IEEE Symposium on Logic in Computer Science (LICS'13), pages 153--162, New-Orleans, Louisiana, USA, June 2013. IEEE Computer Society Press.
doi: 10.1109/LICS.2013.21.
BibTex | DOI | Web page | PDF ]
[AR13]
A. Arul and J. Reichert. The Complexity of Robot Games on the Integer Line. In Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages (QAPl'13), volume 117 of Electronic Proceedings in Theoretical Computer Science, pages 132--148, Rome, Italy, June 2013.
doi: 10.4204/EPTCS.117.9.
BibTex | DOI | Web page | PDF ]
[BS13b]
N. Bertrand and Ph. Schnoebelen. Solving stochastic Büchi games on infinite arenas with a finite attractor. In Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages (QAPl'13), volume 117 of Electronic Proceedings in Theoretical Computer Science, pages 116--131, Rome, Italy, June 2013.
doi: 10.4204/EPTCS.117.8.
BibTex | DOI | Web page | PDF ]
[BFHR13]
R. Bonnet, A. Finkel, S. Haddad, and F. Rosa-Velardo. Ordinal Theory for Expressiveness of Well-Structured Transition Systems. Information and Computation, 224:1--22, March 2013.
doi: 10.1016/j.ic.2012.11.003.
BibTex | DOI | Web page | PDF ]
[BC13]
R. Bonnet and R. Chadha. Bounded Context-Switching and Reentrant Locking. In Proceedings of the 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'13), volume 7794 of Lecture Notes in Computer Science, pages 65--80, Rome, Italy, March 2013. Springer.
doi: 10.1007/978-3-642-37075-5_5.
BibTex | DOI ]
[BNS13]
E. Bertsch, M.-J. Nederhof, and S. Schmitz. On LR Parsing with Selective Delays. In Proceedings of the 22nd International Conference on Compiler Construction (CC'13), volume 7791 of Lecture Notes in Computer Science, pages 244--263, Rome, Italy, March 2013. Springer.
doi: 10.1007/978-3-642-37051-9_13.
BibTex | DOI | Web page | PDF ]
[KS13]
P. Karandikar and S. Schmitz. The Parametric Ordinal-Recursive Complexity of Post Embedding Problems. In Proceedings of the 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'13), volume 7794 of Lecture Notes in Computer Science, pages 273--288, Rome, Italy, March 2013. Springer.
doi: 10.1007/978-3-642-37075-5_18.
BibTex | DOI | Web page | PDF ]
[Fin13]
A. Finkel. REACHARD -- Compte-rendu intermédiaire. Deliverable D2 Reachard (ANR-11-BS02-001), March 2013. 9 pages.
BibTex ]
[Bon13]
R. Bonnet. Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2013.
BibTex | Web page | PDF ]
[DR13]
L. Doyen and A. Rabinovich. Robot games. Research Report LSV-13-02, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2013. 2 pages.
BibTex | Web page | PDF ]
[CFM12b]
M. Cadilhac, A. Finkel, and P. McKenzie. Bounded Parikh automata. International Journal of Foundations of Computer Science, 23(8):1691--1710, December 2012.
doi: 10.1142/S0129054112400709.
BibTex | DOI | Web page | PDF ]
[BFP12]
R. Bonnet, A. Finkel, and M. Praveen. Extending the Rackoff technique to affine nets. In Proceedings of the 32nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), volume 18 of Leibniz International Proceedings in Informatics, Hyderabad, India, December 2012. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2012.301.
BibTex | DOI | Web page | PDF ]
[CD12b]
K. Chatterjee and L. Doyen. Energy parity games. Theoretical Computer Science, 458:49--60, November 2012.
doi: 10.1016/j.tcs.2012.07.038.
BibTex | DOI | Web page | PDF ]
[DDG12]
S. Demri, D. D'Souza, and R. Gascon. Temporal Logics of Repeating Values. Journal of Logic and Computation, 22(5):1059--1096, October 2012.
doi: 10.1093/logcom/exr013.
BibTex | DOI | Web page | PDF ]
[CFM12a]
M. Cadilhac, A. Finkel, and P. McKenzie. Affine Parikh automata. RAIRO Informatique Théorique et Applications, 46(4):511--545, October 2012.
doi: 10.1051/ita/2012013.
BibTex | DOI | Web page | PDF ]
[DDMM12]
Ph. Darondeau, S. Demri, R. Meyer, and Ch. Morvan. Petri Net Reachability Graphs: Decidability Status of FO Properties. Logical Methods in Computer Science, 8(4:9), October 2012.
doi: 10.2168/LMCS-8(4:9)2012.
BibTex | DOI | Web page | PDF ]
[FG12a]
A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. Logical Methods in Computer Science, 8(3:28), September 2012.
doi: 10.2168/LMCS-8(3:28)2012.
BibTex | DOI | Web page | PDF ]
[FLP12]
A. Finkel, J. Leroux, and I. Potapov, editors. Proceedings of the 6th International Wokshop on Reachability Problems (RP'12), volume 7550 of Lecture Notes in Computer Science, Bordeaux, France, September 2012. Springer.
doi: 10.1007/978-3-642-33512-9.
BibTex | DOI | Web page ]
[JKS12]
P. Jančar, P. Karandikar, and Ph. Schnoebelen. Unidirectional channel systems can be tested. In Proceedings of the 7th IFIP International Conference on Theoretical Computer Science (IFIP TCS'12), volume 7604 of Lecture Notes in Computer Science, pages 149--163, Amsterdam, The Netherlands, September 2012. Springer.
doi: 10.1007/978-3-642-33475-7_11.
BibTex | DOI | Web page | PDF ]
[CFM12c]
M. Cadilhac, A. Finkel, and P. McKenzie. Unambiguous Constrained Automata. In Proceedings of the 16th International Conference on Developments in Language Theory (DLT'12), volume 7410 of Lecture Notes in Computer Science, pages 239--250, Taipei, Taiwan, August 2012. Springer.
doi: 10.1007/978-3-642-31653-1_22.
BibTex | DOI | Web page | PDF ]
[CD12a]
F. Carreiro and S. Demri. Beyond Regularity for Presburger Modal Logics. In Selected Papers from the 9th Workshop on Advances in Modal Logics (AiML'12), pages 161--182, Copenhagen, Denmark, August 2012. College Publications.
BibTex | Web page | PDF ]
[DG12]
S. Demri and P. Gastin. Specification and Verification using Temporal Logics. In Modern applications of automata theory, volume 2 of IISc Research Monographs, chapter 15, pages 457--494. World Scientific, July 2012.
BibTex | Web page | PDF ]
[Loz12]
É. Lozes. Separation Logic: Expressiveness and Copyless Message-Passing. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, July 2012.
BibTex | Web page | PDF ]
[BMO+12]
P. Bouyer, N. Markey, J. Ouaknine, Ph. Schnoebelen, and J. Worrell. On Termination and Invariance for Faulty Channel Systems. Formal Aspects of Computing, 24(4-6):595--607, July 2012.
doi: 10.1007/s00165-012-0234-7.
BibTex | DOI | Web page | PDF ]
[KS12]
P. Karandikar and Ph. Schnoebelen. Cutting Through Regular Post Embedding Problems. In Proceedings of the 7th International Computer Science Symposium in Russia (CSR'12), volume 7353 of Lecture Notes in Computer Science, pages 229--240, Nizhni Novgorod, Russia, July 2012. Springer.
doi: 10.1007/978-3-642-30642-6_22.
BibTex | DOI | Web page | PDF ]
[CD12c]
K. Chatterjee and L. Doyen. Partial-Observation Stochastic Games: How to Win when Belief Fails. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS'12), pages 175--184, Dubrovnik, Croatia, June 2012. IEEE Computer Society Press.
doi: 10.1109/LICS.2012.28.
BibTex | DOI | Web page | PDF ]
[FG12b]
A. Finkel and J. Goubault-Larrecq. The Theory of WSTS: The Case of Complete WSTS. In Proceedings of the 33rd International Conference on Applications and Theory of Petri Nets (PETRI NETS'12), volume 7347 of Lecture Notes in Computer Science, pages 3--31, Hamburg, Germany, June 2012. Springer.
doi: 10.1007/978-3-642-31131-4_2.
BibTex | DOI | Web page | PDF ]
[HSS12]
S. Haddad, S. Schmitz, and Ph. Schnoebelen. The Ordinal-Recursive Complexity of Timed-Arc Petri Nets, Data Nets, and Other Enriched Nets. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS'12), pages 355--364, Dubrovnik, Croatia, June 2012. IEEE Computer Society Press.
doi: 10.1109/LICS.2012.46.
BibTex | DOI | Web page | PDF ]
[DDS12]
S. Demri, A. K. Dhar, and A. Sangnier. Taming Past LTL and Flat Counter Systems. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), volume 7364 of Lecture Notes in Artificial Intelligence, pages 179--193, Manchester, UK, June 2012. Springer-Verlag.
doi: 10.1007/978-3-642-31365-3_16.
BibTex | DOI | Web page | PDF ]
[IHL+12]
R. Iosif, P. Habermehl, S. Labbe, É. Lozes, and B. Yakobowski. Concurrent Programs with Simple Data Structures ash Sequential Programs with Composite Data Structures. Deliverable VERIDYC D 2 (ANR-09-SEGI-016), March 2012.
BibTex | Web page | PDF ]
[LL12]
M. Lange and É. Lozes. Model-Checking the Higher-Dimensional Modal μ-Calculus. In Proceedings of the 8th Workshop on Fixed Points in Computer Science (FICS'12), volume 77 of Electronic Proceedings in Theoretical Computer Science, pages 39--46, Tallinn, Estonia, March 2012.
doi: 10.4204/EPTCS.77.6.
BibTex | DOI | Web page | PDF ]
[Doy12]
L. Doyen. Games and Automata: From Boolean to Quantitative Verification. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, March 2012.
BibTex | Web page | PDF ]
[DJLL12]
S. Demri, M. Jurdziński, O. Lachish, and R. Lazić. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 79(1):23--38, February 2012.
doi: 10.1016/j.jcss.2012.04.002.
BibTex | DOI | Web page | PDF ]
[BDL12]
R. Brochenin, S. Demri, and É. Lozes. On the Almighty Wand. Information and Computation, 211:106--137, February 2012.
doi: 10.1016/j.ic.2011.12.003.
BibTex | DOI | Web page | PDF ]
[JLTV12]
F. Jacquemard, É. Lozes, R. Treinen, and J. Villard. Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus. In Revised Selected Papaers of the Workshop on Theory of Security and Applications (TOSCA'11), volume 6993 of Lecture Notes in Computer Science, pages 166--185, Saarbrücken, Germany, January 2012. Springer.
doi: 10.1007/978-3-642-27375-9_10.
BibTex | DOI | Web page | PDF ]
[LV12]
É. Lozes and J. Villard. Reliable Contracts for Unreliable Half-Duplex Communications. In Revised Selected Papers of the 8th International Workshop on Web Services and Formal Methods (WS-FM'11), volume 7176 of Lecture Notes in Computer Science, pages 2--16, Clermont-Ferrand, France, 2012. Springer.
doi: 10.1007/978-3-642-29834-9_2.
BibTex | DOI | Web page | PDF ]
[BFLZ12]
R. Bonnet, A. Finkel, J. Leroux, and M. Zeitoun. Model Checking Vector Addition Systems with one zero-test. Logical Methods in Computer Science, 8(2:11), 2012.
doi: 10.2168/LMCS-8(2:11)2012.
BibTex | DOI | Web page | PDF ]
[LV11]
É. Lozes and J. Villard. Sharing Contract-Obedient Endpoints. Research Report LSV-11-23, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2011. 42 pages.
BibTex | Web page | PDF ]
[CD11b]
K. Chatterjee and L. Doyen. Games and Markov Decision Processes with Mean-payoff Parity and Energy Parity Objectives. In Proceedings of the 7th Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'11), volume 7119 of Lecture Notes in Computer Science, Lednice, Czech Republic, October 2011. Springer.
BibTex | Web page | PDF ]
[BBD+11]
Th. Brihaye, V. Bruyère, L. Doyen, M. Ducobu, and J.-F. Raskin. Antichain-based QBF Solving. In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), volume 6996 of Lecture Notes in Computer Science, pages 183--197, Taipei, Taiwan, October 2011. Springer.
doi: 10.1007/978-3-642-24372-1_14.
BibTex | DOI | Web page | PDF ]
[Cha11]
P. Chambart. Du Problème de sous-mot de Post et de la complexité des canaux non fiables. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2011.
BibTex | Web page | PDF ]
[CFM11a]
M. Cadilhac, A. Finkel, and P. McKenzie. Bounded Parikh Automata. In Proceedings of the 8th International Conference WORDS (WORDS'11), volume 63 of Electronic Proceedings in Theoretical Computer Science, pages 93--102, Prague, Czech Republic, September 2011.
doi: 10.4204/EPTCS.63.13.
BibTex | DOI | Web page | PDF ]
[Bon11a]
R. Bonnet. Decidability of LTL Model Checking for Vector Addition Systems with one Zero-test. In Proceedings of the 5th Workshop on Reachability Problems in Computational Models (RP'11), volume 6945 of Lecture Notes in Computer Science, pages 85--95, Genova, Italy, September 2011. Springer.
doi: 10.1007/978-3-642-24288-5_9.
BibTex | DOI | Web page | PDF ]
[CDS11]
K. Chatterjee, L. Doyen, and R. Singh. On Memoryless Quantitative Objectives. In Proceedings of the 18th International Symposium on Fundamentals of Computation Theory (FCT'11), volume 6914 of Lecture Notes in Computer Science, pages 148--159, Oslo, Norway, August 2011. Springer.
doi: 10.1007/978-3-642-22953-4_13.
BibTex | DOI | Web page | PDF ]
[CD11a]
K. Chatterjee and L. Doyen. Energy and Mean-Payoff Parity Markov Decision Processes. In Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS'11), volume 6907 of Lecture Notes in Computer Science, pages 206--218, Warsaw, Poland, August 2011. Springer.
doi: 10.1007/978-3-642-22993-0_21.
BibTex | DOI | Web page | PDF ]
[DMS11a]
L. Doyen, Th. Massart, and M. Shirmohammadi. Infinite Synchronizing Words for Probabilistic Automata. In Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS'11), volume 6907 of Lecture Notes in Computer Science, pages 278--289, Warsaw, Poland, August 2011. Springer.
doi: 10.1007/978-3-642-22993-0_27.
BibTex | DOI | Web page | PDF ]
[BS11]
M. Blockelet and S. Schmitz. Model-Checking Coverability Graphs of Vector Addition Systems. In Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS'11), volume 6907 of Lecture Notes in Computer Science, pages 108--119, Warsaw, Poland, August 2011. Springer.
doi: 10.1007/978-3-642-22993-0_13.
BibTex | DOI | Web page | PDF ]
[Bon11b]
R. Bonnet. The reachability problem for Vector Addition Systems with one zero-test. In Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS'11), volume 6907 of Lecture Notes in Computer Science, pages 145--157, Warsaw, Poland, August 2011. Springer.
doi: 10.1007/978-3-642-22993-0_16.
BibTex | DOI | Web page | PDF ]
[CFM11b]
M. Cadilhac, A. Finkel, and P. McKenzie. On the Expressiveness of Parikh Automata and Related Models. In Proceedings of the 3rd Workshop on Non-Classical Models of Automata and Applications (NCMA'11), volume 282 of books@ocg.at, pages 103--119, Milano, Italy, July 2011. Austrian Computer Society.
BibTex | DOI | Web page | PDF ]
[Sch11]
S. Schmitz. A Note on Sequential Rule-Based POS Tagging. In Proceedings of the 9th International Workshop on Finite-State Methods and Natural Language Processing (FSMNLP'11), pages 83--87, Blois, France, July 2011. ACL Press.
BibTex | Web page | PDF ]
[BDG+11]
Th. Brihaye, L. Doyen, G. Geeraerts, J. Ouaknine, J.-F. Raskin, and J. Worrell. On Reachability for Hybrid Automata over Bounded Time. In Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP'11) -- Part II, volume 6756 of Lecture Notes in Computer Science, pages 416--427, Zürich, Switzerland, July 2011. Springer.
doi: 10.1007/978-3-642-22012-8_33.
BibTex | DOI | Web page | PDF ]
[SS11]
S. Schmitz and Ph. Schnoebelen. Multiply-Recursive Upper Bounds with Higman's Lemma. In Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP'11) -- Part II, volume 6756 of Lecture Notes in Computer Science, pages 441--452, Zürich, Switzerland, July 2011. Springer.
doi: 10.1007/978-3-642-22012-8_35.
BibTex | DOI | Web page | PDF ]
[CFS11]
P. Chambart, A. Finkel, and S. Schmitz. Forward Analysis and Model Checking for Trace Bounded WSTS. In Proceedings of the 32nd International Conference on Applications and Theory of Petri Nets (PETRI NETS'11), volume 6709 of Lecture Notes in Computer Science, Newcastle upon Tyne, UK, June 2011. Springer.
doi: 10.1007/978-3-642-21834-7_4.
BibTex | DOI | Web page ]
[FFSS11]
D. Figueira, S. Figueira, S. Schmitz, and Ph. Schnoebelen. Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS'11), pages 269--278, Toronto, Canada, June 2011. IEEE Computer Society Press.
doi: 10.1109/LICS.2011.39.
BibTex | DOI | Web page | PDF ]
[BCD+11]
L. Brim, J. Chaloupka, L. Doyen, R. Gentilini, and J.-F. Raskin. Faster algorithms for mean-payoff games. Formal Methods in System Design, 38(2):97--118, April 2011.
doi: 10.1007/s10703-010-0105-x.
BibTex | DOI | Web page | PDF ]
[DMS11b]
L. Doyen, Th. Massart, and M. Shirmohammadi. Synchronizing Objectives for Markov Decision Processes. In Proceedings of the International Workshop on Interactions, Games and Protocols (iWIGP'11), volume 50 of Electronic Proceedings in Theoretical Computer Science, pages 61--75, Saarbrücken, Germany, March 2011.
BibTex | Web page | PDF ]
[BFHR11]
R. Bonnet, A. Finkel, S. Haddad, and F. Rosa-Velardo. Ordinal Theory for Expressiveness of Well Structured Transition Systems. In Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'11), volume 6604 of Lecture Notes in Computer Science, pages 153--167, Saarbrücken, Germany, March-April 2011. Springer.
doi: 10.1007/978-3-642-19805-2_11.
BibTex | DOI | Web page | PDF ]
[Vil11]
J. Villard. Heaps and Hops. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2011.
BibTex | Web page | PDF ]
[DR11]
L. Doyen and J.-F. Raskin. Games with Imperfect Information: Theory and Algorithms. In Lectures in Game Theory for Computer Scientists. Cambridge University Press, January 2011.
BibTex | Web page | PS | PDF ]
[DP11]
S. Demri and D. Poitrenaud. Verification of Infinite-State Systems. In Models and Analysis in Distributed Systems, chapter 8, pages 221--269. John Wiley & Sons, Ltd., 2011.
BibTex | Web page | PDF ]
[BFHR10]
R. Bonnet, A. Finkel, S. Haddad, and F. Rosa-Velardo. Comparing Petri Data Nets and Timed Petri Nets. Research Report LSV-10-23, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2010. 16 pages.
BibTex | Web page | PDF ]
[CDHR10]
K. Chatterjee, L. Doyen, Th. A. Henzinger, and J.-F. Raskin. Generalized Mean-payoff and Energy Games. In Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'10), volume 8 of Leibniz International Proceedings in Informatics, pages 505--516, Chennai, India, December 2010. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2010.505.
BibTex | DOI | Web page | PDF ]
[BFLZ10]
R. Bonnet, A. Finkel, J. Leroux, and M. Zeitoun. Place-Boundedness for Vector Addition Systems with one zero-test. In Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'10), volume 8 of Leibniz International Proceedings in Informatics, pages 192--203, Chennai, India, December 2010. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2010.192.
BibTex | DOI | Web page | PDF ]
[CD10a]
K. Chatterjee and L. Doyen. The Complexity of Partial-Observation Parity Games. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10), volume 6397 of Lecture Notes in Artificial Intelligence, pages 1--14, Yogyakarta, Indonesia, October 2010. Springer.
doi: 10.1007/978-3-642-16242-8_1.
BibTex | DOI | Web page | PS | PDF ]
[BCD+10]
D. Berwanger, K. Chatterjee, L. Doyen, M. De Wulf, and Th. A. Henzinger. Strategy Construction for Parity Games with Imperfect Information. Information and Computation, 208(10):1206--1220, October 2010.
doi: 10.1016/j.ic.2009.09.006.
BibTex | DOI | Web page | PS | PDF ]
[CDH10a]
K. Chatterjee, L. Doyen, and Th. A. Henzinger. Expressiveness and Closure Properties for Quantitative Languages. Logical Methods in Computer Science, 6(3:10), September 2010.
doi: 10.2168/LMCS-6(3:10)2010.
BibTex | DOI | Web page | PS | PDF ]
[LV10]
É. Lozes and J. Villard. A spatial equational logic for the applied π-calculus. Distributed Computing, 23(1):61--83, September 2010.
doi: 10.1007/s00446-010-0112-6.
BibTex | DOI | Web page | PDF ]
[Sch10c]
Ph. Schnoebelen. Lossy Counter Machines Decidability Cheat Sheet. In Proceedings of the 4th Workshop on Reachability Problems in Computational Models (RP'10), volume 6227 of Lecture Notes in Computer Science, pages 51--75, Brno, Czech Republic, August 2010. Springer.
doi: 10.1007/978-3-642-15349-5_4.
BibTex | DOI | Web page | PDF ]
[DDG+10]
A. Degorre, L. Doyen, R. Gentilini, J.-F. Raskin, and S. Toruńczyk. Energy and Mean-Payoff Games with Imperfect Information. In Proceedings of the 19th Annual EACSL Conference on Computer Science Logic (CSL'10), volume 6247 of Lecture Notes in Computer Science, pages 260--274, Brno, Czech Republic, August 2010. Springer.
doi: 10.1007/978-3-642-15205-4_22.
BibTex | DOI | Web page | PDF ]
[Sch10d]
Ph. Schnoebelen. Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS'10), volume 6281 of Lecture Notes in Computer Science, pages 616--628, Brno, Czech Republic, August 2010. Springer.
doi: 10.1007/978-3-642-15155-2_54.
BibTex | DOI | Web page | PDF ]
[CDGH10]
K. Chatterjee, L. Doyen, H. Gimbert, and Th. A. Henzinger. Randomness for Free. In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS'10), volume 6281 of Lecture Notes in Computer Science, pages 246--257, Brno, Czech Republic, August 2010. Springer.
doi: 10.1007/978-3-642-15155-2_23.
BibTex | DOI | Web page | PDF ]
[CDH10b]
K. Chatterjee, L. Doyen, and Th. A. Henzinger. Qualitative Analysis of Partially-observable Markov Decision Processes. In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS'10), volume 6281 of Lecture Notes in Computer Science, pages 258--269, Brno, Czech Republic, August 2010. Springer.
doi: 10.1007/978-3-642-15155-2_24.
BibTex | DOI | Web page | PDF ]
[CDE+10]
K. Chatterjee, L. Doyen, H. Edelsbrunner, Th. A. Henzinger, and P. Rannou. Mean-Payoff Automaton Expressions. In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR'10), volume 6269 of Lecture Notes in Computer Science, pages 269--283, Paris, France, August-September 2010. Springer.
doi: 10.1007/978-3-642-15375-4_19.
BibTex | DOI | Web page | PDF ]
[CS10a]
P. Chambart and Ph. Schnoebelen. Computing blocker sets for the Regular Post Embedding Problem. In Proceedings of the 14th International Conference on Developments in Language Theory (DLT'10), volume 6224 of Lecture Notes in Computer Science, pages 136--147, London, Ontario, Canada, August 2010. Springer.
doi: 10.1007/978-3-642-14455-4_14.
BibTex | DOI | Web page | PDF ]
[HNS10]
P.-C. Héam, C. Nicaud, and S. Schmitz. Parametric Random Generation of Deterministic Tree Automata. Theoretical Computer Science, 411(38-39):3469--3480, August 2010.
doi: 10.1016/j.tcs.2010.05.036.
BibTex | DOI | Web page | PDF ]
[Sch10b]
S. Schmitz. On the Computational Complexity of Dominance Links in Grammatical Formalisms. In Proceedings of the 48th Annual Meeting of the Association for Computational Linguistics (ACL'10), pages 514--524, Uppsala, Sweden, July 2010. Association for Computational Linguistics.
BibTex | Web page | PDF ]
[CS10b]
P. Chambart and Ph. Schnoebelen. Pumping and Counting on the Regular Post Embedding Problem. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP'10) -- Part II, volume 6199 of Lecture Notes in Computer Science, pages 64--75, Bordeaux, France, July 2010. Springer.
doi: 10.1007/978-3-642-14162-1_6.
BibTex | DOI | Web page | PDF ]
[CD10b]
K. Chatterjee and L. Doyen. Energy Parity Games. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP'10) -- Part II, volume 6199 of Lecture Notes in Computer Science, pages 599--610, Bordeaux, France, July 2010. Springer.
doi: 10.1007/978-3-642-14162-1_50.
BibTex | DOI | Web page | PDF ]
[DHLN10]
L. Doyen, Th. A. Henzinger, A. Legay, and D. Nickovic. Robustness of Sequential Circuits. In Proceedings of the 10th International Conference on Application of Concurrency to System Design (ACSD'10), pages 77--84, Braga, Portugal, June 2010. IEEE Computer Society Press.
doi: 10.1109/ACSD.2010.26.
BibTex | DOI | Web page | PDF ]
[DLS10]
S. Demri, R. Lazić, and A. Sangnier. Model checking memoryful linear-time logics over one-counter automata. Theoretical Computer Science, 411(22-24):2298--2316, May 2010.
doi: 10.1016/j.tcs.2010.02.021.
BibTex | DOI | Web page | PDF ]
[VLC10]
J. Villard, É. Lozes, and C. Calcagno. Tracking Heaps that Hop with Heap-Hop. In Proceedings of the 16th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'10), volume 6015 of Lecture Notes in Computer Science, pages 275--279, Paphos, Cyprus, March 2010. Springer.
doi: 10.1007/978-3-642-12002-2_23.
BibTex | DOI | Web page | PDF ]
[DS10]
S. Demri and A. Sangnier. When Model-Checking Freeze LTL over Counter Machines Becomes Decidable. In Proceedings of the 13th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'10), volume 6014 of Lecture Notes in Computer Science, pages 176--190, Paphos, Cyprus, March 2010. Springer.
doi: 10.1007/978-3-642-12032-9_13.
BibTex | DOI | Web page | PDF ]
[CS10c]
P. Chambart and Ph. Schnoebelen. Toward a compositional theory of leftist grammars and transformations. In Proceedings of the 13th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'10), volume 6014 of Lecture Notes in Computer Science, pages 237--251, Paphos, Cyprus, March 2010. Springer.
doi: 10.1007/978-3-642-12032-9_17.
BibTex | DOI | Web page | PDF ]
[Bon10]
R. Bonnet. Well-structured Petri-nets extensions with data. Rapport de Master, Master Computer Science, EPFL, Lausanne, Switzerland, March 2010.
BibTex | Web page | PDF ]
[DR10]
L. Doyen and J.-F. Raskin. Antichains Algorithms for Finite Automata. In Proceedings of the 16th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'10), volume 6015 of Lecture Notes in Computer Science, pages 2--22, Paphos, Cyprus, March 2010. Springer.
doi: 10.1007/978-3-642-12002-2_2.
BibTex | DOI | Web page | PS | PDF ]
[AHL+10]
A. Antonik, M. Huth, K. G. Larsen, U. Nyman, and A. Wąsowski. Modal and mixed specifications: key decision problems and their complexities. Mathematical Structures in Computer Science, 10(1):75--103, February 2010.
doi: 10.1017/S0960129509990260.
BibTex | DOI | Web page | PDF ]
[Sch10a]
S. Schmitz. An Experimental Ambiguity Detection Tool. Science of Computer Programming, 75(1-2):71--84, January 2010.
doi: 10.1016/j.scico.2009.07.002.
BibTex | DOI | Web page | PDF ]
[CLPV10]
R. Chadha, A. Legay, P. Prabhakar, and M. Viswanathan. Complexity bounds for the verification of real-time software. In Proceedings of the 11th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'10), volume 5944 of Lecture Notes in Computer Science, pages 95--111, Madrid, Spain, January 2010. Springer.
doi: 10.1007/978-3-642-11319-2_10.
BibTex | DOI | Web page | PDF ]
[FS10]
A. Finkel and A. Sangnier. Mixing coverability and reachability to analyze VASS with one zero-test. In Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'10), volume 5901 of Lecture Notes in Computer Science, pages 394--406, Špindlerův Mlýn, Czech Republic, January 2010. Springer.
doi: 10.1007/978-3-642-11266-9_33.
BibTex | DOI | Web page | PS | PDF ]
[CDH10c]
K. Chatterjee, L. Doyen, and Th. A. Henzinger. Quantitative Languages. ACM Transactions on Computational Logic, 11(4), 2010.
BibTex | Web page | PS | PDF ]
[DFGvD10]
S. Demri, A. Finkel, V. Goranko, and G. van Drimmelen. Model-checking CTL^* over Flat Presburger Counter Systems. Journal of Applied Non-Classical Logics, 20(4):313--344, 2010.
doi: 10.3166/jancl.20.313-344.
BibTex | DOI | Web page | PDF ]
[DJLL09]
S. Demri, M. Jurdziński, O. Lachish, and R. Lazić. The covering and boundedness problems for branching vector addition systems. In Proceedings of the 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09), volume 4 of Leibniz International Proceedings in Informatics, pages 181--192, Kanpur, India, December 2009. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2009.2317.
BibTex | DOI | Web page | PDF ]
[VLC09]
J. Villard, É. Lozes, and C. Calcagno. Proving Copyless Message Passing. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems (APLAS'09), volume 5904 of Lecture Notes in Computer Science, pages 194--209, Seoul, Korea, December 2009. Springer.
doi: 10.1007/978-3-642-10672-9_15.
BibTex | DOI | Web page | PDF ]
[BDL09]
R. Brochenin, S. Demri, and É. Lozes. Reasoning about sequences of memory states. Annals of Pure and Applied Logics, 161(3):305--323, December 2009.
doi: 10.1016/j.apal.2009.07.004.
BibTex | DOI | Web page | PDF ]
[DG09]
S. Demri and R. Gascon. The Effects of Bounding Syntactic Resources on Presburger LTL. Journal of Logic and Computation, 19(6):1541--1575, December 2009.
doi: 10.1093/logcom/exp037.
BibTex | DOI | Web page | PDF ]
[Bou09]
F. Bouchy. Logiques et modèles pour la vérification de systèmes infinis. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2009.
BibTex | Web page | PDF ]
[BFS09a]
F. Bouchy, A. Finkel, and P. San Pietro. Dense-choice Counter Machines Revisited. In Proceedings of the 11th International Workshops on Verification of Infinite State Systems (INFINITY'09), volume 10 of Electronic Proceedings in Theoretical Computer Science, pages 3--22, Bologna, Italy, November 2009.
doi: 10.4204/EPTCS.10.1.
BibTex | DOI | Web page | PDF ]
[LCE+09]
LIAFA, CRIL, EDF, LSV, and Verimag. Projet RNTL Averiles -- Fourniture F2.2 : Algorithmes de vérification -- Rapport final, November 2009. 25 pages.
BibTex | Web page | PDF ]
[FLS09]
A. Finkel, É. Lozes, and A. Sangnier. Towards Model Checking Pointer Systems. In Revised Selected Papers of the International Conference on Infinity in Logic & Computation (ILC'07), volume 5489 of Lecture Notes in Artificial Intelligence, pages 56--82, Cape Town, South Africa, October 2009. Springer-Verlag.
doi: 10.1007/978-3-642-03092-5_6.
BibTex | DOI | Web page | PS | PDF ]
[Dim09]
J. Dimino. Les systèmes à canaux non-fiables vus comme des transducteurs. Rapport de stage de M1, Master Parisien de Recherche en Informatique, Paris, France, October 2009.
BibTex | Web page | PDF ]
[BCHK09]
Y. Boichut, R. Courbis, P.-C. Héam, and O. Kouchnarenko. Handling Non-left Linear Rules when Completing Tree Automata. International Journal of Foundations of Computer Science, 20(5):837--849, October 2009.
doi: 10.1142/S0129054109006917.
BibTex | DOI | Web page | PDF ]
[DHL09]
F. Dadeau, P.-C. Héam, and J. Levrey. On the Use of Uniform Random Generation of Automata for Testing. In Proceedings of the 5th Workshop on Model-Based Testing (MBT'09), volume 253 of Electronic Notes in Theoretical Computer Science, pages 37--51, York, UK, October 2009. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2009.09.050.
BibTex | DOI | Web page | PDF ]
[BHK09]
Y. Boichut, P.-C. Héam, and O. Kouchnarenko. How to Tackle Integer Weighted Automata Positivity. In Proceedings of the 3rd Workshop on Reachability Problems in Computational Models (RP'09), volume 5797 of Lecture Notes in Computer Science, pages 79--92, Palaiseau, France, September 2009. Springer.
doi: 10.1007/978-3-642-04420-5_9.
BibTex | DOI | Web page | PDF ]
[EF09]
E. Encrenaz and A. Finkel. Automatic verification of counter systems with ranking functions. In Joint Proceedings of the 8th, 9th and 10th International Workshops on Verification of Infinite State Systems (INFINITY'06,'07,'08), volume 239 of Electronic Notes in Theoretical Computer Science, pages 85--103. Elsevier Science Publishers, July 2009.
doi: 10.1016/j.entcs.2009.05.032.
BibTex | DOI | Web page | PS | PDF ]
[BFS09b]
F. Bouchy, A. Finkel, and A. Sangnier. Reachability in Timed Counter Systems. In Joint Proceedings of the 8th, 9th and 10th International Workshops on Verification of Infinite State Systems (INFINITY'06,'07,'08), volume 239 of Electronic Notes in Theoretical Computer Science, pages 167--178. Elsevier Science Publishers, July 2009.
doi: 10.1016/j.entcs.2009.05.038.
BibTex | DOI | Web page | PDF ]
[HV09]
P. Habermehl and T. Vojnar, editors. Joint Proceedings of the 8th, 9th and 10th International Workshops on Verification of Infinite State Systems (INFINITY'06,'07,'08), volume 239 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, July 2009.
doi: 10.1016/j.entcs.2009.05.026.
BibTex | DOI ]
[CHK09]
R. Courbis, P.-C. Héam, and O. Kouchnarenko. TAGED Approximations for Veriying Temporal Patterns. In Proceedings of the 14th International Conference on Implementation and Application of Automata (CIAA'09), volume 5642 of Lecture Notes in Computer Science, pages 135--144, Sydney, Australia, July 2009. Springer-Verlag.
doi: 10.1007/978-3-642-02979-0_17.
BibTex | DOI | Web page | PDF ]
[HNS09]
P.-C. Héam, C. Nicaud, and S. Schmitz. Random Generation of Deterministic Tree (Walking) Automata. In Proceedings of the 14th International Conference on Implementation and Application of Automata (CIAA'09), volume 5642 of Lecture Notes in Computer Science, pages 115--124, Sydney, Australia, July 2009. Springer-Verlag.
doi: 10.1007/978-3-642-02979-0_15.
BibTex | DOI | Web page | PDF ]
[FG09b]
A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. In Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP'09), volume 5556 of Lecture Notes in Computer Science, pages 188--199, Rhodes, Greece, July 2009. Springer.
doi: 10.1007/978-3-642-02930-1_16.
BibTex | DOI | Web page | PDF ]
[BBL09]
K. Bansal, R. Brochenin, and É. Lozes. Beyond Shapes: Lists with Ordered Data. In Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'09), volume 5504 of Lecture Notes in Computer Science, pages 425--439, York, UK, March 2009. Springer.
doi: 10.1007/978-3-642-00596-1_30.
BibTex | DOI | Web page | PDF ]
[FG09a]
A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part I: Completions. In Proceedings of the 26th Annual Symposium on Theoretical Aspects of Computer Science (STACS'09), volume 3 of Leibniz International Proceedings in Informatics, pages 433--444, Freiburg, Germany, February 2009. Leibniz-Zentrum für Informatik.
BibTex | Web page | PDF ]
[San08]
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.
BibTex | Web page | PS | PDF ]
[BFLP08]
S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Acceleration from theory to practice. International Journal on Software Tools for Technology Transfer, 10(5):401--424, October 2008.
doi: 10.1007/s10009-008-0064-3.
BibTex | DOI | Web page ]
[BHK08]
Y. Boichut, P.-C. Héam, and O. Kouchnarenko. Approximation-based Tree Regular Model-Checking. Nordic Journal of Computing, 14(3):216--241, October 2008.
BibTex | Web page | PDF ]
[BDL08]
R. Brochenin, S. Demri, and É. Lozes. On the Almighty Wand. In Proceedings of the 17th Annual EACSL Conference on Computer Science Logic (CSL'08), volume 5213 of Lecture Notes in Computer Science, pages 323--338, Bertinoro, Italy, September 2008. Springer.
doi: 10.1007/978-3-540-87531-4_24.
BibTex | DOI | Web page | PDF ]
[LHS08]
É. Lozes, D. Hirschkoff, and D. Sangiorgi. Separability in the Ambient Logic. Logical Methods in Computer Science, 4(3:4), September 2008.
doi: 10.2168/LMCS-4(3:4)2008.
BibTex | DOI | Web page | PS | PDF ]
[CS08a]
P. Chambart and Ph. Schnoebelen. Mixing Lossy and Perfect Fifo Channels. In Proceedings of the 19th International Conference on Concurrency Theory (CONCUR'08), volume 5201 of Lecture Notes in Computer Science, pages 340--355, Toronto, Canada, August 2008. Springer.
doi: 10.1007/978-3-540-85361-9_28.
BibTex | DOI | Web page | PS | PDF ]
[LV08]
É. Lozes and J. Villard. A Spatial Equational Logic for the Applied π-Calculus. In Proceedings of the 19th International Conference on Concurrency Theory (CONCUR'08), volume 5201 of Lecture Notes in Computer Science, pages 387--401, Toronto, Canada, August 2008. Springer.
doi: 10.1007/978-3-540-85361-9_31.
BibTex | DOI | Web page | PDF ]
[FS08]
A. Finkel and A. Sangnier. Reversal-bounded Counter Machines Revisited. In Proceedings of the 33rd International Symposium on Mathematical Foundations of Computer Science (MFCS'08), volume 5162 of Lecture Notes in Computer Science, pages 323--334, Toruń, Poland, August 2008. Springer.
doi: 10.1007/978-3-540-85238-4_26.
BibTex | DOI | Web page | PS | PDF ]
[BHH+08]
A. Bouajjani, P. Habermehl, L. Holík, T. Touili, and T. Vojnar. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In Proceedings of the 13th International Conference on Implementation and Application of Automata (CIAA'08), volume 5148 of Lecture Notes in Computer Science, pages 57--67, San Francisco, California, USA, July 2008. Springer-Verlag.
doi: 10.1007/978-3-540-70844-5_7.
BibTex | DOI | Web page | PDF ]
[CS08c]
P. Chambart and Ph. Schnoebelen. The Ordinal Recursive Complexity of Lossy Channel Systems. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS'08), pages 205--216, Pittsburgh, Pennsylvania, USA, June 2008. IEEE Computer Society Press.
doi: 10.1109/LICS.2008.47.
BibTex | DOI | Web page | PDF ]
[BFL08]
F. Bouchy, A. Finkel, and J. Leroux. Decomposition of Decidable First-Order Logics over Integers and Reals. In Proceedings of the 15th International Symposium on Temporal Representation and Reasoning (TIME'08), pages 147--155, Montréal, Canada, June 2008. IEEE Computer Society Press.
doi: 10.1109/TIME.2008.22.
BibTex | DOI | Web page | PDF ]
[HIV08]
P. Habermehl, R. Iosif, and T. Vojnar. What else is decidable about arrays? In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), volume 4962 of Lecture Notes in Computer Science, pages 474--489, Budapest, Hungary, March-April 2008. Springer.
doi: 10.1007/978-3-540-78499-9_33.
BibTex | DOI | Web page | PDF ]
[CS08b]
P. Chambart and Ph. Schnoebelen. The ω-Regular Post Embedding Problem. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), volume 4962 of Lecture Notes in Computer Science, pages 97--111, Budapest, Hungary, March-April 2008. Springer.
doi: 10.1007/978-3-540-78499-9_8.
BibTex | DOI | Web page | PS | PDF ]
[VLT08]
J. Villard, É. Lozes, and R. Treinen. A Spatial Equational Logic for the Applied pi-calculus. Research Report LSV-08-10, Laboratoire Spécification et Vérification, ENS Cachan, France, March 2008. 44 pages.
BibTex | Web page | PDF ]
[FL08]
A. Finkel and J. Leroux. Presburger Functions are Piecewise Linear. Research Report LSV-08-08, Laboratoire Spécification et Vérification, ENS Cachan, France, March 2008. 9 pages.
BibTex | Web page | PDF ]
[BMO+08]
P. Bouyer, N. Markey, J. Ouaknine, Ph. Schnoebelen, and J. Worrell. On Termination for Faulty Channel Machines. In Proceedings of the 25th Annual Symposium on Theoretical Aspects of Computer Science (STACS'08), volume 1 of Leibniz International Proceedings in Informatics, pages 121--132, Bordeaux, France, February 2008. Leibniz-Zentrum für Informatik.
BibTex | Web page | PS | PDF ]
[CS07]
P. Chambart and Ph. Schnoebelen. Post Embedding Problem is not Primitive Recursive, with Applications to Channel Systems. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), volume 4855 of Lecture Notes in Computer Science, pages 265--276, New Delhi, India, December 2007. Springer.
doi: 10.1007/978-3-540-77050-3_22.
BibTex | DOI | Web page | PS | PDF ]
[BBS07]
C. Baier, N. Bertrand, and Ph. Schnoebelen. Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Transactions on Computational Logic, 9(1), December 2007.
doi: 10.1145/1297658.1297663.
BibTex | DOI | Web page | PS | PDF ]
[HIRV07]
P. Habermehl, R. Iosif, A. Rogalewicz, and T. Vojnar. Proving Termination of Tree Manipulating Programs. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07), volume 4762 of Lecture Notes in Computer Science, pages 145--161, Tokyo, Japan, October 2007. Springer.
doi: 10.1007/978-3-540-75596-8_12.
BibTex | DOI | Web page | PS | PDF ]
[DR07]
S. Demri and A. Rabinovich. The complexity of temporal logic with until and since over ordinals. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), volume 4790 of Lecture Notes in Artificial Intelligence, pages 531--545, Yerevan, Armenia, October 2007. Springer.
doi: 10.1007/978-3-540-75560-9_38.
BibTex | DOI | Web page | PDF ]
[Cha07]
P. Chambart. Canaux fiables et non-fiables : frontières de la décidabilité. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2007.
BibTex | Web page | PDF ]
[Vil07]
J. Villard. Logique spatiale pour le pi-calcul appliqué. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2007.
BibTex | Web page | PDF ]
[OBRS07]
A. Ourghanlian, M. Bozga, A. Roglewicz, and A. Sangnier. Projet RNTL Averiles -- Fourniture F1.6 : Expérimentation, September 2007. 16 pages.
BibTex | Web page | PDF ]
[LLV07]
LIAFA, LSV, and Verimag. Projet RNTL Averiles -- Fourniture F1.4 : Prototypes d'outil, September 2007. 3 pages.
BibTex | Web page | PDF ]
[LCE+07c]
LIAFA, CRIL Technology, EDF R&D, LSV, and Verimag. Projet RNTL Averiles -- Fourniture F1.3 : Algorithmes de vérification, September 2007. 19 pages.
BibTex | Web page | PDF ]
[LCE+07b]
LIAFA, CRIL Technology, EDF R&D, LSV, and Verimag. Projet RNTL Averiles -- Fourniture F1.2 : Extraction de modèles, September 2007. 19 pages.
BibTex | Web page | PDF ]
[LCE+07a]
LIAFA, CRIL Technology, EDF R&D, LSV, and Verimag. Projet RNTL Averiles -- Fourniture F1.1 : Modèles, September 2007. 6 pages.
BibTex | Web page | PDF ]
[LCE+07d]
LIAFA, CRIL Technology, EDF R&D, LSV, and Verimag. Rapport à mi-parcours du projet RNTL Averiles (analyse et vérification de logiciels embarqués avec structures de mémoire dynamique, September 2007. 4 pages.
BibTex | Web page | PDF ]
[BHJS07]
A. Bouajjani, P. Habermehl, Y. Jurski, and M. Sighireanu. Rewriting Systems with Data -- A Framework for Reasoning About Systems with Unbounded Structures over Infinite Data Domains. In Proceedings of the 16th International Symposium on Fundamentals of Computation Theory (FCT'07), volume 4639 of Lecture Notes in Computer Science, pages 1--22, Budapest, Hungary, August 2007. Springer.
doi: 10.1007/978-3-540-74240-1_1.
BibTex | DOI | Web page | PS | PDF ]
[BDL07]
R. Brochenin, S. Demri, and É. Lozes. Reasoning about Sequences of Memory States. In Proceedings of the 1st Workshop on Heap Analysis and Verification (HAV'07), Braga, Portugal, March 2007.
BibTex | Web page | PDF ]
[BBS06b]
C. Baier, N. Bertrand, and Ph. Schnoebelen. On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems. In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), volume 4246 of Lecture Notes in Artificial Intelligence, pages 347--361, Phnom Penh, Cambodia, November 2006. Springer.
doi: 10.1007/11916277_24.
BibTex | DOI | Web page | PS | PDF ]
[SBS06]
Ph. Schnoebelen, A. Bouajjani, and G. Sutre. ACI Sécurité Informatique PERSÉE --- Rapport final, November 2006. 12 pages.
BibTex | Web page | PDF ]
[DFGvD06]
S. Demri, A. Finkel, V. Goranko, and G. van Drimmelen. Towards a model-checker for counter systems. In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), volume 4218 of Lecture Notes in Computer Science, pages 493--507, Beijing, China, October 2006. Springer.
doi: 10.1007/11901914_36.
BibTex | DOI | Web page | PDF ]
[Ber06a]
N. Bertrand. Modèles stochastiques pour les pertes de messages dans les protocoles asynchrones et techniques de vérification automatique. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2006.
BibTex | Web page | PS | PDF ]
[BBS06c]
C. Baier, N. Bertrand, and Ph. Schnoebelen. Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness. In Proceedings of 26th IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'06), volume 4229 of Lecture Notes in Computer Science, pages 212--227, Paris, France, September 2006. Springer.
doi: 10.1007/11888116_17.
BibTex | DOI | Web page | PS | PDF ]
[BLP06]
S. Bardin, J. Leroux, and G. Point. FAST Extended Release. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 63--66, Seattle, Washington, USA, August 2006. Springer.
doi: 10.1007/11817963_9.
BibTex | DOI | Web page | PS | PDF ]
[KS06]
A. Kučera and Ph. Schnoebelen. A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications. Theoretical Computer Science, 358(2-3):315--333, August 2006.
doi: 10.1016/j.tcs.2006.01.021.
BibTex | DOI | Web page | PS | PDF ]
[BS06]
N. Bertrand and Ph. Schnoebelen. A short visit to the STS hierarchy. In Proceedings of the 12th International Workshop on Expressiveness in Concurrency (EXPRESS'05), volume 154 of Electronic Notes in Theoretical Computer Science, pages 59--69, San Francisco, California, USA, July 2006. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2006.05.007.
BibTex | DOI | Web page | PS | PDF ]
[Bro06]
R. Brochenin. Techniques d'automates pour raisonner sur la mémoire. Rapport de Master, Master Recherche Informatique de Lyon --- Informatique Fondamentale, Lyon, France, June 2006.
BibTex | Web page | PS ]
[FGRV06]
A. Finkel, G. Geeraerts, J.-F. Raskin, and L. Van Begin. On the ω-Language Expressive Power of Extended Petri Nets. Theoretical Computer Science, 356(3):374--386, May 2006.
doi: 10.1016/j.tcs.2006.02.008.
BibTex | DOI | Web page | PDF ]
[BFLS06]
S. Bardin, A. Finkel, É. Lozes, and A. Sangnier. From Pointer Systems to Counter Systems Using Shape Analysis. In Proceedings of the 5th International Workshop on Automated Verification of Infinite-State Systems (AVIS'06), Vienna, Austria, April 2006.
BibTex | Web page | PS | PDF ]
[Ber06b]
N. Bertrand. SuMo -- Reachability analysis for lossy channels, February 2006. See [BBS06c] for a description. Written in OCaml (3000 lines).
BibTex ]
[BBS06a]
C. Baier, N. Bertrand, and Ph. Schnoebelen. A note on the attractor-property of infinite-state Markov chains. Information Processing Letters, 97(2):58--63, January 2006.
doi: 10.1016/j.ipl.2005.09.011.
BibTex | DOI | Web page | PS | PDF ]

This file was generated by bibtex2html 1.98.

About LSV