Welcome to LVL!
Other LVLs...
The Louvain Verification Lab (LVL) is a research team in the ICTEAM institute at Université catholique de Louvain. LVL investigates principles, tools and applications of formal analysis and verification of computer systems. LVL was officially created in 2010 but members of the team have been active in this field at UCL since 2004.
Computer programs continue to invade every inch of individuals, enterprises and societies. They keep getting more complex and interdependent. Just like building bridges or rockets, building dependable programs demands sound engineering principles grounded in solid mathematical foundations. LVL's goal is to invent and improve rigorous techniques for developing, analyzing, transforming and synthesizing models of programs and computing systems.
The research at LVL mainly revolves around the automated verification technique known as model checking, under different views and directions. As typical for such automated software engineering disciplines, the work combines devising new methods and algorithms, implementing these algorithms into actual software tools, and assessing and validating them on actual case studies and applications. Formalisms and languages used to represent systems and their properties are also studied, with connections to logic and automata theory.
More specifically, fields of interest of LVL researchers include:
- Symbolic and Bounded Model-Checking,
- Verification of Human-Computer Interaction,
- Generation of Enriched Verification Explanations,
- Verification of Concurrent Systems and Partial-Order Reduction,
- Structural Coverage Criteria for Specifications,
- Temporal and Epistemic Logics,
- Analysis of Observability and Diagnosis,
- Verification of Autonomous and Intelligent Systems.
- Verification of railway interlocking.
LVL is always looking for opportunities for scientific and industrial collaborations. In particular, pilot studies in applying innovative methods to real-life industrial applications provide an excellent opportunity to assess and demonstrate benefits and identify new challenges.
Latest news 
Sebastien Combefis becomes a Doctor
On Wednesday 20. December 2013, Sébastien Combéfis brilliantly passed the public defense of his doctorate thesis entitled "A Formal Framework for the Analysis of Human-Machine Interactions".
Papers accepted at SR 2013 and NFM 2013
Simon Busard and Charles Pecheur had a paper accepted at SR 2013, and another paper accepted at NFM 2013.
FMICS 2013
FMICS 2013 will take place in Madrid in September.
Jose Vander Meulen completes his PhD
On Friday 17. April, José Vander Meulen brilliantly passed the public defense of his doctorate thesis entitled "Combining Partial Order Reduction with Symbolic Model Checking".
Paper accepted at iWIGP2012
Simon Busard and Charles Pecheur had a paper accepted at IWIGP 2012.
LVL is organizing an HMI meeting this week (November 17, 2011)
LVL is organizing and hosting a meeting focused on Human Machine Interaction this week, on the theme of Models and Tools for Human-Machine Interaction.
Two papers presented at workshops at ASE 2011 including one best paper
Two papers were accepted and presented at MALETS and JPF workshops which took place at ASE 2011. The MALETS paper is the best paper of the workshop.
Paper accepted at SMC 2011
Sébastien Combéfis and Charles Pecheur had a full paper accepted at SMC 2011.
LVL Tools now available
A new Tools section is now available on the LVL website.
Two papers at NFM 2011
José Vander Meulen and Charles Pecheur had a full paper and a tool paper accepted at NFM 2011.
-
Find It
Sections
Verification Diagnosis Autonomy ModelChecking Planning PDDL Requirements Testing LTL ThemeCoverage HumanComputerInteraction UserModel ProjectMOVES ThemeHMI LVL Website SymbolicModelChecking CTL Actions SMV EpistemicLogic ProjectNASA PartialOrderReduction BoundedModelChecking ThemePOR TemporalLogic Simulation Tools Tutorial Publication Equivalences