Université Libre de Bruxelles

research section

	Actual Research		My main interest is formal verification of properties on Petri Nets.
	M.S. Thesis		'Logiques Temporelles et Model Checking: Etude et Implantation.', Université Libre de Bruxelles, Belgium (1999). Summary (French). Master Thesis (French).
	D.E.A. Thesis in Sciences		'Attacking Symbolic State Explosion' , Université Libre de Bruxelles, Belgium (2001).
	Ph.D. Thesis		'Efficient Verification of Counting Abstractions for Parametric systems', Université Libre de Bruxelles, Belgium (2003).
	Conference Publications		T. Massart, L. Van Begin, E. Van Nuffel. 'Design of Timed Systems using a Real-time Process Algebra' ,PLS, 2nd Panhellenic logic symposium, Delphi,Greece, 1999. G. Delzanno, J.-F. Raskin, L. Van Begin. 'Attacking Symbolic State Explosion' ,CAV, 13th International Conference on Computer-Aided Verification , LNCS 2102, Paris, France, 2001. Copyright © Springer-Verlag. G. Delzanno, J.-F. Raskin, L. Van Begin. 'Towards the Automated Verification of Multi-threaded Java Programs' ,TACAS, 8th International Conference on Tools and Algorithms fo Construction and Analysis of Systems , LNCS 2280, Grenoble, France, 2002. Copyright © Springer-Verlag. P. Ammirati, G. Delzanno, P. Ganty, G. Geeraerts, J.-F. Raskin, L. Van Begin. 'Babylon: An integrated toolkit for the specification and verification of parameterized systems' ,SAVE, 2nd workshop on Specification, Analysis and Validation for Emerging technologies , Copenhagen, Denmark, 2002. A.Finkel, J.-F. Raskin, M. Samuelides, L. Van Begin. 'Monotonic Extensisions of Petri Nets : Forward and Backward Search Revisited', INFINITY, 4th international workshop on verification of infinite-state systems, ,Brno, Czech Republic, 2002. Also appears in volume 68(6) of ENTCS, Elsevier, 2003. T. Massart, J.-F. Raskin, L. Van Begin. 'Symbolic Distributed Verification of a Class of Parametric Concurrent Systems', PDMC, 1st workshop on Parallel and Distributed Model Checking, Brno, Czech Republic, 2002. J.-F. Raskin, L. Van Begin. 'Petri Nets with Non-blocking Arcs are Difficult to Analyse', INFINITY 2003, 5th international workshop on verification of infinite-state systems, Marseilles, France, 2003. Also appears in volume 98 of ENTCS, Elsevier, 2004. P. Ganty, L. Van Begin. Non-Deterministic Automata for efficient Verification of Infinite-State Systems(abstract), CP+CV, international workshop on Constraint Programming and Constraint Verification, Barcelona, Spain, 2004. G. Geeraerts, J.-F. Raskin, L. Van Begin. Expand, Enlarge and Check: New Algorithms for the coverability problem of WSTS, FSTTCS, 24th International Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 3328, Chennai, India, 2004. Copyright © Springer-Verlag. Also presented to Journées montoises d'informatique théorique 2004. J.-F. Raskin, M. Samuelides, L. Van Begin. Games for Counting Abstractions, AVoCS, 4th international workshop on Automated Verification of Critical Systems, London, Great Britain, 2004. Also appear in volume 128(6) of ENTCS, Elsevier, 2005. A. Finkel, G. Geeraerts, J.-F. Raskin, L. Van Begin. On the w-language Expressive Power of Extended Petri nets, EXPRESS, 11th international workshop on Expressiveness in Concurrency, London, Great Britain, 2004. Also appear in volume 128(2) of ENTCS, Elsevier, 2005. C. Darlot, A. Finkel, L. Van Begin. About FAST and TReX Accelerations, AVoCS, 4th international workshop on Automated Verification of Critical Systems, London, Great Britain, 2004. Also appear in volume 128(6) of ENTCS, Elsevier, 2005. G. Geeraerts, J.-F. Raskin, L. Van Begin. Expand, Enlarge and Check...Made Efficient, CAV, 17th International Conference on Computer-Aided Verification , LNCS 3576, Edinburgh, Scotland, 2005. Copyright © Springer-Verlag. P.Ganty, J.-F. Raskin, L. Van Begin. A Complete Abstract Interpretation Framework for Coverability Properties of WSTS, VMCAI, 7th International Conference on Verification, Model Checking and Abstract Interpretation , LNCS 3855, Charleston, USA, 2006. Copyright © Springer-Verlag. P. Ganty, J.-F. Raskin, L. Van Begin. From Many Places to Few: Automatic Abstraction Refinement for Petri Nets, ATPN, 28th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, LNCS 4546, Siedlce, Poland, 2007. Copyright © Springer-Verlag. G. Kalyon, T. Massart, C. Meuter, L. Van Begin. Testing Distributed Systems through Symbolic Model Checking of Traces, FORTE, 27th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems (BEST PAPER AWARD), LNCS 4574, Tallinn, Estonia, 2007.Copyright © Springer-Verlag. P.A. Abdulla, G. Delzanno, L. Van Begin. Comparing the Expressive Power of Well-structured Transition Systems, CSL, 16th EACSL Annual Conference on Computer Science and Logic , LNCS 4646, Lausanne, Switzerland, 2007. Copyright © Springer-Verlag. G.Delzanno, L. Van Begin. On the Dynamics of PB-systems with Volatile Membranes, WMC, 8th Workshop on Membrane Computing, LNCS 4860, Thessaloniki, Greece, 2007. Copyright © Springer-Verlag. G. Geeraerts, J.-F. Raskin, L. Van Begin On the Efficient Computation of the Minimal Coverability set of Petri Nets, ATVA, 5th International Symposium on Automated Technology for Verification and Analysis, LNCS 4762, Tokyo, Japan, 2007. Copyright © Springer-Verlag. P.A. Abdulla, G. Delzanno, L. Van Begin. On the qualitative analysis of conformons P-systems, WMC, 9th Workshop on Membrane Computing (BEST PAPER AWARD), will appear in LNCS, Edinburgh, Scotland, 2008. Copyright © Springer-Verlag. G. Delzanno, L. Van Begin. A biologically inspired model with fusion and clonation of membranes, UC, 7th International Conference on Unconventional Computing, LNCS 5204, Vienna, Austria, 2008. Copyright © Springer-Verlag. P.A. Abdulla, G. Delzanno, L. Van Begin. A Language-Based Comparison of Extended Petri Nets with and Without Whole-Place Operations, LATA, 3rd Internatonal Conference on Language and Automata Theory and Applications, will appear in LNCS, Tarragona, Spain, 2009. Copyright © Springer-Verlag.
	Journal Publications		G.Delzanno, J.-F. Raskin, L. Van Begin. CSTs (Covering Sharing Trees): compact Data Structures for Parameterized Verification, In Software Tools for Technology Transfer manuscript 5(2-3):268-297, 2004. Copyright © Springer-Verlag. A. Finkel, G. Geeraerts, J.-F. Rasking, L. Van Begin. On the w-language Expressive Power of Extended Petri nets, In journal of Theoretical Computer Science 356(3):374-386, 2006. G. Geeraerts, J.-F. Raskin, L. Van Begin. Expand, Enlarge and Check: New Algorithms for the coverability problem of WSTS, In journal of Computer and System Sciences 72(1):180-203,2006. R. Devillers, L. Van Begin. Boundedness undecidability for synchronized nets, In Information Processing Letters 99, 2006. G. Geeraerts, J.-F. Raskin, L. Van Begin. Well-structured languages, In Acta Informatica 44(3-4): 249-288, 2007. Copyright © Springer-Verlag. T. Massart, C. Meuter, L. Van Begin. On the complexity of the partial order trace model checking, In Information Processing Letters 106(3): 120-126, 2008. P. Ganty, J.-F. Raskin, L. Van Begin. From many places to few: automatic abstraction refinement for Petri nets, will appear in Fundamenta Informaticae, 2008. P. Ganty, G. Geeraerts, J.-F. Raskin, L. Van Begin. Le problème de couverture pour les réseaux de Petri: résultats classiques et développements récents (in French), accepted for publication in Technique et Science Informatique, 2008. G. Geeraerts, J.-F. Raskin, L. Van Begin. On the computation of the minimal coverability set of Petri nets, submitted to the International Journal of Fondations of Computer Science, 2008.
	Other Publications		G. Geerearts, L. Van Begin. Concurrent Boolean Programs, Technical Report 505, ULB 2003. J.-F. Raskin, M. Samuelides, L. Van Begin. Petri games are Monotonic but difficult to decide, Technical Report 508, ULB 2003. A. Finkel, G. Geeraerts, J.-F. Raskin, L. Van Begin. A counter-example to the minimal coverability tree algorithm, Technical Report 535, ULB 2005. P. Ganty, G. Delzanno, G. Kalyon, C. Meuter, J.-F. Raskin, L. Van Begin. Symbolic Data Structure for sets of k-uples of integers, Technical Report 570, ULB 2006.
	Scientific Awards		Prix IBM Belgium d'informatique 2000.
	Winter-Summer School		MOVEP'2k in Nantes from 19 to 23 june 2000. 21st International Summer School Markoberdorf in Markoberdork from july 25 to August 5 2000. MOVEP 2004 in Brussels from 13 to 17 december 2004.
	Project		Babylon project.
	Practical Contribution		The IST library (available on request to pganty[at]ulb.ac.be).
	Talks		"Logiques Temporelles et Model Checking: Etude et Implantation",F.N.R.S. awards, Bruxelles, Belgium,23 october 2000. "Efficient Verification of Upper-Closed Properties of a Class of Infinite State Systems",F.N.R.S. meeting on Theoretical Computer Science,Universite Libre de Bruxelles, Bruxelles, Belgium, 6 june 2001. "Towards the Automated Verification of Multi-threaded Java Programs",F.N.R.S. meeting on Theoretical Computer Science,Facultes Universitaires Notre-Dame de la Paix,Namur, Belgium, 22 may 2002.
	Collaborators		Prof. Th. Massart Prof. J.-F. Raskin Prof. G. Delzanno Prof. A. Finkel The Formal Methods and Verification Group at ULB C.F.V.

Université Libre de Bruxelles - Last modification: 06 June 2008.
Comments: lvbegin@ulb.ac.be.

This page has been created with the vi editor