Rich Counter-Examples for Temporal-Epistemic Logic Model Checking - Simon Busard; Charles Pecheur (IWIGP, 2012)

PyNuSMV: NuSMV as a Python Library. - Simon Busard; Charles Pecheur (NASA Formal Methods, 2013)

Reasoning about Strategies under Partial Observability and Fairness Constraints - Simon Busard; Charles Pecheur; Hongyang Qu 001; Franco Raimondi (SR, 2013)

Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints. - Simon Busard; Charles Pecheur; Hongyang Qu 001; Franco Raimondi (ICFEM, 2014)

Verification of railway interlocking systems. - Simon Busard; Quentin Cappart; Christophe Limbrée; Charles Pecheur; Pierre Schaus (ESSS, 2015)

Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. - Simon Busard; Charles Pecheur; Hongyang Qu 001; Franco Raimondi (Inf. Comput., 2015)

A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability. - Simon Busard; Charles Pecheur (GandALF, 2017)

Symbolic model checking of multi-modal logics: uniform strategies and rich explanations. - Simon Busard (2017)

Producing Explanations for Rich Logics. - Simon Busard; Charles Pecheur (FM, 2018)

Comparing approaches for model-checking strategies under imperfect information and fairness constraints. - Simon Busard; Charles Pecheur; Hongyang Qu 001; Franco Raimondi (Int. J. Softw. Tools Technol. Transf., 2019)

Verification of Scenario-based Behavioural Models using Capella and PyNuSMV. - Simon Busard; Christophe Ponsard; Charles Pecheur (MODELSWARD, 2021)