Members

Charles Pecheur

Contact Information

Charles Pecheur
Professor, LVL Group Lead
UCL / EPL / ICTEAM / INGI
Place Sainte Barbe, 2
1348 Louvain-la-Neuve
Belgium

Office: Réaumur A.211 (2nd floor)
Phone: +32 10 47 87 79
Fax: +32 10 45 03 45
Email: Charles [period] Pecheur [snail] uclouvain [period] be

Biography

Charles Pecheur is professor in the Dept. Computer and Software Engineering at Université catholique de Louvain in Belgium. He is interested in formal methods and automated verification, and related aspects of software engineering. He was born in Liège, Belgium, and lived and studied there until he obtained my PhD from Université de Liège. Then he went on a post-doctoral fellowship at INRIA in Grenoble, France, before he crossed the Atlantic to join the Automated Software Engineering Group at NASA Ames in California. He came back to Belgium and Louvain-la-Neuve in 2004. He is married and father of two.

Courses

LFSAB1401 - Informatique 1 (2005-...)
LSINF1101 - Introduction à la Programmation (2012-...)
LFSAB1501 - Projet 1 (2005-...)
LSINF2224 - Programming Methods (2004-...)
LINGI2143 - Concurrent Systems: Models and Analysis (2007-...)
LINGI2264 - Automated Reasoning (2008-...)

Former Home Pages

For publications and talks before 2005, see Charles Pecheur's former UCL home page

Publications

A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railway. Christophe Limbrée, Charles Pecheur. .
A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability. Simon Busard, Charles Pecheur. Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, Roma, Italy, 20-22 September 2017.
Verification of railway interlocking - Compositional approach with OCRA. Christophe Limbrée, Quentin Cappart, Charles Pecheur, Stefano Tonetta ?. Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification.
Automatic Detection of Potential Automation Surprises for ADEPT Models. Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur. IEEE Transactions on Human-Machine Systems.
Tasks Decomposition of System Models for Human-Machine Interaction Analysis. Guillaume Maudoux, Sébastien Combéfis, Charles Pecheur. Proceedings of the Workshop on Formal Methods for Human Computer Interaction 2015.
Verification of railway interlocking systems. Simon Busard, Quentin Cappart, Christophe Limbrée, Charles Pecheur, Pierre Schaus. Proceedings 4th International Workshop on Engineering Safety and Security Systems, Oslo, Norway, June 22, 2015.
Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi. Information and Computation.
Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints. Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi. Formal Methods and Software Engineering.
A Methodology for Analyzing Human-Automation Interactions in Flight Operations Using Formal Verification Techniques. Denis Javaux, Bertram Wortelen, Andreas Lüdtke, Charles Pecheur, Regina Peldszus, Sonja Sievi, Yuri Yushtein. Proceedings of AAAI Symposium on Formal Verification in Human-Machine Systems.
State Event Models for the Formal Analysis of Human-Machine Interactions. Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur. Proceedings of AAAI Symposium on Formal Verification in Human-Machine Systems.
Formal Methods for Industrial Critical Systems, 18th International Workshop (FMICS 2013). Charles Pecheur, Michael Dierkes (Eds.). Springer.
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, Franco Raimondi. Proceedings 1st International Workshop on Strategic Reasoning, Rome, Italy, March 16-17, 2013.
Rich Counter-Examples for Temporal-Epistemic Logic Model Checking. Simon Busard, Charles Pecheur. Proceedings Second International Workshop on Interactions, Games and Protocols, Tallinn, Estonia, 25th March 2012.
A JavaPathfinder Extension to Analyse Human-Machine Interactions. Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur, Peter Mehlitz. Java Pathfinder Workshop 2011.
Learning System Abstractions for Human Operators. Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur, Michael Feary. International Workshop on Machine Learning Technologies in Software Engineering.
A Formal Framework for Design and Analysis of Human-Machine Interaction. Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur, Michael Feary. 2011 IEEE International Conference on Systems, Man, and Cybernetics.
Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction. José Vander Meulen, Charles Pecheur. NASA FORMAL METHODS 2011.
Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties. José Vander Meulen, Charles Pecheur . NASA FORMAL METHODS 2011.
25th IEEE-ACM International Conference on Automated Software Engineering. Charles Pecheur, Jamie Andrews, Elisabetta Di Nitto (Eds.). ACM.
A Bisimulation-Based Approach to the Analysis of Human-Computer Interaction. Sébastien Combéfis, Charles Pecheur. ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2009, Pittsburgh, PA.
A Formal Analysis of Requirements-Based Testing. Charles Pecheur, Franco Raimondi, Guillaume Brat. 2009 International Conference on Software Testing and Analysis (ISSTA), Chicago, IL.
PDVer, a Tool to Verify PDDL Planning Domains. Franco Raimondi, Charles Pecheur, Guillaume Brat. Proceedings of ICAPS'09 Workshop on Verification and Validation of Planning and Scheduling Systems, Thessaloniki, Greece.
Combining Partial Order Reduction with Bounded Model Checking. José Vander Meulen, Charles Pecheur. Proceedings of Communicating Process Architectures 2009, Eindhoven, Netherlands.
Efficient Symbolic Model Checking for Process Algebras. José Vander Meulen, Charles Pecheur. Proceedings of 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), L'Aquila, Italy.
Symbolic Model Checking of Logics with Actions. Charles Pecheur, Franco Raimondi. Workshop on Model Checking and Artificial Intelligence (MOCHART), Riva del Garda, Italy, 29 Aug 2006.
Automatic Verification of Knowledge and Time with NuSMV. Alessio Lomuscio, Charles Pecheur, Franco Raimondi. 20th International Joint Conference on Artificial Intelligence (IJCAI-07), Hyderabad, India.
Testing Planning Domains (without Model Checkers). Franco Raimondi, Charles Pecheur, Guillaume Brat. Third Workshop on Model-Based Testing (MBT 2007), Braga, Portugal.
Formal Verification of Autonomy Models: From Livingstone to SMV. Charles Pecheur, Reid Simmons, Peter Engrand. Agent Technology from a Formal Perspective.
Verification and Validation and Artificial Intelligence. Tim Menzies, Charles Pecheur. Advances in Computers, vol. 65.
Applications of model checking for multi-agent systems: verification of diagnosability and recoverability. Franco Raimondi, Charles Pecheur, Alessio Lomuscio. Proceedings of Concurrency Specification and Programming (CSP 2005), Ruciane-Nida, Poland.

Talks

Computer Science and Proof: a Brief History of Automated Reasoning. Charles Pecheur. seminar series Fondements et Notions Fondamentales, UCL, 12 Mar 2012.
Learning System Abstractions for Human Operators. Charles Pecheur. MALETS Workshop, Lawrence, KA, USA, Nov 12, 2011.
Verification of Embedded Software: from Mars to Actions. Charles Pecheur. Seminar at Xerox PARC, Jul 31, 2009, derived from FMICS 2007.
Model Checking for Software. Charles Pecheur. Tutorial for MOVES meeting, June 2008.
Testing Planning Domains (without Model Checkers). Charles Pecheur. MBT Workshop, Braga, Portugal, Mar 31, 2007.
Verification of Embedded Software: from Mars to Actions. Charles Pecheur. Invited Talk at FMICS 2007, June 1, 2007.
Guided Simulation of Autonomous Controllers. Charles Pecheur. Dagstuhl seminar on Directed Model Checking, Dagstuhl, Germany, May 2006.
Symbolic Model Checking of Logics with Actions. Charles Pecheur. MOCHART Workshop, Riva del Garda, Italy, Aug 29, 2006.
Verification of Intelligent Controllers using Model Checking. Charles Pecheur. Invited Talk at ASTRA 2006, Nov 2006.

Tags: Verification, Autonomous Systems, Symbolic Model Checking, Epistemic Logic, Coverage Criteria

Find It

Louvain Verification Lab