Specification and Verification Axis
Paris 13 > LIPN > LCR > Specification and Verification Axis
Members
Full professors
Professors
Ph.D. Students
Interns
Upcoming events
MeFoSyLoMa seminary and CosyVerif Day
Friday March 23rd 2012 at LIPN
- MeFoSyLoMa seminary dedicated to the CosyVerif platform, of which several tools in the Specification and Verification axes are members.
CosyVerif Day
Friday March 23rd 2012 at LSV (ENS Cachan)
- Integration-party of the CosyVerif platform, of which several tools in the Specification and Verification axes are members.
Some recent events
Seminary by Hanen Ochi
Friday January 27th 2012 at 3pm30 at LIPN (room A304)
- Hanen Ochi, Ph.D. candidate at LIPN, will be giving a talk on Modular Verification of Inter-enterprise Business Processes.
Seminary by Jean-Claude Royer
Friday December 9th 2011 at 10.30am at LIPN
- Jean-Claude Royer, professor at École des Mines de Nantes, will be giving a talk on type controle in Web services with dynamic chanel discovery.
Mid-Ph.D. Defense of Alfred Sanogo
Friday December 9th 2011 at 1.30pm at LIPN
- Alfred Sanogo, Ph.D. candidate at LIPN, will be giving a talk on methodology of conception of models expressed using Petri nets.
Themes
See our research activity report 2003 − 2006 at LIPN (the 2007−2010 activity report is under construction and will be ready late 2012).
See the axis bibliography, or the bibliography of each our members.
Last minute
We are looking for an engineer (CDD, 4 months) and a Master 2 intern (funding provided), in order to perform software integration to the CosyVerif platform. Starting as soon as possible (spring and summer 2012). More information here (in French! please write us for English translation and additional information).
Internships 2012
Our research axis proposes a list of internship opportunities for Master students, for spring and summer 2012.
In case you are interested in a particular subject, please contact the researcher(s) proposing it.
Also feel free to contact us for any question.
Tools
- Helena: a high level Petri net model checker
- IMITATOR: synthesis of parameters for timed automata (co-developed at LSV)
- MCsog: LTL\X model checker based on symbolic observation graphs
- modsog: tool for building a symbolic observation graph in a symbolic manner
Projects
- CosyVerif: Software environment whose goal is the formal specification and verification of dynamic systems
- Merlion: Software Verification from Design to Implementation
- Neoppod: specification and verification of large scale distributed database system
Collaborations and visitors
- Jonathan Billington (University of South Australia, Australie)
- Patrice Carle (Onera)
- Philippe Darondeau (IRISA, Rennes, France)
- Jörg Desel (Universität Hagen)
- Jin-Song Dong (National University of Singapore)
- Laurent Fribourg (LSV, Cachan, France)
- Maritta Heisel (Duisburg−Essen)
- Kurt Jensen (Université d’Århus, Danemark)
- Romain Kervarc (Onera)
- Ekkart Kindler (DTU)
- Lars Michael Kristensen (Bergen University College, Bergen, Norvège)
- Charles Lakos (University of Adelaide, Australie)
- Shang-Wei Lin (National University of Singapore)
- Yang Liu (National University of Singapore)
- Gianna Reggio (Université de Gênes, Italie)
- Romain Soulat (LSV, Cachan, France)
- Jun Sun (Singapore University of Technology and Design)
Former members
- Olivier Bertrand (DGA)
- Fabien Bonnefoi
- Samir Youcef (LORIA, Nancy, France)
Seminaries
]
]