Selected publications by Alain Finkel
Books
Edited Books
-
G. Berry, H. Comon and A. Finkel (eds.). Proceedings of the 13th International Conference on Computer
Aided Verification (CAV'01), Paris, France, July 2001, LNCS 2102. Springer. ( Web page | BibTeX )
-
P. Enjalbert, A. Finkel and K. W. Wagner (eds.). Proceedings of the 10th Annual Symposium on Theoretical
Aspects of Computer Science (STACS'93), February 1993, LNCS 665. Springer-Verlag. ( Web page | BibTeX )
-
A. Finkel and M. Jantzen (eds.). Proceedings of the 9th Annual Symposium on Theoretical
Aspects of Computer Science (STACS'92), Cachan, France, February
1992, LNCS 577. Springer-Verlag. ( Web page | BibTeX )
Journals
-
A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. Logical Methods in Computer Science, 2012. To appear. ( BibTeX + Abstract )
-
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), pages 313-344, 2010. ( PDF | BibTeX + Abstract )
-
P. Arnoux and A. Finkel. Using mental imagery processes for teaching and research in mathematics
and computer science. International Journal of Mathematical Education in Science and
Technology 41(2), pages 229-242, 2010. ( PDF | BibTeX + Abstract )
-
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), pages 401-424, 2008. ( PDF (long version) | BibTeX + Abstract )
-
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), pages 374-386, 2006. ( PDF | BibTeX + Abstract )
-
G. Cécé and A. Finkel. Verification of Programs with Half-Duplex Communication. Information and Computation 202(2), pages 166-190, 2005. ( PDF | BibTeX + Abstract )
-
A. Finkel and J. Leroux. The Convex Hull of a Regular Set of Integer Vectors is Polyhedral and
Effectively Computable. Information Processing Letters 96(1), pages 30-35, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract )
-
A. Finkel, P. McKenzie and C. Picaronny. A Well-Structured Framework for Analysing Petri Net Extensions. Information and Computation 195(1-2), pages 1-29, 2004. ( PS | PS.GZ | BibTeX )
-
A. Finkel, S. Purushothaman Iyer and G. Sutre. Well-Abstracted Transition Systems: Application to FIFO Automata. Information and Computation 181(1), pages 1-31, 2003. ( PS | PS.GZ | BibTeX )
-
A. Finkel and Ph. Schnoebelen. Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256(1-2), pages 63-92, 2001. ( PDF | PS | PS.GZ | BibTeX + Abstract )
-
A. Bouajjani, J. Esparza, A. Finkel, O. Maler, P. Rossmanith, B. Willems and P. Wolper. An Efficient Automata Approach to some Problems on Context-Free
Grammars. Information Processing Letters 74(5-6), pages 221-227, 2000. ( PS | PS.GZ | BibTeX )
-
C. Dufourd and A. Finkel. A Polynomial λ-Bisimilar Normalization for Reset Petri
Nets. Theoretical Computer Science 222(1-2), pages 187-194, 1999. ( PS | PS.GZ | BibTeX )
-
Ch. Collet, A. Finkel and R. Gherbi. CapRe: A Gaze Tracking System in Man-Machine Interaction. Journal of Advanced Computational Intelligence 2(3), pages 77-81, 1998. ( PS | PS.GZ | BibTeX )
-
A. Finkel and P. McKenzie. Verifying Identical Communicating Processes is Undecidable. Theoretical Computer Science 174(1-2), pages 217-230, 1997. ( PS | PS.GZ | BibTeX )
-
A. Finkel and I. Tellier. A Polynomial Algorithm for the Membership Problem with Categorial
Grammars. Theoretical Computer Science 164(1-2), pages 207-221, 1996. ( PDF | BibTeX )
-
G. Cécé, A. Finkel and S. Purushothaman Iyer. Unreliable Channels are Easier to Verify than Perfect Channels. Information and Computation 124(1), pages 20-31, 1996. ( PS | PS.GZ | BibTeX )
-
A. Finkel. Decidability of the Termination Problem for Completely Specified
Protocols. Distributed Computing 7(3), pages 129-135, 1994. ( BibTeX )
-
A. Finkel and L. Petrucci. Propriétés de la composition/décomposition de
réseaux de Petri et de leurs graphes de couverture. RAIRO Informatique Théorique et Applications 28(2), pages 73-124, 1994. ( BibTeX )
-
A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation 89(2), pages 144-179, 1990. ( BibTeX )
-
G. Berthelot, A. Finkel, C. Johnen and L. Petrucci. A Generic Example for Testing Performance of Reachability and Covering
Graphs Construction Algorithms. Petri Net Newsletter 35, pages 6-7, 1990. ( BibTeX )
-
A. Finkel and A. Choquet. Fifo nets without order deadlock. Acta Informatica 25, pages 15-36, 1987. ( BibTeX )
-
A. Finkel. Une généralisation des théorèmes de Higman et de
Simon aux mots infinis. Theoretical Computer Science 38, pages 137-142, 1985. ( BibTeX )
-
A. Finkel and G. Memmi. An introduction to Fifo nets - monogeneous nets: a subclass of
Fifo nets. Theoretical Computer Science 35, pages 191-214, 1985. ( BibTeX )
Conferences
-
M. Cadilhac, A. Finkel and P. McKenzie. Bounded Parikh Automata. In WORDS'11, Electronic Proceedings in Theoretical Computer Science 63, pages 93-102. 2011. ( PDF | BibTeX )
-
M. Cadilhac, A. Finkel and P. McKenzie. On the Expressiveness of Parikh Automata and Related Models. In CMA'11, books@ocg.at 282, pages 103-119. Austrian Computer Society, 2011. ( PDF | BibTeX )
-
P. Chambart, A. Finkel and S. Schmitz. Forward Analysis and Model Checking for Trace Bounded WSTS. In ICATPN'11, LNCS 6709. Springer, 2011. ( Web page | PDF (long version) | BibTeX + Abstract )
-
R. Bonnet, A. Finkel, S. Haddad and F. Rosa-Velardo. Ordinal Theory for Expressiveness of Well Structured Transition
Systems. In FoSSaCS'11, LNCS 6604, pages 153-167. Springer, 2011. ( PDF | BibTeX )
-
R. Bonnet, A. Finkel, J. Leroux and M. Zeitoun. Place-Boundedness for Vector Addition Systems with one zero-test. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 192-203. Leibniz-Zentrum für Informatik, 2010. ( PDF | BibTeX + Abstract )
-
A. Finkel and A. Sangnier. Mixing coverability and reachability to analyze VASS with one
zero-test. In SOFSEM'10, LNCS 5901, pages 394-406. Springer, 2010. ( PDF | PS | PS.GZ | PDF (long version) | BibTeX + Abstract )
-
F. Bouchy, A. Finkel and P. San Pietro. Dense-choice Counter Machines revisited. In INFINITY'09, Electronic Proceedings in Theoretical Computer Science 10, pages 3-22. 2009. ( PDF | BibTeX + Abstract )
-
A. Finkel, É. Lozes and A. Sangnier. Towards Model Checking Pointer Systems. In ILC'07, LNAI 5489, pages 56-82. Springer-Verlag, 2009. ( PDF | PS | PS.GZ | BibTeX + Abstract )
-
F. Bouchy, A. Finkel and A. Sangnier. Reachability in Timed Counter Systems. In INFINITY'06,'07,'08, ENTCS 239, pages 167-178. Elsevier Science Publishers, 2009. ( PDF | BibTeX + Abstract )
-
E. Encrenaz and A. Finkel. Automatic verification of counter systems with ranking functions. In INFINITY'06,'07,'08, ENTCS 239, pages 85-103. Elsevier Science Publishers, 2009. ( PDF | PS | PS.GZ | PDF (long version) | BibTeX + Abstract )
-
A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. In ICALP'09, LNCS 5556, pages 188-199. Springer, 2009. ( PDF | BibTeX + Abstract )
-
A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part I: Completions. In STACS'09, Leibniz International Proceedings in Informatics 3, pages 433-444. Leibniz-Zentrum für Informatik, 2009. ( PDF | BibTeX + Abstract )
-
A. Finkel and A. Sangnier. Reversal-bounded Counter Machines Revisited. In MFCS'08, LNCS 5162, pages 323-334. Springer, 2008. ( PDF | PS | PS.GZ | PDF (long version) | BibTeX + Abstract )
-
F. Bouchy, A. Finkel and J. Leroux. Decomposition of Decidable First-Order Logics over Integers and Reals. In TIME'08, pages 147-155. IEEE Computer Society Press, 2008. ( PDF | BibTeX + Abstract )
-
S. Demri, A. Finkel, V. Goranko and G. van Drimmelen. Towards a model-checker for counter systems. In ATVA'06, LNCS 4218, pages 493-507. Springer, 2006. ( PDF | BibTeX + Abstract )
-
S. Bardin, A. Finkel, J. Leroux and Ph. Schnoebelen. Flat acceleration in symbolic model checking. In ATVA'05, LNCS 3707, pages 474-488. Springer, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract )
-
Ch. Darlot, A. Finkel and L. Van Begin. About Fast and TReX Accelerations. In AVoCS'04, ENTCS 128(6), pages 87-103. Elsevier Science Publishers, 2005. ( PDF | BibTeX )
-
A. Finkel, G. Geeraerts, J.-F. Raskin and L. Van Begin. On the Omega-Language Expressive Power of Extended Petri Nets. In EXPRESS'04, ENTCS 128(2), pages 87-101. Elsevier Science Publishers, 2005. ( PDF | BibTeX )
-
S. Bardin and A. Finkel. Composition of accelerations to verify infinite heterogeneous systems. In ATVA'04, LNCS 3299, pages 248-262. Springer, 2004. ( PS | PS.GZ | BibTeX + Abstract )
-
A. Finkel and J. Leroux. Image Computation in Infinite State Model Checking. In CAV'04, LNCS 3114, pages 361-371. Springer, 2004. ( PS | PS.GZ | BibTeX )
-
A. Finkel and J. Leroux. Polynomial Time Image Computation With Interval-Definable Counters
Systems. In SPIN'04, LNCS 2989, pages 182-197. Springer, 2004. ( PS | PS.GZ | BibTeX )
-
S. Bardin, A. Finkel and J. Leroux. FASTer Acceleration of Counter Automata in Practice. In TACAS'04, LNCS 2988, pages 576-590. Springer, 2004. ( PS | PS.GZ | BibTeX + Abstract )
-
S. Bardin, A. Finkel, J. Leroux and L. Petrucci. FAST: Fast Acceleration of Symbolic Transition Systems. In CAV'03, LNCS 2725, pages 118-121. Springer, 2003. ( PS | PS.GZ | BibTeX + Abstract )
-
A. Finkel and J. Leroux. How To Compose Presburger-Accelerations: Applications to Broadcast
Protocols. In FSTTCS'02, LNCS 2556, pages 145-156. Springer, 2002. ( PS | PS.GZ | BibTeX )
-
A. Finkel, J.-F. Raskin, M. Samuelides and L. Van Begin. Monotonic Extensions of Petri Nets: Forward and Backward Search
Revisited. In INFINITY'02, ENTCS 68(6), pages 121-144. Elsevier Science Publishers, 2002. ( PS | PS.GZ | BibTeX )
-
F. Herbreteau, F. Cassez, A. Finkel, O. Roux and G. Sutre. Verification of Embedded Reactive Fiffo Systems. In LATIN'02, LNCS 2286, pages 400-414. Springer, 2002. ( PS | PS.GZ | BibTeX )
-
A. Finkel, S. Purushothaman Iyer and G. Sutre. Well-Abstracted Transition Systems. In CONCUR 2000, LNCS 1877, pages 566-580. Springer, 2000. ( PS | PS.GZ | BibTeX )
-
A. Finkel and G. Sutre. An Algorithm Constructing the Semilinear Post* for 2-Dim
Reset/Transfer VASS. In MFCS 2000, LNCS 1893, pages 353-362. Springer, 2000. ( PS | PS.GZ | BibTeX )
-
A. Finkel and G. Sutre. Decidability of Reachability Problems for Classes of Two-Counter
Automata. In STACS 2000, LNCS 1770, pages 346-357. Springer, 2000. ( PS | PS.GZ | BibTeX )
-
J. Esparza, A. Finkel and R. Mayr. On the verification of broadcast protocols. In LICS'99, pages 352-359. IEEE Computer Society Press, 1999. ( PS | PS.GZ | BibTeX )
-
G. Sutre, A. Finkel, O. F. Roux and F. Cassez. Effective Recognizability and Model Checking of Reactive Fiffo
Automata. In AMAST'98, LNCS 1548, pages 106-123. Springer, 1999. ( PS | PS.GZ | BibTeX )
-
Z. Bouziane and A. Finkel. The Equivalence Problem for Commutative Semigroups and Reversible
Petri Nets is Complete in Exponential Space under Log-Lin Reducibility. In Proceedings of the International Conference in Semigroups and
its Related Topics, Kunming, China, August 1995, pages 63-76. Springer, 1998. ( BibTeX )
-
A. Finkel and I. Tellier. From Natural Language to Cognitive Style. In ICCS'95, pages 271-279. Kluwer Academic Publishers, 1998. ( PDF | BibTeX )
-
C. Dufourd, A. Finkel and Ph. Schnoebelen. Reset Nets between Decidability and Undecidability. In ICALP'98, LNCS 1443, pages 103-115. Springer, 1998. ( PS | PS.GZ | BibTeX + Abstract )
-
A. Finkel and Ph. Schnoebelen. Fundamental Structures in Well-Structured Infinite Transition Systems. In LATIN'98, LNCS 1380, pages 102-118. Springer, 1998. ( PS | PS.GZ | BibTeX )
-
C. Dufourd and A. Finkel. Polynomial-Time Many-One Reductions for Petri Nets. In FSTTCS'97, LNCS 1346, pages 312-326. Springer, 1997. ( PS | PS.GZ | BibTeX )
-
Ch. Collet, A. Finkel and R. Gherbi. Gaze Capture System in Man-Machine Interaction. In INES'97, pages 557-581. IEEE Press, 1997. ( PS | PS.GZ | BibTeX )
-
Z. Bouziane and A. Finkel. Cyclic Petri Net Reachability Sets are Semi-Linear Effectively
Constructible. In INFINITY'97, ENTCS 9, pages 15-24. Elsevier Science Publishers, 1997. ( PS | PS.GZ | BibTeX )
-
A. Finkel, B. Willems and P. Wolper. A Direct Symbolic Approach to Model Checking Pushdown Systems (Extended
Abstract). In INFINITY'97, ENTCS 9, pages 27-39. Elsevier Science Publishers, 1997. ( PS | PS.GZ | BibTeX )
-
G. Cécé and A. Finkel. Programs with Quasi-Stable Channels are Effectively Recognizable. In CAV'97, LNCS 1254, pages 304-315. Springer, 1997. ( PS | PS.GZ | BibTeX )
-
A. Finkel and I. Tellier. The Cognitive Style of Decision Making Narrations. In The Cognitive Level: Language and Mind Modelized, Duisburg L.A.U.D. Symposium, Series B: Applied and
Interdisciplinary Papers 273, pages 41-59. 1996. ( PDF | BibTeX )
-
G. Cécé, A. Finkel and S. Purushothaman Iyer. Duplication, Insertion and Lossiness Errors in Unreliable Communication
Channels. In SIGSOFT FSE'94, ACM SIGSOFT Software Engineering Notes 19(5), pages 35-43. 1994. ( BibTeX )
-
A. Finkel and I. Tellier. An Algorithmic Overview On Categorial Grammars (extended abstract). In Proceedings of the 5th Symposium on Logic and Language,
Noszvaj, Hungary, September 1994. 1994. ( BibTeX )
-
A. Finkel. The Minimal Coverability Graph for Petri Nets. In APN'91, LNCS 674, pages 210-243. Springer-Verlag, 1993. ( BibTeX )
-
A. Finkel and L. Petrucci. Avoiding State Explosion by Composition of Minimal Covering Graphs. In CAV'91, LNCS 575, pages 169-180. Springer-Verlag, 1992. ( BibTeX )
-
A. Finkel and L. Rosier. A Survey on the Decidability Questions for Classes of FIFO Nets. In APN'87, LNCS 340, pages 106-132. Springer-Verlag, 1988. ( BibTeX )
-
G. Bochmann and A. Finkel. Impact of queued interaction on protocol specification and
verification. In ISIIS'88. IOS Press, 1988. ( BibTeX )
-
A. Finkel. A new class of analysable CFSMs with unbounded FIFO channels. In PSTV'88. North-Holland, 1988. ( BibTeX )
-
A. Finkel. A generalization of the procedure of Karp and Miller to well
structured transition system. In ICALP'87, LNCS 267, pages 499-508. Springer-Verlag, 1987. ( PDF | BibTeX )
-
A. Finkel and A. Choquet. Simulation of linear fifo nets by Petri nets having a structured set
of terminal markings. In APN'87. 1987. ( BibTeX )
-
A. Finkel. Blocage et vivacité dans les réseaux à pile-file. In STACS'84, LNCS 166, pages 151-162. Springer-Verlag, 1984. ( BibTeX )
-
A. Finkel. Control of a Petri net by a finite automaton. In FSTTCS'83. 1983. ( BibTeX )
-
A. Finkel and G. Memmi. Fifo nets: a new model of parallel computation. In Proceedings of the 6th GI-Conference on Theoretical Computer
Science, Dortmund, Germany, January 1983, LNCS 145, pages 111-121. Springer-Verlag, 1982. ( BibTeX )
-
A. Finkel. About monogeneous fifo Petri nets. In APN'82. 1982. ( BibTeX )
Other Publications
-
R. Saint Bauzel and A. Finkel. Se représenter pour mieux apprendre: les représentations
mentales comme outils didactiques favorisant la transmission du savoir. In SFP'11, pages 171-173. 2011. ( PDF | BibTeX )
-
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. ( PDF | BibTeX + Abstract )
-
P. Arnoux and A. Finkel. Using mental imagery processes for teaching/searching in
mathematics and computer science. In ICME'08. 2008. ( PDF | BibTeX + Abstract )
-
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. ( PDF | BibTeX + Abstract )
-
S. Bardin, A. Finkel, É. Lozes and A. Sangnier. From Pointer Systems to Counter Systems Using Shape Analysis. In AVIS'06. 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
-
S. Bardin, Ch. Darlot and A. Finkel. FAST: un model-checker pour systèmes à compteurs. In AFADL'04, pages 377-380. 2004. ( PS | PS.GZ | BibTeX + Abstract )
-
S. Bardin, A. Finkel and D. Nowak. Toward Symbolic Verification of Programs Handling Pointers. In AVIS'04. 2004. ( PS | PS.GZ | BibTeX + Abstract )
-
A. Finkel and J. Leroux. Acceleration of Loops for Verification, Invited talk, Workshop on Mathematical Models and Techniques for
Analysing Systems, Montréal, Canada, 2002. ( BibTeX )
-
A. Finkel and J. Leroux. A Finite Covering Tree for Analysing Entropic Broadcast Protocols. In VCL 2000. University of Southampton, Southampton, UK, 2000. ( PS | PS.GZ | BibTeX )
-
A. Finkel, P. McKenzie and C. Picaronny. A Well-Structured Framework for Analysing Petri Net Extensions. Research Report LSV-99-2, Laboratoire Spécification et Vérification, ENS Cachan,
France, February 1999. ( PS | PS.GZ | BibTeX )
-
Ch. Collet, A. Finkel and R. Gherbi. Prise en compte dynamique des attitudes perceptive de l'usager, Rapport de synthèse (version IV de l'Action Inter-PRC 10.2
GDR-PRC ISIS & CHM : « Interaction Système-Environnement pour
l'Interprétation des Signaux et des Images », 1997. ( BibTeX )
-
Ch. Collet, A. Finkel and R. Gherbi. CapRe : un système de capture du regard dans un contexte
d'interaction homme-machine. In Actes des 6èmes Journées Internationales Interfaces,
Montpellier, France, May 1997, pages 36-39. 1997. ( PS | PS.GZ | BibTeX )
-
A. Finkel. Algorithms and Semi-Algorithms for Infinite State Systems. In Proceedings of the Grenoble-Alpes d'Huez European School of
Computer Science, Methods and Tools for the Verification of
Infinite State Systems, Grenoble, France, March 1997, pages 189-190. 1997. Invited tutorial. ( BibTeX )
-
Z. Bouziane and A. Finkel. La vérification des réseaux de Petri réversibles est
primitive récursive. Internal Report 96-6, Laboratoire d'Informatique Fondamentale et Appliquée de Cachan,
ENS Cachan, France, June 1996. ( BibTeX )
-
A. Finkel and O. Marcé. Verification of Infinite Regular Communicating Automata. Internal Report 96-4, Laboratoire d'Informatique Fondamentale et Appliquée de Cachan,
ENS Cachan, France, April 1996. ( BibTeX )
-
C. Dufourd and A. Finkel. A Polynomial λ-Bisimilar Normalization for Petri Nets. Internal Report 96-1, Laboratoire d'Informatique Fondamentale et Appliquée de Cachan,
ENS Cachan, France, March 1996. ( BibTeX )
-
A. Finkel, P. McKenzie and C. Picaronny. Minimal Coverability Trees for High Level Nets. Internal Report 96-3, Laboratoire d'Informatique Fondamentale et Appliquée de Cachan,
ENS Cachan, France, March 1996. ( BibTeX )
-
A. Finkel and I. Tellier. Individual Regularities and Cognitive Automata. Internal Report 96-2, Laboratoire d'Informatique Fondamentale et Appliquée de Cachan,
ENS Cachan, France, March 1996. ( PDF | BibTeX )
-
A. Finkel and P. McKenzie. Verifying Identical Communicating Processes is Undecidable. In ICTCS'95, pages 307-322. World Scientific, 1995. ( BibTeX )
-
A. Finkel, O. Marcé and L. Petrucci. Un algorithme en n3/2 pour le problème de la borne des
bonnes places d'un réseau de Petri. In Actes du 4ème Colloque Francophone sur l'Ingénierie des
Protocoles, Rennes, France, May 1995, pages 401-418. Hermès, 1995. ( BibTeX )
-
A. Finkel, C. Johnen and L. Petrucci. Decomposition of Petri Nets for Parallel Analysis. Technical report, Laboratoire d'Informatique Fondamentale et Appliquée de Cachan,
ENS Cachan, France, 1992. ( BibTeX )