Université Libre de Bruxellesresearch 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).



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
Realtime 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 ComputerAided Verification , LNCS 2102, Paris, France, 2001. Copyright © SpringerVerlag. G. Delzanno, J.F. Raskin, L. Van Begin. 'Towards the Automated Verification of Multithreaded Java Programs' ,TACAS, 8th International Conference on Tools and Algorithms fo Construction and Analysis of Systems , LNCS 2280, Grenoble, France, 2002. Copyright © SpringerVerlag. 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 infinitestate 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 Nonblocking Arcs are Difficult to Analyse', INFINITY 2003, 5th international workshop on verification of infinitestate systems, Marseilles, France, 2003. Also appears in volume 98 of ENTCS, Elsevier, 2004. P. Ganty, L. Van Begin. NonDeterministic Automata for efficient Verification of InfiniteState 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 © SpringerVerlag. 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 wlanguage 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 ComputerAided Verification , LNCS 3576, Edinburgh, Scotland, 2005. Copyright © SpringerVerlag. 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 © SpringerVerlag. 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 © SpringerVerlag. 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 © SpringerVerlag. P.A. Abdulla, G. Delzanno, L. Van Begin. Comparing the Expressive Power of Wellstructured Transition Systems, CSL, 16th EACSL Annual Conference on Computer Science and Logic , LNCS 4646, Lausanne, Switzerland, 2007. Copyright © SpringerVerlag. G.Delzanno, L. Van Begin. On the Dynamics of PBsystems with Volatile Membranes, WMC, 8th Workshop on Membrane Computing, LNCS 4860, Thessaloniki, Greece, 2007. Copyright © SpringerVerlag. 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 © SpringerVerlag. P.A. Abdulla, G. Delzanno, L. Van Begin. On the qualitative analysis of conformons Psystems, WMC, 9th Workshop on Membrane Computing (BEST PAPER AWARD), will appear in LNCS, Edinburgh, Scotland, 2008. Copyright © SpringerVerlag. 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 © SpringerVerlag. P.A. Abdulla, G. Delzanno, L. Van Begin. A LanguageBased Comparison of Extended Petri Nets with and Without WholePlace Operations, LATA, 3rd Internatonal Conference on Language and Automata Theory and Applications, will appear in LNCS, Tarragona, Spain, 2009. Copyright © SpringerVerlag.  
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(23):268297, 2004. Copyright
© SpringerVerlag.
A. Finkel, G. Geeraerts, J.F. Rasking, L. Van Begin. On the wlanguage Expressive Power of Extended Petri nets, In journal of Theoretical Computer Science 356(3):374386, 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):180203,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. Wellstructured languages, In Acta Informatica 44(34): 249288, 2007. Copyright © SpringerVerlag. T. Massart, C. Meuter, L. Van Begin. On the complexity of the partial order trace model checking, In Information Processing Letters 106(3): 120126, 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 counterexample 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 kuples of integers, Technical Report 570, ULB 2006. 

Scientific Awards 
Prix IBM Belgium
d'informatique 2000. 

WinterSummer 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 UpperClosed 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 Multithreaded Java Programs",F.N.R.S. meeting on Theoretical Computer Science,Facultes Universitaires NotreDame 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. 