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.
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 
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.
Simon Busard joins LVL
The LVL team welcomes new researcher Simon Busard.
LVL site goes public
The LVL site is now stable, operational and open to public visit.
ASE 2010 in Antwerp in September
Charles Pecheur is chairing the 25th IEEE/ACM International Conference on Automated Software Engineering, which will be held in Antwerp, Belgium, 20-24 September 2010.
-
Find It
Sections
LVL PartialOrderReduction SymbolicModelChecking Verification BoundedModelChecking ThemeExplanation Counterexamples EpistemicLogic Publications HumanComputerInteraction Equivalences ProjectMOVES ProjectNASA ThemeHMI ToolJpf-hmi Learning ProcessAlgebra CTL ThemePOR ModelChecking LTL ToolMilestones Simulation Requirements CoverageCriteria ThemeCoverage Testing Planning StructuralCoverage PDDL SoftwareEngineering