@INPROCEEDINGS{lvl-2018-962145,
    TITLE = {A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railway},
    AUTHOR = {Christophe Limbrée and Charles Pecheur},
    YEAR = {2018},
    URL = {https://lvl.info.ucl.ac.be/Publications/AFrameworkForTheFormalVerificationOfNetworksOfRailwayInterlockings-ApplicationToTheBelgianRailway},
  }
  @INPROCEEDINGS{lvl-2017-815241,
    TITLE = {A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability},
    AUTHOR = {Simon Busard and Charles Pecheur},
    YEAR = {2017},
    VOLUME = {256},
    PAGES =  {253-267},
    BOOKTITLE = {Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, Roma, Italy, 20-22 September 2017},
    PUBLISHER = {Open Publishing Association},
    EDITOR = {Patricia Bouyer and Andrea Orlandini and Pierluigi San Pietro},
    SERIES = {Electronic Proceedings in Theoretical Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/ABackward-traversal-basedApproachForSymbolicModelCheckingOfUniformStrategiesForConstrainedReachability},
  }
  @BOOK{lvl-2017-675896,
    TITLE = {Symbolic model checking of multi-modal logics: uniform strategies and rich explanations},
    AUTHOR = {Simon Busard},
    YEAR = {2017},
    VOLUME = {610},
    PUBLISHER = {Doctoral thesis, Université catholique de Louvain},
    URL = {https://lvl.info.ucl.ac.be/Publications/SymbolicModelCheckingOfMulti-modalLogicsUniformStrategiesAndRichExplanations},
  }
  @INPROCEEDINGS{lvl-2016-452384,
    TITLE = {Verification of railway interlocking - Compositional approach with OCRA},
    AUTHOR = {Christophe Limbree and Quentin Cappart and Charles Pecheur and Stefano Tonetta},
    YEAR = {2016},
    VOLUME = {9707},
    PAGES =  {134--149},
    BOOKTITLE = {Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification},
    PUBLISHER = {Springer International Publishing},
    SERIES = {Lecture Notes in Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/VerificationOfRailwayInterlocking-CompositionalApproachWithOCRA},
  }
  @ARTICLE{lvl-2016-382952,
    TITLE = {Automatic Detection of Potential Automation Surprises for ADEPT Models},
    AUTHOR = {Sébastien Combéfis and Dimitra Giannakopoulou and Charles Pecheur},
    YEAR = {2016},
    JOURNAL = {IEEE Transactions on Human-Machine Systems},
    VOLUME = {46},
    NUMBER = {2},
    PAGES =  {267--278},
    URL = {https://lvl.info.ucl.ac.be/Publications/AutomaticDetectionOfPotentialAutomationSurprisesForADEPTModels},
  }
  @INPROCEEDINGS{lvl-2015-225165,
    TITLE = {Verification of railway interlocking systems},
    AUTHOR = {Simon Busard and Quentin Cappart and Christophe Limbr\ee and },
    YEAR = {2015},
    VOLUME = {184},
    PAGES =  {19-31},
    BOOKTITLE = {Proceedings 4th International Workshop on Engineering Safety and Security Systems, Oslo, Norway, June 22, 2015},
    PUBLISHER = {Open Publishing Association},
    EDITOR = {ang and Jun and Liu and Yang and Mauw and Sjouke},
    SERIES = {Electronic Proceedings in Theoretical Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/VerificationOfRailwayInterlockingSystems},
  }
  @INPROCEEDINGS{lvl-2015-885814,
    TITLE = {Tasks Decomposition of System Models for Human-Machine Interaction Analysis},
    AUTHOR = {Guillaume Maudoux and Sébastien Combéfis and Charles Pecheur},
    YEAR = {2015},
    PAGES =  {7-12},
    BOOKTITLE = {Proceedings of the Workshop on Formal Methods for Human Computer Interaction 2015},
    EDITOR = {Benjamin Weyers and Judy Bowen and Alan Dix and Philippe Palanque},
    URL = {https://lvl.info.ucl.ac.be/Publications/TasksDecompositionOfSystemModelsForHuman-MachineInteractionAnalysis},
  }
  @ARTICLE{lvl-2015-423232,
    TITLE = {Reasoning about memoryless strategies under partial observability and unconditional fairness constraints},
    AUTHOR = {Simon Busard and Charles Pecheur and Hongyang Qu and Franco Raimondi},
    YEAR = {2015},
    JOURNAL = {Information and Computation},
    VOLUME = {242},
    NUMBER = {0},
    PAGES =  {128-156},
    URL = {https://lvl.info.ucl.ac.be/Publications/ReasoningAboutMemorylessStrategiesUnderPartialObservabilityAndUnconditionalFairnessConstraints},
  }
  @INPROCEEDINGS{lvl-2014-825257,
    TITLE = {Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints},
    AUTHOR = {Simon Busard and Charles Pecheur and Hongyang Qu and Franco Raimondi},
    YEAR = {2014},
    VOLUME = {8829},
    PAGES =  {27-42},
    BOOKTITLE = {Formal Methods and Software Engineering},
    PUBLISHER = {Springer International Publishing},
    EDITOR = {Stephan Merz and Jun Pang},
    SERIES = {Lecture Notes in Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/ImprovingTheModelCheckingOfStrategiesUnderPartialObservabilityAndFairnessConstraints},
  }
  @INPROCEEDINGS{lvl-2014-229048,
    TITLE = {A Methodology for Analyzing Human-Automation Interactions in Flight Operations Using Formal Verification Techniques},
    AUTHOR = {Denis Javaux and Bertram Wortelen and Andreas Lüdtke and Charles Pecheur and Regina Peldszus and Sonja Sievi and Yuri Yushtein},
    YEAR = {2014},
    BOOKTITLE = {Proceedings of AAAI Symposium on Formal Verification in Human-Machine Systems},
    PUBLISHER = {AAAI},
    EDITOR = {Eric G. Mercer and Michael A. Goodrich and Neha Rungta and Ellen Bass },
    URL = {https://lvl.info.ucl.ac.be/Publications/AMethodologyForAnalyzingHuman-AutomationInteractionsInFlightOperationsUsingFormalVerificationTechniques},
  }
  @INPROCEEDINGS{lvl-2014-975903,
    TITLE = {State Event Models for the Formal Analysis of Human-Machine Interactions},
    AUTHOR = {Sébastien Combéfis and Dimitra Giannakopoulou and Charles Pecheur},
    YEAR = {2014},
    BOOKTITLE = {Proceedings of AAAI Symposium on Formal Verification in Human-Machine Systems},
    PUBLISHER = {AAAI},
    EDITOR = {Eric G. Mercer and Michael A. Goodrich and Neha Rungta and Ellen Bass},
    URL = {https://lvl.info.ucl.ac.be/Publications/StateEventModelsForTheFormalAnalysisOfHuman-MachineInteractions},
  }
  @BOOK{lvl-2013-887851,
    TITLE = {A Formal Framework for the Analysis of Human-Machine Interactions},
    AUTHOR = {Sébastien Combéfis},
    YEAR = {2013},
    VOLUME = {459},
    PUBLISHER = {Doctoral thesis, Université catholique de Louvain},
    URL = {https://lvl.info.ucl.ac.be/Publications/AFormalFrameworkForTheAnalysisOfHuman-MachineInteractions},
  }
  @BOOK{lvl-2013-668504,
    TITLE = {Formal Methods for Industrial Critical Systems, 18th International Workshop (FMICS 2013)},
    AUTHOR = {Charles Pecheur and Michael Dierkes},
    YEAR = {2013},
    VOLUME = {8187},
    PUBLISHER = {Springer},
    SERIES = {LNCS},
    URL = {https://lvl.info.ucl.ac.be/Publications/FormalMethodsForIndustrialCriticalSystems18thInternationalWorkshopFMICS2013},
  }
  @INPROCEEDINGS{lvl-2013-707009,
    TITLE = {PyNuSMV: NuSMV as a Python Library},
    AUTHOR = {Simon Busard and Charles Pecheur},
    YEAR = {2013},
    VOLUME = {7871},
    PAGES =  {453-458},
    BOOKTITLE = {Nasa Formal Methods 2013},
    PUBLISHER = {Springer-Verlag},
    EDITOR = {G. Brat and N. Rungta and and A. Venet},
    SERIES = {LNCS},
    URL = {https://lvl.info.ucl.ac.be/Publications/PyNuSMVNuSMVAsAPythonLibrary},
  }
  @INPROCEEDINGS{lvl-2013-641696,
    TITLE = {Reasoning about Strategies under Partial Observability and Fairness Constraints},
    AUTHOR = {Simon Busard and Charles Pecheur and Hongyang Qu and Franco Raimondi},
    YEAR = {2013},
    VOLUME = {112},
    PAGES =  {71-79},
    BOOKTITLE = {Proceedings 1st International Workshop on Strategic Reasoning, Rome, Italy, March 16-17, 2013},
    PUBLISHER = {Open Publishing Association},
    EDITOR = {Mogavero and Fabio and Murano and Aniello and Vardi and Moshe Y.},
    SERIES = {Electronic Proceedings in Theoretical Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/ReasoningAboutStrategiesUnderPartialObservabilityAndFairnessConstraints},
  }
  @BOOK{lvl-2012-971829,
    TITLE = {Combining Partial Order Reduction with Symbolic Model Checking},
    AUTHOR = {José {Vander Meulen}},
    YEAR = {2012},
    VOLUME = {370},
    PUBLISHER = {Doctoral thesis, Université catholique de Louvain},
    URL = {https://lvl.info.ucl.ac.be/Publications/CombiningPartialOrderReductionWithSymbolicModelChecking},
  }
  @INPROCEEDINGS{lvl-2012-994846,
    TITLE = {Rich Counter-Examples for Temporal-Epistemic Logic Model Checking},
    AUTHOR = {Simon Busard and Charles Pecheur},
    YEAR = {2012},
    VOLUME = {78},
    PAGES =  {39-53},
    BOOKTITLE = {Proceedings Second International Workshop on Interactions, Games and Protocols, Tallinn, Estonia, 25th March 2012},
    PUBLISHER = {Open Publishing Association},
    EDITOR = {Johannes Reich and Bernd Finkbeiner},
    SERIES = {Electronic Proceedings in Theoretical Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/RichCounter-ExamplesForTemporal-EpistemicLogicModelChecking},
  }
  @INPROCEEDINGS{lvl-2011-959764,
    TITLE = {A JavaPathfinder Extension to Analyse Human-Machine Interactions},
    AUTHOR = {Sébastien Combéfis and Dimitra Giannakopoulou and Charles Pecheur and Peter Mehlitz},
    YEAR = {2011},
    BOOKTITLE = {Java Pathfinder Workshop 2011},
    URL = {https://lvl.info.ucl.ac.be/Publications/AJavaPathfinderExtensionToAnalyseHuman-MachineInteractions},
  }
  @INPROCEEDINGS{lvl-2011-784048,
    TITLE = {Learning System Abstractions for Human Operators},
    AUTHOR = {Sébastien Combéfis and Dimitra Giannakopoulou and Charles Pecheur and Michael Feary},
    YEAR = {2011},
    BOOKTITLE = {International Workshop on Machine Learning Technologies in Software Engineering},
    URL = {https://lvl.info.ucl.ac.be/Publications/LearningSystemAbstractionsForHumanOperators},
  }
  @INPROCEEDINGS{lvl-2011-1,
    TITLE = {Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties},
    AUTHOR = {José {Vander Meulen} and Charles Pecheur },
    YEAR = {2011},
    VOLUME = {6617},
    BOOKTITLE = {NASA FORMAL METHODS 2011},
    PUBLISHER = {Springer},
    EDITOR = {Mihaela Bobaru and Klaus Havelund and Gerard Holzmann and Rajeev Joshi },
    SERIES = {LNCS},
    URL = {https://lvl.info.ucl.ac.be/Publications/CombiningPartialOrderReductionAndSymbolicModelCheckingToVerifyLTLProperties},
  }
  @INPROCEEDINGS{lvl-2011-2,
    TITLE = {Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction},
    AUTHOR = {José {Vander Meulen} and Charles Pecheur},
    YEAR = {2011},
    VOLUME = {6617},
    BOOKTITLE = {NASA FORMAL METHODS 2011},
    PUBLISHER = {Springer},
    EDITOR = {Mihaela Bobaru and Klaus Havelund and Gerard Holzmann and Rajeev Joshi},
    SERIES = {LNCS},
    URL = {https://lvl.info.ucl.ac.be/Publications/MilestonesAModelCheckerCombiningSymbolicModelCheckingAndPartialOrderReduction},
  }
  @INPROCEEDINGS{lvl-2011-3,
    TITLE = {A Formal Framework for Design and Analysis of Human-Machine Interaction},
    AUTHOR = {Sébastien Combéfis and Dimitra Giannakopoulou and Charles Pecheur and Michael Feary},
    YEAR = {2011},
    BOOKTITLE = {2011 IEEE International Conference on Systems, Man, and Cybernetics},
    PUBLISHER = {IEEE},
    URL = {https://lvl.info.ucl.ac.be/Publications/AFormalFrameworkForDesignAndAnalysisOfHuman-MachineInteraction},
  }
  @BOOK{lvl-2010-1,
    TITLE = {25th IEEE-ACM International Conference on Automated Software Engineering},
    AUTHOR = {Charles Pecheur and Jamie Andrews and Elisabetta {Di Nitto} and Eds.},
    YEAR = {2010},
    PUBLISHER = {ACM},
    NOTE = {Conference proceedings},
    URL = {https://lvl.info.ucl.ac.be/Publications/25thIEEE-ACMInternationalConferenceOnAutomatedSoftwareEngineering},
  }
  @INPROCEEDINGS{lvl-2009-3,
    TITLE = {Combining Partial Order Reduction with Bounded Model Checking},
    AUTHOR = {José {Vander Meulen} and Charles Pecheur},
    YEAR = {2009},
    BOOKTITLE = {Proceedings of Communicating Process Architectures 2009, Eindhoven, Netherlands},
    PUBLISHER = {IOS Press},
    URL = {https://lvl.info.ucl.ac.be/Publications/CombiningPartialOrderReductionWithBoundedModelChecking},
  }
  @INPROCEEDINGS{lvl-2009-4,
    TITLE = {A Bisimulation-Based Approach to the Analysis of Human-Computer Interaction},
    AUTHOR = {Sébastien Combéfis and Charles Pecheur},
    YEAR = {2009},
    PAGES =  {101--110},
    BOOKTITLE = {ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2009, Pittsburgh, PA},
    PUBLISHER = {ACM},
    EDITOR = {G. Calvary and {T. N.} Graham and P. Gray},
    URL = {https://lvl.info.ucl.ac.be/Publications/ABisimulation-BasedApproachToTheAnalysisOfHuman-ComputerInteraction},
  }
  @INPROCEEDINGS{lvl-2009-1,
    TITLE = {A Formal Analysis of Requirements-Based Testing},
    AUTHOR = {Charles Pecheur and Franco Raimondi and Guillaume Brat},
    YEAR = {2009},
    EDITOR = {ACM},
    URL = {https://lvl.info.ucl.ac.be/Publications/AFormalAnalysisOfRequirements-BasedTesting},
  }
  @INPROCEEDINGS{lvl-2009-2,
    TITLE = {PDVer, a Tool to Verify PDDL Planning Domains},
    AUTHOR = {Franco Raimondi and Charles Pecheur and Guillaume Brat},
    YEAR = {2009},
    BOOKTITLE = {Proceedings of ICAPS'09 Workshop on Verification and Validation of Planning and Scheduling Systems, Thessaloniki, Greece},
    URL = {https://lvl.info.ucl.ac.be/Publications/PDVerAToolToVerifyPDDLPlanningDomains},
  }
  @INPROCEEDINGS{lvl-2009-5,
    TITLE = {Operational Model: Integrating User Tasks and Environment Information with System Model},
    AUTHOR = {Sébastien Combéfis},
    YEAR = {2009},
    BOOKTITLE = {3rd International Workshop on Formal Methods for Interactive Systems (FMIS 2009), Eindhoven, Netherlands},
    NOTE = {Short paper},
    URL = {https://lvl.info.ucl.ac.be/Publications/OperationalModelIntegratingUserTasksAndEnvironmentInformationWithSystemModel},
  }
  @INPROCEEDINGS{lvl-2008-1,
    TITLE = {Efficient Symbolic Model Checking for Process Algebras},
    AUTHOR = {José {Vander Meulen} and Charles Pecheur},
    YEAR = {2008},
    VOLUME = {5596},
    BOOKTITLE = {Proceedings of 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), L'Aquila, Italy},
    PUBLISHER = {Springer},
    SERIES = {LNCS},
    URL = {https://lvl.info.ucl.ac.be/Publications/EfficientSymbolicModelCheckingForProcessAlgebras},
  }
  @INPROCEEDINGS{lvl-2007-1,
    TITLE = {Testing Planning Domains (without Model Checkers)},
    AUTHOR = {Franco Raimondi and Charles Pecheur and Guillaume Brat},
    YEAR = {2007},
    BOOKTITLE = {Third Workshop on Model-Based Testing (MBT 2007), Braga, Portugal},
    URL = {https://lvl.info.ucl.ac.be/Publications/TestingPlanningDomainsWithoutModelCheckers},
  }
  @INPROCEEDINGS{lvl-2007-3,
    TITLE = {Symbolic Model Checking of Logics with Actions},
    AUTHOR = {Charles Pecheur and Franco Raimondi},
    YEAR = {2007},
    VOLUME = {4428},
    BOOKTITLE = {Workshop on Model Checking and Artificial Intelligence (MOCHART), Riva del Garda, Italy, 29 Aug 2006},
    EDITOR = {Springer},
    SERIES = {LNAI},
    URL = {https://lvl.info.ucl.ac.be/Publications/SymbolicModelCheckingOfLogicsWithActions},
  }
  @INPROCEEDINGS{lvl-2007-2,
    TITLE = {Automatic Verification of Knowledge and Time with NuSMV},
    AUTHOR = {Alessio Lomuscio and Charles Pecheur and Franco Raimondi},
    YEAR = {2007},
    BOOKTITLE = {20th International Joint Conference on Artificial Intelligence (IJCAI-07), Hyderabad, India},
    URL = {https://lvl.info.ucl.ac.be/Publications/AutomaticVerificationOfKnowledgeAndTimeWithNuSMV},
  }
  @INCOLLECTION{lvl-2006-1,
    TITLE = {Formal Verification of Autonomy Models: From Livingstone to SMV},
    AUTHOR = {Charles Pecheur and Reid Simmons and Peter Engrand},
    YEAR = {2006},
    BOOKTITLE = {Agent Technology from a Formal Perspective},
    PUBLISHER = {Springer Verlag},
    EDITOR = {Rouff and C. and Hinchey and M. and Rash and J. and Truszkowski and W. and Gordon-Spears and D.},
    SERIES = {NASA Monographs in Systems and Software Engineering},
    URL = {https://lvl.info.ucl.ac.be/Publications/FormalVerificationOfAutonomyModelsFromLivingstoneToSMV},
  }
  @INPROCEEDINGS{lvl-2005-1,
    TITLE = {Applications of model checking for multi-agent systems: verification of diagnosability and recoverability},
    AUTHOR = {Franco Raimondi and Charles Pecheur and Alessio Lomuscio},
    YEAR = {2005},
    BOOKTITLE = {Proceedings of Concurrency Specification and Programming (CSP 2005), Ruciane-Nida, Poland},
    URL = {https://lvl.info.ucl.ac.be/Publications/ApplicationsOfModelCheckingForMulti-agentSystemsVerificationOfDiagnosabilityAndRecoverability},
  }
  @INCOLLECTION{lvl-2005-2,
    TITLE = {Verification and Validation and Artificial Intelligence},
    AUTHOR = {Tim Menzies and Charles Pecheur},
    YEAR = {2005},
    BOOKTITLE = {Advances in Computers, vol. 65},
    PUBLISHER = {Elsevier},
    EDITOR = {M. Zelkowitz},
    URL = {https://lvl.info.ucl.ac.be/Publications/VerificationAndValidationAndArtificialIntelligence},
  }