| 2007 | CSR | Decidability of Parameterized Probabilistic Information Flow. | Danile Beauquier, Marie Duflot, Yury Lifshits |
| 2004 | TACAS | Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic. | Danile Beauquier, Tristan Crolard, Evguenia Prokofieva |
| 2002 | CSL | A Logic of Probability with Decidable Model-Checking. | Danile Beauquier, Alexander Moshe Rabinovich, Anatol Slissenko |
| 1999 | FCT | Decidable Classes of the Verification Problem in a Timed Predicate Logic. | Danile Beauquier, Anatol Slissenko |
| 1998 | FOSSACS | Pumping Lemmas for Timed Automata. | Danile Beauquier |
| 1995 | MFCS | On the Complexity of Finite Memory Policies for Markov Decision Processes. | Danile Beauquier, Dima Burago, Anatol Slissenko |
| 1993 | MFCS | Rabin Tree Automata and Finite Monoids. | Danile Beauquier, Andreas Podelski |
| 1992 | LATIN | A Decidability Result about Convex Polyominoes. | Danile Beauquier, Michel Latteux, Karine Slowinski |
| 1991 | FCT | About the Effect of the Number of Successful Paths in an Infinite Tree on the Recognizability by a Finite Automaton with Bchi Conditions. | Danile Beauquier, Maurice Nivat, Damian Niwinski |
| 1989 | ICALP | Factors of Words. | Danile Beauquier, Jean-Eric Pin |
| 1987 | ICALP | Minimal Automaton of a Rational Cover. | Danile Beauquier |
| 1985 | FCT | Muller automata and bi-infinite words. | Danile Beauquier |
| 1985 | ICALP | About Rational Sets of Factors of a Bi-Infinite Word. | Danile Beauquier, Maurice Nivat |
| 1984 | ICALP | Some Results About Finite and Infinite Behaviours of a Pushdown Automaton. | Danile Beauquier |