Formal Methods and Verification at ULB   Computer Science Department at ULB  

Jean-Francois Raskin

Professor of Computer Science at ULB
PhD FUNDP 1999 (Belgium)



Recipient of an ERC Stg Grant in 2011


Email: jraskin [at] ulb [dot] ac [dot] be
SnailMail: ULB - Campus de la Plaine, CP212 - 1050 Bruxelles - Belgium
Tel: +32 2 650 55 92
Fax: +32 2 650 56 09

Several open positions: see project inVEST.

>>> The Formal Methods and Verification Group at ULB <<<
>>>Centre Fédéré en Vérification <<<
>>>Computer Science Seminars <<<

Recent Past Events :

HSCC'11, Chicago, PC Member.
STACS'11, Dortmund, PC Member.
MSR'11, Lille, PC Member.
ACSD'11, Kanazawa, PC Member.
iWIGP'11, Saarbrucken, PC Member.
GandALF 2011, Amalfi Coast, PC Member.
FORMATS'11, Aalborg, PC Member.
Reachability Worshop 2011, Genova, Invited Speaker.
Journées FAC 2011, Toulouse, Invited Speaker.
IEEE/IFIP IC on Embedded and Ubiquitous Computing, Australia. PC Member.
Dutch Model-Checking Day, Delft, The Netherlands, June 17, 2011. Invited Speaker.
IEEE SIES'11, Västeras Sweden, June 15. Keynote Speaker.

Upcoming Events :

MSR'11, Lille, Invited Speaker.
Formal Methods 2012, Paris, PC Member.
iWIGP'12, Talin, PC Member.
CONCUR'12, Newcastle, PC Member.
RP'12, Bordeaux, PC Member.
Journées Nationales GDR Math-Info, Paris, Invited Speaker.
LSV 15th anniversary, Cachan, Invited Speaker.
GASICS Workshop, Newcastle, Organizer.

ShortCV -- Projects -- Collaborations-- Publications -- Teaching


 
Short Curriculum Vitae

Jean-François Raskin was born in Belgium, in 1972. He received his master and Ph.D. degrees in computer science from the Université de Namur, Belgium, in june 1995 and april 1999, respectively. From 1995 to 1999, he was a Research Associate (aspirant) of the Belgian National Fund for Scientific Research (FNRS), Université de Namur, Belgium.  He worked on the decidability,complexity and expressiveness of formalisms for reasoning about real-time systems.

After several research stays at the University of California at Berkeley, Max-Planck Institute for Computer Science (Saarbrücken), and ENS Paris, he is now a Professor of computer science at the Université Libre de Bruxelles (ULB), Belgium. His research interests are the formal methods for the verification and synthesis of concurrent, real-time, and hybrid systems. His main research interests are:

    • Logic formalisms, especially temporal logics and real-time logics;
    • Automata formalisms and their extensions for real-time and hybrid systems;
    • Abstract interpretation theory and its application to the verification of concurrent, real-time and hybrid systems;
    • Game theory for synthesis of controllers.
For more details about his research, see the page of the group for Formal Methods and Verificiation at ULB.

At the ULB, he teaches subjects in theoretical computer science : logic in computer science, computability and complexity, and computer aided verification. He is also the secretary of the Belgian F.N.R.S. contact group on Theoretical Computer Science.

>> You can also download here a more complete CV.<<
 

Projects

  PAI-Moves




Recent past


Team

Current PhD Students

Marc Ducobu (co-supervision V. Bruyère)

Mikael Randour (co-supervision V. Bruyère)

Aaron Bohy (co-supervision V. Bruyère)

Current Post-Doc Students

Alexander Heussner

Emmanuel Filiot

Current Visitors
Line Juhl (March-May 2011)

Raffaella Gentilini (March-May 2011)

Former PhD Students

Steve Kremer, Formal Analysis of Optimistic Fair Exchange Protocols. December 2003. (Now permanent INRIA researcher at LSV-Cachan)

Laurent Van Begin, Efficient Verification of Counting Abstractions for Parametric Systems. December 2003. (Now at AtosWorldwide)

Laurent Doyen. Algorithmic Analysis of Complex Semantics for Timed and Hybrid Systems. June 2006. (Now permanent CNRS researcher at LSV-Cachan)

Martin De Wulf. From Timed Models to Timed Implementations. December 2006. (Now IT Manager at "My media is rich")

Pierre Ganty. The Fixpoint Checking Problem: an Abstraction Refinement Perspective. September 2007. (Now assistant Professor at IMDEA, Madrid)

Gilles Geeraerts. Coverability and Expressiveness Properties of Well Structured Transition Systems. March 2007. (Now Assistant Professor at ULB)

Nicolas Maquet. New algorithm and Data structures for the Emptiness of Alternating Automata. March 2011. (Now starting his own company)

Frédéric Servais. Visibly Pushdown Transducers. September 2011. (Now Post-Doc in U Hasselt)

Former Post-Doc Students

Nicolas Markey (Now permanent CNRS researcher at LSV-ENS Cachan).

Sébastien Bardin (Now at CEA Saclay, France).

Pierre-Alain Reynier (Now Assistant Professor at Université de Marseille).

Raffaella Gentilini (Now Assitant Professor at University of Perugia).

Naiyong Jin (Now Researcher at Synopsys Shanghai)

Nathalie Snjazder (Now Assistant Professor at U Paris 6)

Aldric Degorre (Now Assistant Professor at U Paris 7)

Tristan Legal (Now at CEA Saclay, France).

 

Collaborations

Our research group has collaborations with the following groups:


Main publications
My DBLP page
Google Scholar me

PDF of my (recent) papers can be downloaded here

Please email me if you do not find the one you want !

    2011

  • Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. Quantitative Languages Defined by Functional Automata. Submitted for publication. 26 pages. 2011
  • Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jin Nayong, and Jean-François Raskin. Acacia+, a Tool for LTL Synthesis. Submitted for publication. 6 pages. 2011.
  • Jean-François Raskin. Reachability problems for hybrid automata. In RP'11, LNCS 6945, Springer, pp. 28-30,  2011.
  • Gilles Geeraerts, Nathalie Snaider, and Jean-François Raskin. Event clock automata: from theory to practice. In FORMATS'11, LNCS 6919, Springer, pp.209-224, 2011.
  • Thomas Brihaye, Véronique Bruyère, Laurent Doyen, Marc Ducobu, and Jean-François Raskin. Antichain-based QBF Solving. In ATVA'11, LNCS 6996, Springer, pp.183-197, 2011.
  • Lubos Brim, Jakub Chaloupka, Laurent Doyen, Rafaella Gentilini, and Jean-François Raskin. Faster Algorithms for Mean-Payoff Games. In Journal of Formal Methods for System Design, 38(2): 97-118, 2011.
  • Laurent Doyen and Jean-François Raskin. Games with Imperfect Information: Theory and Algorithms. Lecture in Games Theory for Computer Scientists. Cambridge University Press, pp.185-212, 2011.
  • Thomas Brihaye, Gilles Geeraerts, Laurent Doyen, Joel Ouaknine, Jean-François Raskin and James Worrell. On reachability for Hybrid Automata over Bounded Time. In ICALP'11, LNCS 6756, Springer, pp. 416-427, 2011. 
  • Emmanuel Filiot, Jin Nayong, and Jean-François Raskin. Antichain and Compositional Algorithms for LTL Synthesis. To appear in Journal of Formal Methods for System Design, 2011.
  • Franck Cassez, Kim Larsen, Jean-François Raskin. Chapter on An Introduction to Discrete and Timed Controller Synthesis. In Quasimodo Handbook, Springer Book Series, 16 pages, 2011.
  • Franck Cassez, Kim Larsen, Jean-François Raskin. Chapter on Controller Synthesis: the Hydac case study. In Quasimodo Handbook, Springer Book Series, 18 pages, 2011.
  • Emmanuel Filiot, Jin Nayong, and Jean-François Raskin. Exploiting Structure in LTL Synthesis. To appear in STTT, 21 pages, 2011.

    • 2010

  • Krishnendu Chatterjee, Laurent Doyen, Thomas Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In FSTTCS'10, Leibniz International Proceedings in Informatics, Chenay, Indian, December 2010.
  • Pierre Ganty, Nicolas Maquet, and Jean-François Raskin. Fixpoint Guided Abstraction for Alternating Automata. Extended invited version. In Theoretical Computer Science 411(38-39):3444-3459, Elsevier, 2010.
  • Barbara Di Giampaolo, Gilles Geeraerts, Jean-François Raskin, and Nathalie Sznajder. Safraless Procedures for Timed Specifications. In FORMATS'10, LNCS 6246, Springer, pp. 2-22, 2010.
  • Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier, Frédéric Servais, and Jean-Marc Talbot. Properties of Visibly Pushdown Transducers. In MFCS'10, LNCS 6281, Springer, pp. 355-367, Springer, 2010.
  • Andreas Classen, Patrick Heymans, Axel Legay, Jean-François Raskin, and Pierre-Yves Schobbens. Model Checking lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines. In International Conference Software Engineering 2010, IEEE, Cape Town, pp. 335-344, 2010.
  • Emmanuel Filiot, Tristan Le Gall, Jean-François Raskin. Regret Minimization in Game Graphs. To appear in MFCS'10, LNCS 6281, Springer, pp. 342-354, 2010.  
  • G. Geeraerts, G. Kalyon, T. Le Gall, N. Maquet, and J.-F. Raskin. Lattice-Valued Binary Decision Diagrams. In ATVA'10, LNCS 6252, Springer, pp. 158-172, 2010.
  • Emmanuel Filiot, Nayiong Jin, and Jean-François Raskin. Compositional Algorithms for LTL Synthesis. In ATVA'10, LNCS 6252, Springer, pp. 112-127, 2010.
  • Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Torunczyk. Energy and Mean-Payoff Games with Imperfect Information. In CSL'10, LNCS 6247, Springer, pp. 260-274, 2010.
  • Laurent Doyen and Jean-François Raskin. Antichain Algorithms for Finite Automata. In TACAS'10, LNCS, 6015, Springer, pp. 2-22, 2010.
  • Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. On the efficient computation of the coverability set for Petri nets. International Journal of Foundations of Computer Science, 21(2):135-165, 2010.
          2009 
  • Pierre Ganty, Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin. Méthodes algorithmiques pour l'analyse des réseaux de Petri. Techniques et sciences informatiques 28/9, 1107-1142, Lavoisier, 2009.
  • Jean-François Raskin. Exploiting Structure in Automata Constructions (abstract). Invited talk at the General Meeting of the Authomatha project. 3 pages. Liège, 2009.
  • Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, and Julien Reichert. Realizability of Real-time Logics. In FORMATS09, LNCS 5813, Springer, pp.133-148 2009.
  • Pierre Ganty, Nicolas Maquet, and Jean-François Raskin. Fixpoint Guided Abstraction for Alternating Automata. In CIAA'09, LNCS 5642, Springer, pp.155-164, 2009.
  • Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. An Antichain Algorithm for LTL Realizability. In CAV'09, LNCS 5643, Springer, pp.263-277, 2009.
  • Laurent Doyen and Jean-François Raskin. Improved Algorithms for the Automata-Based Approach to Model-Checking. In Journal of Logical Methods in Computer Science-5(1:5)2009.
  • Franck Cassez, Jan J. Jessen, Kim Larsen, Jean-François Raskin, and Pierre-Alain Reynier. Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study. In HSCC'09, LNCS 5469, Springer, pp. 90-104, 2009.

    • 2008

  • Martin De Wulf, Laurent Doyen, Nicolas Maquet, and Jean-François Raskin. Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking. In TACAS'08, LNCS 4963, Springer, pp. 63-77, 2008.
  • Laurent Doyen, Tom Henzinger, and Jean-François Raskin. Equivalence of Labelled Markov Chains. In International Journal of Foundations of Computer Science, 19(3):549-563, 2008.
  • Pierre Ganty, Jean-François Raskin, Laurent Van Begin. From Many Places to Few: Automatic Abstraction Refinement for Petri Nets. Invited extended version. In Fundamenta Informaticae:88(3), 275-305, 2008.
  • Jean-François Raskin and Frédéric Servais. Visibly Pushdown Transducers. In ICALP'08, LNCS 5126, Springer, pp. 386-397, 2008.
  • Martin De Wulf, Laurent Doyen, Nicolas Marquet, and Jean-François Raskin. LTL Satisfiability, Alternating Büchi Automata Emptiness, and Model-Checking with ALASKA. In ATVA'08, LNCS 5311, Springer, pp. 240-245, 2008.
  • Martin De Wulf, Laurent Doyen, Nicolas Markey, Jean-François Raskin: Robust safety of timed automata. Formal Methods in System Design 33(1-3): 45-84 (2008)
  • Véronique Bruyère, Emmanuel Dal'ollio, and Jean-François Raskin. Durations and Parametric Model-Checking in Timed Automata. In Transactions on Computational Logic, 9(2), 21 pages, ACM press, 2008.

    2007

  • Jean-Francois Raskin. Controller Synthesis using Lattice Theory. Invited tutorial. Proceeding of the 46th conference on Decision and Control (CDC 2007), IEEE press. New-Orleans. December 2007. (4 pages)
  • Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. Well-structured Languages. In Acta Informatica 44(3-4):249-288, Springer, 2007.
  • Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. On the efficient computation of the coverability set for Petri nets. In ATVA'07, LNCS 4762, Springer, pp.98-113, 2007.
  • Franck Cassez, Alexandre David, Didier Lime, Kim Larsen, and Jean-François Raskin. Timed Control with Observation Based and Stuttering Invariant Strategies. In ATVA'07, LNCS 4762, Springer, pp.192-206, 2007.
  • Patrick Cousot, Pierre Ganty, and Jean-Francois Raskin. Fixpoint-based Abstraction Refinement. In SAS'07, LNCS 4634, Springer, pp.333-348, 2007.
  • Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, and Jean-Francois Raskin. Minimum-Time Reachability in Timed Games. In ICALP'07, LNCS 4596, Springer, pp.825-837, 2007.
  • Khrishnendu Charterjee, Laurent Doyen, Thomas A. Henzinger and Jean-Francois Raskin. Algorithms for Omega-regular games of Incomplete Information (extended version). Accepted for publication in Logical Methods in Computer Science, 2007. (30 pages).
  • Thomas Brihaie, Patricia Boyer, Véronique Bruyère, Jean-François Raskin. On the Optimal Reachability Problem for Timed Automata. In Formal Methods in Systems Design 31(2):135-175, Springer, 2007.
  • Pierre Ganty, Jean-François Raskin, Laurent Van Begin. From Many Places to Few: Automatic Abstraction Refinement for Petri Nets. In ICATPN'07, LNCS 4546, Springer, pp.124-143, 2007.
  • Véronique Bruyère and Jean-François Raskin. Real-Time Model-Checking: Parameters Everywhere (extended version). In Logical Methods in Computer Science 3(1):1-30, 2007.
  • Laurent Doyen and Jean-François Raskin. Improved Algorithms for the Automata-based Approach to Model-Checking. In TACAS'07, LNCS 4424,  Springer Verlag, 2007.
  • Véronique Bruyère and Jean-Francois Raskin. Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic. In Transactions in Computatitonal Logic 9(2), ACM Press, 2007.

2006

  • Khrishnendu Charterjee, Laurent Doyen, Thomas A. Henzinger and Jean-Francois Raskin. Algorithms for Omega-regular games of Incomplete Information. In CSL'06, Lecture Notes in Computer Science, 4207, 287-302, 2006. (16 pages)
  • Jean-Francois Raskin and Frédéric Servais. On the Symbolic Computation of the Hardest Configurations of the Rush Hour Game. To appear in CG'06, Lecture Notes in Computer Science. (12 pages)
  • Martin De Wulf, Laurent Doyen, Thomas A. Henzinger and Jean-Francois Raskin. Antichains: a New Algorithm to Solve Universality of FA. In CAV'06, Lecture Notes in Computer Science, 4144, Springer-Verlag, pp. 17-30, 2006.
  • Martin De Wulf, Laurent Doyen, and Jean-Francois Raskin. A Lattice Theory for Solving Games of Imperfect Information. In HSCC'06, Lecture Notes in Computer Science, 3927, pp. 153-168, Springer-Verlag, 2006.
  • Pierre Ganty, Jean-François Raskin, and Laurent Van Begin. A Complete Abstract Interpretation Framework for Coverability Properties of WSTS. In VMCAI'06, Lecture Notes in Computer Science 3855, pp. 49-64, Springer Verlag, 2006.
  • Nicolas Markey and Jean-François Raskin. Model-Checking Restricted Sets of Timed Paths (extended version). In Theoretical Computer Science, 358(2-3):273--292, Elsevier Science, 2006.
  • Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On Model-Checking Timed Automata with Stopwatch Observers. In Information and Computation, 204:408--433, Elservier Sciences, 2006.
  • Alain Finkel, Gilles Geeraerts, Jean-François Raskin and Laurent Van Begin. On the Omega-Language Expressive Power of Extended Petri Nets (extended version). In Theoretical Computer Science, 356(3):374--386, Elsevier Sciences, 2006.

    2005

  • Laurent Doyen, Tom Henzinger, Jean-François Raskin. Automatic Rectangular Refinement of Affine Hybrid Systems. In FORMATS'05, Lecture Notes in Computer Science 3829, pp. 144--161,Springer-Verlag, 2005.
  • Gilles Geeraerts, Jean-Francois Raskin and Laurent Van Begin. Expand,Enlarge, and Check. New Algorithms to Solve the Coverability Problem of WSTS (extended version). In Journal of Computer and System Sciences, 72(1):180-203, Elsevier Sciences, 2005. 
  • Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On Optimal Timed Strategies. In FORMATS'05, Lecture Notes in Computer Science 3829, pp. 49--64, Springer-Verlag, 2005.
  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Systematic Implementations of Timed Models. In FM'05, Lecture Notes in Computer Science 3582, pp. 139--156, Springer-Verlag, 2005.
  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Almost ASAP Semantics: from Timed Models to Timed Implementations (extended version).In Formal Aspect of Computing, 17(3):319--341, Springer-Verlag, 2005.
  • Jean-François Raskin. An Introduction to Hybrid Automata. In Handbook of Networked and Embedded Control Systems, pp 491-518, Dimitrios Hristu-Varsakelis, William S. Levine (Eds.), Birkhauser, 2005, ISBN 0-8176-3239-5.
  • Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. Expand, Enlarge and Check Made Efficient. In CAV'05, Lecture Notes in Computer Science 3576, pp. 394--407, Springer-Verlag, 2005.
  • Alain Finkel, Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. On the omega-language expressive power of extended Petri nets. In Electronic Notes in Theoretical Computer Science, Volume 128, Issue 2, pp 87-101, 2005. 
  • Thomas Henzinger, Rupak Manjumdar, and Jean-François Raskin. A Classification of Symbolic Transition Systems. In Transactions on Computational Logic, Volume 6, Number 1, pp 1-31, ACM Press, 2005.
  • Jean-Francois Raskin and Laurent Van Begin. Games for Counting Abstractions. In Electronic Notes in Theoretical Computer Science, 128(6):69-85, Elsevier Science, 2005.

    2004

  • Giorgio Delzanno, Jean-Francois Raskin, and Laurent Van Begin. Covering Sharing-Trees: a Compact Data-Structure for Parametrized Verification. In the Journal of Software Tools for Technology Transfer, Volume 5, Numbers 2-3, pp 268-297, Springer Verlag, March 2004. [Postscript]
  • Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robustness and Implementability of Timed Automata. In FORMATS'04, Lecture Notes in Computer Science, 3253, pp. 118-133, Springer Verlag, 2004.
  • Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. In FSTTCS'04, Lecture Notes in Computer Science, 3328, pages 287--298. Springer-Verlag, 2004.
  • Jean-françois Raskin and Laurent Van Begin. Petri with Non-blocking Arcs are Difficult to Analyze. In Electronic Notes in Theoretical Computer Science, 98, 35-55, Elsevier Science, 2004 [Postscript]
  • Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin.  Model-Checking Weigthed Timed Automata. In FORMATS'04, Lecture Notes in Computer Science, 3253, pp. 277-292, Springer Verlag, 2004.
  • Nicolas Markey and Jean-François Raskin. Model-Checking Restricted Sets of Timed Paths. In CONCUR'04, Lecture Notes in Computer Science, 3170, pp. 432-447, Springer-Verlag, 2004.
  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Almost ASAP Semantics: From Timed Models to Timed Implementations. In HSCC'04, Lecture Notes in Computer Science, 2993, pp 296-310, 2004. [Postscript]

    2003

  • Jean-françois Raskin, Mathias Samuelides, and Laurent Van Begin. Petri Games are Monotonic but Difficult to Decide. Technical Report 508, ULB, 2003. [Postscript]
  • Steve Kremer and Jean-François Raskin. A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols (Extended Version). In Journal of Computer Security, 11(3), 399-430, Ios Press. 2003.  [Postscript]
  • Véronique Bruyère, Jean-François Raskin. Real-time Model-checking: Parameters Everywhere ! In the In FSTTCS'03, Lecture Notes in Computer Science, 2914, pp. 100-111, Springer-Verlag, 2003. [Postscript]
  • Véronique Bruyère, Emmanuel Dall'Olio, Jean-François Raskin. Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic. In STACS'03, Lecture Notes in Computer Science, 2607, Berlin, 2003. [Postscript]

    2002

  • Alain Finkel, Jean-François Raskin, Mathias Samuelidis, and Laurent Van Begin. Monotonic Extensions of Petri Nets: Forward and Backward Search Revisited. In the proceedings of INFINITY'02, Electronic Notes in Theoretical Computer Science, Volume 68, Issue 6, Elsevier, Brno, 2002. (20 pages) 
  • Jean-Francois Raskin, Pierre-Yves Schobbens, Thomas A. Henzinger and Laurent F'erier. Axioms for Real-Time Logics. In Theoretical Computer Science, 274(1-2), 151-182, Elsevier Science, 2002.
  • Thierry Massart, Jean-françois Raskin, and Laurent Van Begin. Symbolic Distributed Verification of a Class of Parametric Concurrent Systems. In the proceedings of PDMC'02, Brno, 2002. (6 pages) [Postscript]
  • Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. Towards Automated Verification of Multithreaded Java Programs. In the Proc. of TACAS'02, Lecture Notes in Computer Science, 2280, Springer, pp 173-187. 2002. [Postscript]
  • Franck Cassez, Thomas Henzinger, and Jean-François Raskin. A Comparison of Control Problems for Timed and Hybrid Systems. In HSCC'02, Lecture Notes in Computer Science, 2289, pp. 134-148, Springer-Verlag, 2002 (18 pages) [Postscript]
  • Steve Kremer and Jean-François Raskin. Game Analysis of Abuse-free Contract Signing . In Computer Security Foundations Workshop 2002 (CSFW 2002),Cape Breton, Nova Scotia, Canada (15 pages).  [Postscript]

    2001

  • Steve Kremer and Jean-François Raskin. A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols . In CONCUR 2001-Concurrency Theory,, Aalborg, Danemark, August 2001 (15 pages).  [Postscript]
  • Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. Attacking Symbolic State Explosion in Parametrized Verification. In the Proc. of CAV'01: International Conference on Computer Aided Verification, Lecture Notes in Computer Science, 2102, Springer, pp 298-310, Paris, 2001. [Postscript]

    2000

  • Thomas Henzinger and Jean-François Raskin. Robust Undecidability of Timed and Hybrid Systems. In HSCC'00, Lecture Notes in Computer Science, 1790, pp. 145-159, Springer Verlag, 2000. [Postscript]
  • Giorgio Delzanno and Jean-Francois Raskin. Symbolic Representation Of Up-Ward Closed Sets. In Tacas'00, Lecture Notes In Computer Science 1785, Pp. 426-440, Springer-Verlag, 2000.
  • Thomas A. Henzinger, Freddy Mang, Rupak Manjumdar and Jean-Francois Raskin. Abstract Interpretation of Game Properties. In SAS'00, Lecture Notes in Computer Science 1824, pp. 220-239, Springer-Verlag, 2000.
  • Jean-François Raskin and Pierre-Yves Schobbens. Automata for Qualitative Real-Time. In the proceedings of Les journées montoises de l'informatique théorique, Marnes-La-Vallée, France, March 2000. [Postscript]
  • Steve Kremer and Jean-François Raskin. Formal Verification of Non-Repudiation Protocols- A Game Approach . In Formal Methods for Computer Security, Chicago, USA, July 2000 (13 pages).  [Postscript]
  • Steve Kremer and Jean-François Raskin. A Game Approach to the Verification of Exchange Protocols - Application to Non-Repudiation Protocols. In Workshop on Issues in the Theory of Security (WITS '00), Geneve, Switzerland, June 2000. (6 pages). [Postscript]

    1999

  • Jean-François Raskin and Pierre-Yves Schobbens. The Logic of Event Clocks, Decidability, Complexity,and Expressiveness. In Journal of Automata, Languages and Combinatorics, 4, 3, Otto-von-Guericke-Universität Magdeburg, September 1999. (37 pages) [Postscript]
  • Laurent Ferrier, Jean-François Raskin, and Pierre-Yves Schobbens. Models Generation of a Fictitious Clock Real-Time Logic Using Sharing-Trees. In Symbolic Model Checking 99, appeared as Volume 23, Issue 2 of Electronic Notes in Theoretical Computer Science, Trento, Italy, July 1999. [Postscript]
  • Jean-François Raskin. Logics, Automata and Classical Theories for Deciding Real Time. Ph. D. Thesis of the Computer Science Department. University of Namur, Belgium, April 1999. (223 pages) [Postscript]
  • Jean-François Raskin and Pierre-Yves Schobbens. The Logic of Initially and Next, Complete Axiomatisationand Complexity Issues. In Information ProcessingLetters, 69, Issue 5, pp 221-225, Elsevier Science, March 1999. [Postscript]

    1998

  • Thomas Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. Axioms for Real-Time Logics. In International Conference on Concurrency, Lecture Notes in Computer Science, 1466, Springer-Verlag, Nice, France, August 1998. [Postscript]
  • Thomas Henzinger, Jean-François Raskin and Pierre-Yves Schobbens. The Regular Real-Time Languages. In International Colloquium on Automata, Languages,and Programming, Lecture Notes in Computer Science, 1443, Springer-Verlag, pp 580-591, Aalborg, Denmark, July 1998. [Postscript]

    1997

  • Jean-François Raskin and Pierre-Yves Schobbens. Real-Time Logics : Fictitious Clock as an Abstraction of Dense Time. In Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science,  1217, Springer Verlag, pp165-182, Twente,The Netherlands, April 1997. [Postscript]
  • Jean-François Raskin and Pierre-Yves Schobbens. State Clock Logic: a Decidable Real-Time Logic .In  Hybrid and Real-Time Systems, Lecture Notes in Computer Science, 1201, Springer Verlag, pp 31-47, Grenoble, France, March 1997. [Postscript]
Teaching (some in french)

NEW INFO-F-408 Calculability and complexity.
Schedule of the course (1st semester 2010-2011) - Slides (English)
List of questions for the exam.

INFO-F-421. Advanced course on calculability and complexity. Slides. Slides 2

INFO-F-513. Vérification 2. Description du cours.

INFO-F-302. Logique pour l'informatique.

INFO-F-502. Séminaire d'informatique approfondie.

Last updated: October 2011.

Free counter and web stats