Publications : Alain FINKEL

[FP19]
A. Finkel and M. Praveen. Verification of Flat FIFO Systems. In Proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19), Leibniz International Proceedings in Informatics, Amsterdam, The Netherlands, August 2019. Leibniz-Zentrum für Informatik. To appear.
BibTex ]
[FHK19]
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 ]
[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), 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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[Fin17]
A. Finkel. L'analyse cognitive, la psychologie numérique et la formation des enseignants à l'université. Pratiques Psychologiques, 23(3):303--323, 2017.
doi: https://doi.org/10.1016/j.prps.2017.05.006.
BibTex | DOI | Web page | 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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[Fin14]
A. Finkel. REACHARD -- Compte-rendu intermédiaire. Deliverable D3 Reachard (ANR-11-BS02-001), February 2014. 18 pages.
BibTex ]
[CFM13]
M. Cadilhac, A. Finkel, and P. McKenzie. Unambiguous Contrained Automata. International Journal of Foundations of Computer Science, 24(7):1099--1116, November 2013.
doi: 10.1142/S0129054113400339.
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 ]
[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 ]
[Fin13]
A. Finkel. REACHARD -- Compte-rendu intermédiaire. Deliverable D2 Reachard (ANR-11-BS02-001), March 2013. 9 pages.
BibTex ]
[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 ]
[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 ]
[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 ]
[SF12]
R. Saint Bauzel and A. Finkel. Qu'est-ce qu'une représentation efficace pour favoriser les apprentissages ? In Actes du 54ème Congrès National de la Société Française de Psychologie (SFP'12), pages 89--91, Montpellier, France, September 2012.
BibTex | 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 ]
[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 ]
[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 ]
[SF11]
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 Actes du 53ème Congrès National de la Société Française de Psychologie (SFP'11), pages 171--173, Metz, 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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[AF10]
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):229--242, January 2010.
doi: 10.1080/00207390903372429.
BibTex | DOI | Web page | 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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[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 ]
[AF08]
P. Arnoux and A. Finkel. Using mental imagery processes for teaching/searching in mathematics and computer science. In Proceedings of the 11th International Congress on Mathematical Education (ICME'08), Monterrey, Mexico, July 2008.
BibTex | 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 ]
[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 ]
[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 ]
[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 ]
[CF05]
G. Cécé and A. Finkel. Verification of Programs with Half-Duplex Communication. Information and Computation, 202(2):166--190, November 2005.
doi: 10.1016/j.ic.2005.05.006.
BibTex | DOI | Web page | PDF ]
[FL05]
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):30--35, October 2005.
doi: 10.1016/j.ipl.2005.04.004.
BibTex | DOI | Web page | PS | PDF ]
[BFLS05]
S. Bardin, A. Finkel, J. Leroux, and Ph. Schnoebelen. Flat acceleration in symbolic model checking. In Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 474--488, Taipei, Taiwan, October 2005. Springer.
doi: 10.1007/11562948_35.
BibTex | DOI | Web page | PS | PDF ]
[DFV05]
Ch. Darlot, A. Finkel, and L. Van Begin. About Fast and TReX Accelerations. In Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 87--103, London, UK, May 2005. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2005.04.006.
BibTex | DOI | Web page | PDF ]
[FGRV05b]
A. Finkel, G. Geeraerts, J.-F. Raskin, and L. Van Begin. On the Omega-Language Expressive Power of Extended Petri Nets. In Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 87--101, London, UK, April 2005. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2004.11.030.
BibTex | DOI | Web page | PDF ]
[FGRV05a]
A. Finkel, G. Geeraerts, J.-F. Raskin, and L. Van Begin. A counter-example the the minimal coverability tree algorithm. Technical Report 535, Université Libre de Bruxelles, Belgium, 2005.
BibTex | Web page | PDF ]
[FMP04]
A. Finkel, P. McKenzie, and C. Picaronny. A Well-Structured Framework for Analysing Petri Net Extensions. Information and Computation, 195(1-2):1--29, November 2004.
doi: 10.1016/j.ic.2004.01.005.
BibTex | DOI | Web page | PS ]
[BF04]
S. Bardin and A. Finkel. Composition of accelerations to verify infinite heterogeneous systems. In Proceedings of the 2nd International Symposium on Automated Technology for Verification and Analysis (ATVA'04), volume 3299 of Lecture Notes in Computer Science, pages 248--262, Taipei, Taiwan, October-November 2004. Springer.
BibTex | Web page | PS ]
[FL04a]
A. Finkel and J. Leroux. Image Computation in Infinite State Model Checking. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of Lecture Notes in Computer Science, pages 361--371, Boston, Massachusetts, USA, July 2004. Springer.
BibTex | Web page | PS ]
[BDF04a]
S. Bardin, Ch. Darlot, and A. Finkel. FAST: un model-checker pour systèmes à compteurs. In Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), pages 377--380, Besançon, France, June 2004.
BibTex | Web page | PS ]
[BDF+04b]
S. Bardin, Ch. Darlot, A. Finkel, J. Leroux, and L. Van Begin. FAST v1.5: Fast Acceleration of Symbolic Transition Systems. Available at http://www.lsv.ens-cachan.fr/fast/, June 2004.
BibTex | Web page ]
[BFN04]
S. Bardin, A. Finkel, and D. Nowak. Toward Symbolic Verification of Programs Handling Pointers. In Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Barcelona, Spain, April 2004.
BibTex | Web page | PS ]
[FL04b]
A. Finkel and J. Leroux. Polynomial Time Image Computation With Interval-Definable Counters Systems. In Proceedings of the 11th International SPIN Workshop on Model Checking Software (SPIN'04), volume 2989 of Lecture Notes in Computer Science, pages 182--197, Barcelona, Spain, April 2004. Springer.
BibTex | Web page | PS ]
[BFL04]
S. Bardin, A. Finkel, and J. Leroux. FASTer Acceleration of Counter Automata in Practice. In Proceedings of the 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 576--590, Barcelona, Spain, March 2004. Springer.
BibTex | Web page | PS ]
[BFN03b]
S. Bardin, A. Finkel, and D. Nowak. Rapport final. Contract Report P11L03/F01304/0 + 50.0241, collaboration entre EDF et le LSV, November 2003. 50 pages.
BibTex ]
[BFN03a]
S. Bardin, A. Finkel, and D. Nowak. Note de synthèse à 10 mois. Contract Report P11L03/F01304/0 + 50.0241, collaboration entre EDF et le LSV, August 2003. 21 pages.
BibTex ]
[BFL+03b]
S. Bardin, A. Finkel, J. Leroux, L. Petrucci, and L. Worobel. FAST User's Manual, August 2003. 33 pages.
BibTex | Web page | PS ]
[BFNS03]
S. Bardin, A. Finkel, D. Nowak, and Ph. Schnoebelen. Note de synthèse à 6 mois. Contract Report P11L03/F01304/0 + 50.0241, collaboration entre EDF et le LSV, July 2003. 43 pages.
BibTex ]
[BFLP03]
S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Fast Acceleration of Symbolic Transition Systems. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV'03), volume 2725 of Lecture Notes in Computer Science, pages 118--121, Boulder, Colorado, USA, July 2003. Springer.
BibTex | Web page | PS ]
[BFL03a]
S. Bardin, A. Finkel, and J. Leroux. FAST v1.0: Fast Acceleration of Symbolic Transition Systems, July 2003. See [BFLP03] for description. Written in C++ (about 4400 lines on top of the MONA v1.4 library).
BibTex | Web page ]
[FPS03]
A. Finkel, S. Purushothaman Iyer, and G. Sutre. Well-Abstracted Transition Systems: Application to FIFO Automata. Information and Computation, 181(1):1--31, February 2003.
BibTex | Web page | PS ]
[FL02b]
A. Finkel and J. Leroux. How To Compose Presburger-Accelerations: Applications to Broadcast Protocols. In Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02), volume 2556 of Lecture Notes in Computer Science, pages 145--156, Kanpur, India, December 2002. Springer.
BibTex | Web page | PS ]
[FL02a]
A. Finkel and J. Leroux. Acceleration of Loops for Verification. Invited talk, Workshop on Mathematical Models and Techniques for Analysing Systems, Montréal, Canada, October 2002.
BibTex ]
[FRSV02]
A. Finkel, J.-F. Raskin, M. Samuelides, and L. Van Begin. Monotonic Extensions of Petri Nets: Forward and Backward Search Revisited. In Proceedings of the 4th International Workshop on Verification of Infinite State Systems (INFINITY'02), volume 68 of Electronic Notes in Theoretical Computer Science, pages 121--144, Brno, Czech Republic, August 2002. Elsevier Science Publishers.
BibTex | Web page | PS ]
[HCF+02]
F. Herbreteau, F. Cassez, A. Finkel, O. F. Roux, and G. Sutre. Verification of Embedded Reactive Fiffo Systems. In Proceedings of the 5th Latin American Symposium on Theoretical Informatics (LATIN'02), volume 2286 of Lecture Notes in Computer Science, pages 400--414, Cancun, Mexico, April 2002. Springer.
BibTex | Web page | PS ]
[FS01]
A. Finkel and Ph. Schnoebelen. Well-Structured Transition Systems Everywhere! Theoretical Computer Science, 256(1-2):63--92, April 2001.
doi: 10.1016/S0304-3975(00)00102-X.
BibTex | DOI | Web page | PS | PDF ]
[BBF+01]
B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and Ph. Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.
BibTex | Web page ]
[FPS00]
A. Finkel, S. Purushothaman Iyer, and G. Sutre. Well-Abstracted Transition Systems. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000), volume 1877 of Lecture Notes in Computer Science, pages 566--580, Pennsylvania State University, Pennsylvania, USA, August 2000. Springer.
BibTex | Web page | PS ]
[FS00a]
A. Finkel and G. Sutre. An Algorithm Constructing the Semilinear Post* for 2-Dim ResetashTransfer VASS. In Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS 2000), volume 1893 of Lecture Notes in Computer Science, pages 353--362, Bratislava, Slovakia, August 2000. Springer.
BibTex | Web page | PS ]
[FL00]
A. Finkel and J. Leroux. A Finite Covering Tree for Analysing Entropic Broadcast Protocols. In Proceedings of the International Workshop on Verification and Computational Logic (VCL 2000), London, UK, July 2000. University of Southampton, Southampton, UK.
BibTex | Web page | PS ]
[BEF+00]
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):221--227, June 2000.
BibTex | Web page | PS ]
[FS00b]
A. Finkel and G. Sutre. Decidability of Reachability Problems for Classes of Two-Counter Automata. In Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science (STACS 2000), volume 1770 of Lecture Notes in Computer Science, pages 346--357, Lille, France, February 2000. Springer.
doi: 10.1007/3-540-46541-3_29.
BibTex | DOI | Web page | PS ]
[DF99]
C. Dufourd and A. Finkel. A Polynomial λ-Bisimilar Normalization for Reset Petri Nets. Theoretical Computer Science, 222(1-2):187--194, July 1999.
BibTex | Web page | PS ]
[EFM99]
J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS'99), pages 352--359, Trento, Italy, July 1999. IEEE Computer Society Press.
BibTex | Web page | PS ]
[FMP99]
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.
BibTex | Web page | PS ]
[SFRC99]
G. Sutre, A. Finkel, O. F. Roux, and F. Cassez. Effective Recognizability and Model Checking of Reactive Fiffo Automata. In Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST'98), volume 1548 of Lecture Notes in Computer Science, pages 106--123, Amazonia, Brasil, January 1999. Springer.
BibTex | Web page | PS ]
[CDF98]
G. Cécé, P.-É. Deutsch, and A. Finkel. FORMAashSSCOP --- LSV, bilan de l'année 1998. Contract report, FORMA, November 1998.
BibTex ]
[BCD+98]
B. Bérard, G. Cécé, C. Dufourd, A. Finkel, F. Laroussinie, A. Petit, Ph. Schnoebelen, and G. Sutre. Le model-checking, une technique de vérification en plein essor. II --- Quelques outils. Contract report, EDF/DER/MOS - LSV, October 1998.
BibTex ]
[Fin98]
A. Finkel. Analyse des systèmes infinis bien structurés ou << reconnaissables >>. Invited tutorial, 3ème École d'été Modélisation et Vérification des Processus Parallèles (MOVEP'98), Nantes, France, July 1998.
BibTex ]
[DFS98]
C. Dufourd, A. Finkel, and Ph. Schnoebelen. Reset Nets between Decidability and Undecidability. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP'98), volume 1443 of Lecture Notes in Computer Science, pages 103--115, Aalborg, Denmark, July 1998. Springer.
doi: 10.1007/BFb0055044.
BibTex | DOI | Web page | PS ]
[FS98]
A. Finkel and Ph. Schnoebelen. Fundamental Structures in Well-Structured Infinite Transition Systems. In Proceedings of the 3rd Latin American Symposium on Theoretical Informatics (LATIN'98), volume 1380 of Lecture Notes in Computer Science, pages 102--118, Campinas, Brasil, April 1998. Springer.
doi: 10.1007/BFb0054314.
BibTex | DOI | Web page | PS ]
[FT98]
A. Finkel and I. Tellier. From Natural Language to Cognitive Style. In Proceedings of the 4th International Colloquium on Cognitive Science (ICCS'95), pages 271--279, Donostia, San Sebastian, Spain, 1998. Kluwer Academic Publishers.
BibTex | Web page | PDF ]
[BF98]
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, pages 63--76, Kunming, China, 1998. Springer.
BibTex ]
[CFG98]
Ch. Collet, A. Finkel, and R. Gherbi. CapRe: A Gaze Tracking System in Man-Machine Interaction. Journal of Advanced Computational Intelligence, 2(3):77--81, 1998.
BibTex | Web page | PS ]
[DF97]
C. Dufourd and A. Finkel. Polynomial-Time Many-One Reductions for Petri Nets. In Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'97), volume 1346 of Lecture Notes in Computer Science, pages 312--326, Kharagpur, India, December 1997. Springer.
BibTex | Web page | PS | PDF ]
[CFG97b]
Ch. Collet, A. Finkel, and R. Gherbi. Gaze Capture System in Man-Machine Interaction. In Proceedings of the IEEE International Conference on Intelligent Engineering Systems (INES'97), pages 557--581, Budapest, Hungary, September 1997. IEEE Press.
BibTex | Web page | PS | PDF ]
[FWW97]
A. Finkel, B. Willems, and P. Wolper. A Direct Symbolic Approach to Model Checking Pushdown Systems (Extended Abstract). In Proceedings of the 2nd International Workshop on Verification of Infinite State Systems (INFINITY'97), volume 9 of Electronic Notes in Theoretical Computer Science, pages 27--39, Bologna, Italy, July 1997. Elsevier Science Publishers.
BibTex | Web page | PS | PDF ]
[BF97]
Z. Bouziane and A. Finkel. Cyclic Petri Net Reachability Sets are Semi-Linear Effectively Constructible. In Proceedings of the 2nd International Workshop on Verification of Infinite State Systems (INFINITY'97), volume 9 of Electronic Notes in Theoretical Computer Science, pages 15--24, Bologna, Italy, July 1997. Elsevier Science Publishers.
BibTex | Web page | PS | PDF ]
[CF97]
G. Cécé and A. Finkel. Programs with Quasi-Stable Channels are Effectively Recognizable. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), volume 1254 of Lecture Notes in Computer Science, pages 304--315, Haifa, Israel, June 1997. Springer.
BibTex | Web page | PS | PDF ]
[CFG97a]
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, pages 36--39, Montpellier, France, May 1997.
BibTex | Web page | PS | PDF ]
[Fin97]
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, pages 189--190, Grenoble, France, March 1997. Invited tutorial.
BibTex ]
[FM97]
A. Finkel and P. McKenzie. Verifying Identical Communicating Processes is Undecidable. Theoretical Computer Science, 174(1-2):217--230, March 1997.
BibTex | Web page | PS | PDF ]
[CFG97c]
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 ]
[FT96c]
A. Finkel and I. Tellier. A Polynomial Algorithm for the Membership Problem with Categorial Grammars. Theoretical Computer Science, 164(1-2):207--221, September 1996.
BibTex | Web page | PDF ]
[BF96]
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 ]
[FM96]
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 ]
[FT96b]
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.
BibTex | Web page | PDF ]
[FMP96]
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 ]
[DF96]
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 ]
[FT96a]
A. Finkel and I. Tellier. The Cognitive Style of Decision Making Narrations. In The Cognitive Level: Language and Mind Modelized, volume 273 of Duisburg L.A.U.D. Symposium, Series B: Applied and Interdisciplinary Papers, pages 41--59, 1996.
BibTex | Web page | PDF ]
[CFP96]
G. Cécé, A. Finkel, and S. Purushothaman Iyer. Unreliable Channels are Easier to Verify than Perfect Channels. Information and Computation, 124(1):20--31, January 1996.
BibTex | Web page | PS ]
[FM95]
A. Finkel and P. McKenzie. Verifying Identical Communicating Processes is Undecidable. In Proceedings of the 5th Italian Conference on Theoretical Computer Science (ICTCS'95), pages 307--322, Ravello, Italy, November 1995. World Scientific.
BibTex ]
[FMP95]
A. Finkel, O. Marcé, and L. Petrucci. Un algorithme en n^3/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, pages 401--418, Rennes, France, May 1995. Hermès.
BibTex ]
[CFP94]
G. Cécé, A. Finkel, and S. Purushothaman Iyer. Duplication, Insertion and Lossiness Errors in Unreliable Communication Channels. In Proceedings of the 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering (SIGSOFT FSE'94), volume 19 of ACM SIGSOFT Software Engineering Notes, pages 35--43, New Orleans, Louisiana, USA, December 1994.
BibTex ]
[FT94]
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.
BibTex ]
[Fin94]
A. Finkel. Decidability of the Termination Problem for Completely Specified Protocols. Distributed Computing, 7(3):129--135, 1994.
doi: 10.1007/BF02277857.
BibTex | DOI ]
[FP94]
A. Finkel and L. Petrucci. Propriétés de la compositionash décomposition de réseaux de Petri et de leurs graphes de couverture. RAIRO Informatique Théorique et Applications, 28(2):73--124, 1994.
BibTex ]
[Fin93]
A. Finkel. The Minimal Coverability Graph for Petri Nets. In Papers from the 12th International Conference on Applications and Theory of Petri Nets (APN'91), volume 674 of Lecture Notes in Computer Science, pages 210--243, Gjern, Denmark, 1993. Springer-Verlag.
BibTex ]
[FJP92]
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 ]
[FP92]
A. Finkel and L. Petrucci. Avoiding State Explosion by Composition of Minimal Covering Graphs. In Proceedings of the 3rd International Workshop on Computer Aided Verification (CAV'91), volume 575 of Lecture Notes in Computer Science, pages 169--180, Aalborg, Denmark, 1992. Springer-Verlag.
BibTex ]
[BFJP90]
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:6--7, April 1990.
BibTex ]
[Fin90]
A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89(2):144--179, 1990.
BibTex ]
[BF88]
G. Bochmann and A. Finkel. Impact of queued interaction on protocol specification and verification. In Proceedings of the 2nd International Symposium on Interoperable Information Systems (ISIIS'88), Tokyo, Japan, November 1988. IOS Press.
BibTex ]
[Fin88]
A. Finkel. A new class of analysable CFSMs with unbounded FIFO channels. In Proceedings of the IFIP WG6.1 8th International Conference on Protocol Specification, Testing and Verification (PSTV'88), Atlantic City, New Jersey, USA, June 1988. North-Holland.
BibTex ]
[FR88]
A. Finkel and L. Rosier. A Survey on the Decidability Questions for Classes of FIFO Nets. In Advances in Petri Nets 1988, Selected Papers from the 8th International Conference on Applications and Theory of Petri Nets (APN'87), volume 340 of Lecture Notes in Computer Science, pages 106--132, Zaragoza, Spain, 1988. Springer-Verlag.
BibTex ]
[Fin87]
A. Finkel. A generalization of the procedure of Karp and Miller to well structured transition system. In Proceedings of the 14th International Colloquium on Automata, Languages and Programming (ICALP'87), volume 267 of Lecture Notes in Computer Science, pages 499--508, Karlsruhe, Germany, July 1987. Springer-Verlag.
BibTex | Web page | PDF ]
[FC87b]
A. Finkel and A. Choquet. Simulation of linear fifo nets by Petri nets having a structured set of terminal markings. In Proceedings of the 8th International Conference on Applications and Theory of Petri Nets (APN'87), Zaragoza, Spain, June 1987.
BibTex ]
[FC87a]
A. Finkel and A. Choquet. Fifo nets without order deadlock. Acta Informatica, 25:15--36, 1987.
BibTex ]
[FM85]
A. Finkel and G. Memmi. An introduction to Fifo nets -- monogeneous nets: a subclass of Fifo nets. Theoretical Computer Science, 35:191--214, 1985.
BibTex ]
[Fin85]
A. Finkel. Une généralisation des théorèmes de Higman et de Simon aux mots infinis. Theoretical Computer Science, 38:137--142, 1985.
BibTex ]
[Fin84]
A. Finkel. Blocage et vivacité dans les réseaux à pile-file. In Proceedings of the 1st Annual Symposium on Theoretical Aspects of Computer Science (STACS'84), volume 166 of Lecture Notes in Computer Science, pages 151--162, Paris, France, April 1984. Springer-Verlag.
BibTex ]
[Fin83]
A. Finkel. Control of a Petri net by a finite automaton. In Proceedings of the 3rd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'83), Bangalore, India, December 1983.
BibTex ]
[Fin82]
A. Finkel. About monogeneous fifo Petri nets. In Proceedings of the 3rd International Conference on Applications and Theory of Petri Nets (APN'82), Varenna, Italy, September 1982.
BibTex ]
[FM82]
A. Finkel and G. Memmi. Fifo nets: a new model of parallel computation. In Proceedings of the 6th GI-Conference on Theoretical Computer Science, volume 145 of Lecture Notes in Computer Science, pages 111--121, Dortmund, Germany, 1982. Springer-Verlag.
BibTex ]

This file was generated by bibtex2html 1.98.

About LSV