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".

Sébastien is the second LVL researcher to earn his doctorate, after José Vander Meulen in 2012. He started as a PhD student in 2007. Stay tuned on this channel for updates on his upcoming endeavours.

Tags: Human Computer Interaction, Verification, LVL, Thesis

FMICS 2013 will take place in Madrid in September.

The 18th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2013) will take place September 23-24, 2013 in Madrid, in co-location with SEFM 2013. FMICS 2013 is co-chaired by Charles Pecheur from LVL and Michael Dierkes from Rockwell-Collins (France). Submissions are due May 3, 2013.

For more information, please visit the FMICS 2013 website.

Tags: Event, Fmics, Conference

Simon Busard and Charles Pecheur had a paper accepted at SR 2013, and another paper accepted at NFM 2013.

SR 2013, the First International Workshop on Strategic Reasoning, was co-located with ETAPS 2013 and took place in Rome, Italy, in March 2013. The paper covers recent research in the field of reasoning about strategies under partial observability and fairness constraints.

NFM 2013, the 5th NASA Formal Methods Symposium, will take place at the NASA Ames Research Center, in Moffett Field, CA, USA, in May 2013. The paper presents PyNuSMV, a Python framework for experimenting and prototyping BDD-based model checking algorithms based on NuSMV.

Tags: Strategies, Tools, Publications

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".

José thus becomes the first researcher to earn his PhD in the young LVL team. He was also the first to join Charles Pecheur back in 2006, initiating what would become LVL a few years later. Stay tuned on this channel for updates on his upcoming endeavours.

Tags: LVL, Partial Order Reduction, Symbolic Model Checking

Simon Busard and Charles Pecheur had a paper accepted at IWIGP 2012.

IWIGP 2012, the International Workshop on Interactions, Games and Protocols, is co-located with ETAPS 2012 and will take place Tallinn, Estonia, in March 2012. This paper covers recent advances in the research of Simon Busard.

Tags: Counterexamples, Epistemic Logic, Publications

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.

Two papers resulting from the collaboration with NASA Ames were presented last week at the MALETS 2011 workshop and the JPF workshop 2011 which were satellite workshops of the ASE 2011 conference (Lawrence, KA, USA).

The paper presented at MALETS, entitled "Learning System Abstractions for Human Operators", has been designated as the best paper of the workshop.

The two papers:

• Learning System Abstractions for Human Operators
• A JavaPathfinder Extension to Analyse Human-Machine Interactions

Tags: ProjectNASA, Human Computer Interaction

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.

The LVL group is organizing a meeting on Human Machine Interaction, this week, on November 17. The meeting is focused on Models and Tools for Human-Machine Interaction.

The meeting has two parts: the morning consists of workshop-style presentations and the afternoon will be dedicated to open discussions.

Full details on the HMI Meeting 2011 page.

Tags: Human Computer Interaction

Sébastien Combéfis and Charles Pecheur had a full paper accepted at SMC 2011.

SMC 2011 has this year a special track on "Applications of Formal Methods to Human-Automation Interaction" where the paper "A Formal Framework for Design and Analysis of Human-Machine Interaction" will be presented.

That paper is the result of a collaboration with the Robust Software Engineering and Human Factors groups from the NASA Ames Research Center.

Tags: Human Computer Interaction, Publications

A new Tools section is now available on the LVL website.

This new section gives access to software developed by LVL. Two packages are currently proposed:

• Milestones is a model checker that combines symbolic model-checking and partial-order reduction (by José Vander Meulen).
• NuSMV-ARCTL-TLACE is an extension of the NuSMV model-checker adding two main functionalities: model checking of ARCTL (by Franco Raimondi) and generation of complete counter-examples (by Simon Busard).

More will come soon, stay tuned...

Tags: Tools, Website, LVL

José Vander Meulen and Charles Pecheur had a full paper and a tool paper accepted at NFM 2011.

NFM 2011, the Third NASA Formal Methods Symposium, will take place in Pasadena, CA in April 2011. Both papers cover recent advances in the research of José Vander Meulen.

Tags: Symbolic Model Checking, Partial Order Reduction, Publications