Publications
From Averiss
- Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Mihaela Sighireanu. A Logic-Based Framework for Reasoning about Composite Data Structures. In CONCUR'09, Springer, LNCS volume 5710, pages 178-195 (2009) pdf [BoDES09]
- Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer. Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. In TACAS'09 Springer, LNCS, volume 5797,pages 107-123 (2009) pdf [AtBQ09]
- Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar. Composed Bisimulation for Tree Automata. In International Journal of Computer Science volume 20(4), pages 685-700 (2009) pdf [AbBHKV09]
- Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Yan Jurski, Mihaela Sighireanu. A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes. In Logical Methods in Computer Science volume 5(2), (2009) pdf [BoDEJS09]
- Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konecný, Tomás Vojnar. Automatic Verification of Integer Array Programs. In CAV'09 Springer, LNCS, volume 5643,pages: 157-172 (2009) ps [BoHIKV09]
- Benedikt Bollig, Manuela-Lidia Grindei, Peter Habermehl. Realizability of Concurrent Recursive Programs. In FOSSACS'09 Springer, LNCS, volume 5504, pages 410-424 (2009) pdf [BoGH09]
- Mohamed Faouzi Atig, Peter Habermehl. On Yen's Path Logic for Petri Nets. In RP'09 Springer, LNCS, volume 5797, pages 51-63 (2009)pdf [AtH09]
- Mohamed Faouzi Atig, Tayssir Touili. Verifying Parallel Programs with Dynamic Communication Structures. In CIAA'09, Springer, LNCS, volume 5642, pages: 145-154 (2009) ps [AtTo09]
- Tayssir Touili. Constrained Reachability of Process Rewrite Systems. In ICTAC'09 Springer, LNCS,volume 5684, pages 307-321 (2009) ps [Touilli09]
- Nicholas Kidd, Peter Lammich, Tayssir Touili, Thomas W. Reps. A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks. In SPIN'09, Springer, LNCS, volume 5578, pages 125-142 (2009) pdf [KiLTR09]
- Narjes Ben Rajeb, Brahim Nasraoui, Riadh Robbana, Tayssir Touili. Verifying Multithreaded Recursive Programs with Integer Variables. In Electronic Notes in Theoretical Computer Science, volume 239, pages 143-154 (2009) ps [RaNRT09]
- Mihaela Sighireanu, Tayssir Touili. Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism. In Electronic Notes in Theoretical Computer Science, volume 239, pages 43-56 (2009) ps [SiTo09]
- Krishnendu Chatterjee, Thomas A. Henzinger, Florian Horn. Stochastic Games with Finitary Objectives. In MFCS'09, Springer, LNCS, volume 5734, pages 34-54 (2009) pdf [ChHH09]
- Florian Horn. Random Fruits on the Zielonka Tree. In STACS'09, pages 541-552 (2009) pdf [Horn09]
- Alain Finkel, Jean Goubault-Larrecq. Forward Analysis for WSTS, Part I: Completions. In STACS'09 (2009) pdf [FGL-stacs2009]
- Alain Finkel, Jean Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. In ICALP'09 LNCS volume 5556 (2009) pdf [FGL-icalp09]
- Florent Bouchy, Alain Finkel, Arnaud Sangnier. Reachability in Timed Counter Systems. In Infinity'08 ENTCS volume 239 pages 167-178 (2009) pdf [BFS-infinity08]
- Kshitij Bansal, Rémi Brochenin, Étienne Lozes. Beyond Shapes: Lists with Ordered Data. In FoSSaCS'09, LNCS volume 5504, pages 425-439 (2009) pdf [BBL-Fossacs09]
- Roméo Courbis, Pierre-Cyrille Héam, Olge Kouchnarenko. TAGED Approximations for Veriying Temporal Patterns . In CIAA'09, to appear LNCS (2009) pdf [CHK-ciaa09]
- Stéphane Demri, Régis Gascon.The Effects of Bounding Syntactic Resources on Presburger LTL. In Journal of Logic and Computation, Oxford University Press 2009 pdf. [DG-jlc09]
- Stéphane Demri, Paul Gastin. Specification and Verification using Temporal Logics. In Modern applications of automata theory, World Scientific,IISc Research Monographs volume 2 (2009) pdf [DG-iis09]
- Pierre-Cyrille Héam, Cyril Nicaud, Sylvain Schmitz.Random Generation of Deterministic Tree (Walking) Automata. In CIAA'09 LNCS (2009) pdf [HNS-ciaa09]
- A.Heussner, T. Le Gall, G.Sutre. Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems. In SPIN'09, LNCS (2009) pdf [Heussner-2009-SPIN]
- A.Heussner, T. Le Gall, G.Sutre. Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems. Research Report RR-1459-09, LABRI (2009) pdf [Heussner-2009-TR-LaBRI]
- A.Heussner. Model Extraction for Sockets-based Distributed Programs. In HAL, nr. hal-00425099, (2009) pdf [Heussner-2009]
- Bernard Boigelot, Julien Brusten, Jérôme Leroux. A Generalization of Semenov's Theorem to Automata over Real Numbers. In CADE'09 LNCS (2009)pdf [BOIGELOT-BRUSTEN-LEROUX-CADE2009]
- Jérôme Leroux. The General Vector Addition System Reachability Problem by Presburger Inductive Invariants. In LICS'09, IEEE Computer Society (2009) pdf [LEROUX-LICS2009]
- Jérôme Leroux, Gérald Point. TaPAS : The Talence Presburger Arithmetic Suite. In TACAS'09, Springer, LNCS, volume 5505, pages 182-185 (2009)pdf [LEROUX-POINT-TACAS2009]
- Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine. Monotonic Abstraction for Programs with Dynamic Memory Heaps. In CAV'08, volume 5123 (2008) pdf [ABCHR08]
- Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holik, Lisa Kaati, Tomás Vojnar. Composed Bisimulation for Tree Automata. In CIAA'08, LNCS volume 5148, pages 212-222 (2008)pdf [ABHKV08a]
- Ahmed Bouajjani, Peter Habermehl, Lukás Holik,Tayssir Touili, Tomás Vojnar Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In CIAA'08, LNCS volume 5148, pages 57-67 (2008)ps [BHHTV08]
- Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili. On the Reachability Analysis of Acyclic Networks of Pushdown Systems. In CONCUR'08, LNCS volume 5201, pages 356-371 (2008) ps [AtBT08a]
- Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili. Analyzing Asynchronous Programs with Preemption. In FSTTCS'08, LNCS volume 08004 (2008) ps [AtBT08b]
- Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holik, Lisa Kaati, Tomás Vojnar. Computing Simulations over Tree Automata. In TACAS'08, LNCS volume 4963, pages 93-108 (2008) pdf [ABHKV08b]
- Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar. Verification of parametric concurrent systems with prioritised FIFO resource management. In Formal Methods in System Design, volume 32, number 2, pages 129-172 (2008) pdf [BoHV08]
- Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Orso. Monotonic and Downward Closed Games. In J. Log. Comput., volume 18, number 1, pages 153-169 (2008) ps [AbBO08]
- Mohamed Faouzi Atig, Benedikt Bollig, Peter Habermehl. Emptiness of Multi-pushdown Automata Is 2ETIME-Complete. In DLT'08, LNCS volume 5257, pages 121-133 (2008)pdf [AtBH08]
- Peter Habermehl, Radu Iosif, Tomás Vojnar. What Else Is Decidable about Integer Arrays?. In FoSSaCS'08, LNCS volume 4962, pages 474-489 (2008) pdf [HaIV08a]
- Peter Habermehl, Radu Iosif, Tomás Vojnar. A Logic of Singly Indexed Arrays. In LPAR'08, LNCS volume 5330, pages 558-573 (2008) pdf [HaIV08b]
- Akash Lal,Tayssir Touili, Nicholas Kidd, Thomas W. Reps. Interprocedural Analysis of Concurrent Programs Under a Context Bound. In TACAS'08, LNCS volume 4963, pages 282-298 (2008) ps [LTKR08]
- Florian Horn. Explicit Muller Games are PTIME. In FSTTCS'08, LNCS volume 08004 (2008)pdf [Horn08]
- Julien Cristau, Florian Horn. Graph Games on Ordinals. In FSTTCS'08, LNCS volume 08004 (2008) pdf [CrHo08]
- Hugo Gimbert, Florian Horn. Simple Stochastic Games with Few Random Vertices Are Easy to Solve. In FoSSaCS'08 LNCS volume 4962, pages 5-19 (2008)pdf [GiHo08b]
- Nutan Limaye, Meena Mahajan, Antoine Meyer. On the Complexity of Membership and Counting in Height-Deterministic Pushdown Automata. In CSR'08, LNCS volume 5010, pages 240-251 (2008) pdf [LiMM08]
- Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H. Luke Ong, Olivier Serre. Winning Regions of Higher-Order Pushdown Games. In LICS'08, IEEE Computer Society (2008) pdf [CHMOS08]
- Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci. FAST: Acceleration from theory to practice. In International Journal on Software Tools for Technology Transfer Springer volume 10, pages 401-424 (2008) pdf [BFLP-sttt08]
- Alain Finkel, Arnaud Sangnier. Reversal-bounded Counter Machines Revisited. In MFCS'08, LNCS volume 5162, pages 323-334 (2008) pdf [FS-mfcs08]
- Florent Bouchy, Alain Finkel, Jérôme Leroux. Decomposition of Decidable First-Order Logics over Integers and Reals. In TIME'08, IEEE Computer Society Press, pages 147-155 (2008) pdf [BFL-time08]
- Pierre Chambart, Philippe Schnoebelen.Mixing Lossy and Perfect Fifo Channels. In CONCUR'08, LNCS volume 5201, pages 340-355 (2008) pdf [CS-concur08]
- Pierre Chambart, Philippe Schnoebelen.The Ordinal Recursive Complexity of Lossy Channel Systems. In LICS'08, IEEE Computer Society Press (2008) pdf [CS-lics08]
- Pierre Chambart, Philippe Schnoebelen. The ω-Regular Post Embedding Problem. In FoSSaCS'08 LNCS volume 4962 pages 97-111 (2008) pdf [CS-fossacs08]
- Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, James Worrell. On Termination for Faulty Channel Machines. In STACS'08 IBFI pages 121-132 (2008) pdf [BMOSW-stacs08]
- Stéphane Demri, Régis Gascon. Verification of Qualitative Z constraints. In Theoretical Computer Science, Elsevier Science Publishers volume 409 (2008) pdf [DG-tcs08]
- Stéphane Demri, Ranko Lazić, Arnaud Sangnier.Model checking freeze LTL over one-counter automata. In FoSSaCS'08 LNCS volume 4962, pages 490-504 (2008) pdf. [DLS-fossacs08]
- Stéphane Demri, Ranko Lazić. LTL with the freeze quantifier and register automata. In ACM Transactions on Computational Logic} ACM Press (2008) pdf [DL-tocl08]
- Alexander Heussner, Grégoire Sutre, Tristan Le Gall. CEGAR for Communicating FIFO Machines. In Workshop Proceedings of MEMICS 2008 pages 68-75 (2008) pdf [heussner-a-2008-68-a]
- Andrzej S. Murawski, Igor Walukiewicz. Third-Order Idealized Algol with Iteration is Decidable. In TCS volume 390, pages 214-229 (2008) pdf [MurWal08]
- Jérôme Leroux. Structural Presburger Digit Vector Automata. In Theoretical Computer Science, Elsevier, volume 409, number 3, pages 549--556 (2008) pdf [LEROUX-TCS2008]
- Jérôme Leroux. Convex Hull of Arithmetic Automata. In SAS'08, Springer, LNCS volume 5059, pages 47-61 (2008) ps [LEROUX-SAS2008]
- Florent Bouchy, Jérôme Leroux, Alain Finkel. Decomposition of Decidable First-Order Logics over Integers and Reals. In TIME'08, IEEE Computer Society Press, pages 147-155 (2008) ps [BOUCHY-LEROUX-FINKEL-TIME2008]
- Nicolas Caniart, Emmanuel Fleury, Jérôme Leroux, Marc Zeitoun. Accelerating Interpolation-based Model-Checking. In TACAS'08 Springer, LNCS volume 4963 (2008) pdf [CANIART-FLEURY-LEROUX-ZEITOUN-TACAS2008]
- Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci. FAST: acceleration from theory to practice. In International Journal on Software Tools for Technology Transfer (STTT), Springer, volume 10, pages 410-424 (2008) ps [BARDIN-FINKEL-LEROUX-PETRUCCI-STTT2008]
- Christel Baier, Nathalie Bertrand, Philippe Schnoebelen. Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. In ACM Transactions on Computational Logic, volume 9(1) (2007)pdf [BBS07]
- Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Larsen, Didier Lime. UPPAAL-Tiga: Time for Playing Games! In CAV'07, LNCS volume 4590, pages 121-125 (2007)pdf [BCDFLL07]
- Rémi Brochenin, Stéphane Demri, Étienne Lozes. Reasoning about sequences of memory states. In LFCS'07, LNCS volume 4514, pages 100-114 (2007)pdf [BDL07]
- Rémi Brochenin, Stéphane Demri, Étienne Lozes. Reasoning about Sequences of Memory States. In Proceedings of the 1st Workshop on Heap Analysis and Verification (2007)pdf [BDL07b]
- Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer. Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. In CAV'07, LNCS volume 4590, pages 207-220 (2007) pdf [BFQ07]
- Ahmed Bouajjani, Peter Habermehl, Yan Jurski, Mihaela Sighireanu. Rewriting Systems with Data. In FCT'07, LNCS volume 4639, pages 1-22 (2007) pdf [BHJS07]
- Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu. A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes. In TACAS'07, LNCS volume 4424, pages 690-705 (2007)pdf [BJS07]
- Ahmed Bouajjani, Anca Muscholl, Tayssir Touili. Permutation Rewriting and Algorithmic Verification. Information and Computation, volume 205(2), pages 199-224 (2007) ps [BMT07]
- Ahmed Bouajjani, Jan Strejcek, Tayssir Touili. On Symbolic Verification of Weakly Extended PAD. Electronic Notes in Theoretical Computer Science, volume 175(3), pages 47-64 (2007) ps [BST07]
- Ahmed Bouajjani, Tayssir Touili, Laurent van Begin. On the Reachability Game for Dynamic Networks of Pushdown Processes. Technical report, LIAFA, University Paris 7 (2007) [BTvB07]
- Pierre Chambart, Philippe Schnoebelen. Post Embedding Problem is not Primitive Recursive, with Applications to Channel Systems. In FSTTCS'07, LNCS volume 4855, pages 265-276 (2007)pdf [CS07]
- Patrick Chervet, Igor Walukiewicz. Minimizing Variants of Visibly Pushdown Automata. In MFCS'07, LNCS volume 4708, pages 135—146 (2007)pdf [CW07]
- Davide D'Aprile, Susanna Donatelli, Arnaud Sangnier, Jeremy Sproston. From Time Petri Nets to Timed Automata: An Untimed Approach. In TACAS'07, LNCS volume 4424, pages 216-230 (2007)pdf [DADSS07]
- Emmanuelle Encrenaz, Alain Finkel. Automatic verification of counter systems with ranking functions. In INFINITY'07, Electronic Notes in Theoretical Computer Science, à paraître (2008) pdf [EF07]
- Alain Finkel, Étienne Lozes, Arnaud Sangnier. Towards Model Checking Pointer Systems. In Proceedings of the International Conference on Infinity in Logic & Computation (2007)pdf [FLS07]
- Hugo Gimbert, Wieslaw Zielonka. Perfect Information Stochastic Priority Games. In ICALP'07, LNCS volume 4596, pages 850-861 (2007)pdf [GZ07]
- Hugo Gimbert, Wieslaw Zielonka Limits of Multi-Discounted Markov Decision Processes. In LICS'07, IEEE Computer Society, pages 89-98 (2007)pdf [GZ07b]
- Florian Horn. Faster Algorithms for Finitary Games. In TACAS'07, LNCS volume 4424, pages 472-484 (2007)pdf [H07]
- Florian Horn. Dicing on the Streett. In Information Processing Letters, volume 104(1), pages 1-9 (2007)ps [H07b]
- Peter Habermehl, Radu Iosif, Adam Rogalewicz, Tomás Vojnar. Proving Termination of Tree Manipulating Programs. In ATVA'07, LNCS volume 4762, pages 145-161 (2007)ps [HIRV07]
- Frédéric Herbreteau, Grégoire Sutre, The Quang Tran: Unfolding Concurrent Well-Structured Transition Systems. Unfolding Concurrent Well-Structured Transition Systems. In TACAS'07, LNCS volume 4424, pages 706—720 (2007) ps [HST07]
- Akash Lal, Nicholas Kidd, Thomas Reps, Tayssir Touili. Abstract Error Projection. In SAS'07, LNCS volume 4634, pages 200-217 (2007)ps [LKTR07]
- Christof Löding, Carsten Lutz, Olivier Serre. Propositional dynamic logic with recursive programs. In J. Log. Algebr. Program., volume 73(1-2), pages 51-69 (2007) pdf [LLS07]
- Jérôme Leroux, Grégoire Sutre. Acceleration in Convex Data-Flow Analysis. In FSTTCS'07, LNCS volume 4855, pages 520—531 (2007) pdf [LS07]
- Jérôme Leroux, Grégoire Sutre. Accelerated Data-flow Analysis. In SAS'07, LNCS volume 4634, pages 184—199 (2007) pdf [LS07b]
- Anca Muscholl, Igor Walukiewicz. A lower bound on web services composition. In FOSSACS'07, LNCS (2007) pdf [MW07]
- Gaël Patin, Mihaela Sighireanu, Tayssir Touili. Spade: Verification of Multithreaded Dynamic and Recursive Programs. In CAV'07, LNCS volume 4590, pages 254-257 (2007)ps [PST07]
- Tayssir Touili. Computing Transitive Closures of Hedge Transformations. In VECOS'07, eWIC Series, British Computer Society (2007)ps [T07]
- Greta Yorsh, Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani. A logic of reachable patterns in linked data-structures. In Journal of Logic and Algebraic Programming, volume 73(1-2), pages 111-142 (2007)pdf [YRSMB07]
- André Arnold Igor Walukiewicz. Nondeterministic controllers of nondeterministic processes . In Logic and Automata, Amsterdam University Press, volume (2) (2007) pdf [ArnWal07]
- Mikolaj Bojanczyk, Igor Walukiewicz. Forest Algebras. In Logic and Automata, Amsterdam University Press, volume 2, pages 107-132 (2007) pdf [bojwal07]