Charles Pecheur
List of Publications
This page only contains publications from 2009 and before.
Recent publications are found on the LVL
website.
Articles
- José Vander Meulen, Charles Pecheur. Combining
Partial
Order Reduction with Bounded Model Checking.
Proceedings of Communicating
Process Architectures 2009, IOS Press, Nov 2009, Eindhoven,
Netherlands.
- Franco Raimondi, Charles Pecheur, Guillaume Brat. PDVer, a
Tool to Verify PDDL Planning Domains. Proceedings of ICAPS'09 Workshop
on Verification and Validation of Planning and Scheduling
Systems, Sept 2009, Thessaloniki, Greece.
- Charles Pecheur, Franco Raimondi, Guillaume Brat. A Formal
Analysis of Requirements-Based Testing. Proceedings of 2009 International
Conference on Software Testing and Analysis (ISSTA), July
2009, Chicago, IL.
- Sébastien Combéfis, Charles Pecheur. A
Bisimulation-Based Approach to the Analysis of
Human-Computer Interaction. Proceedings of ACM SIGCHI
Symposium on Engineering Interactive Computing Systems (EICS
2009), July 2009, Pittsburgh, PA.
- José Vander Meulen, Charles Pecheur. Efficient
Symbolic
Model Checking for Process Algebras. Proceedings of 13th International
Workshop on Formal Methods for Industrial Critical Systems
(FMICS 2008), September 2008, L'Aquila, Italy.
- Franco Raimondi, Charles Pecheur, Guillaume Brat. Testing Planning Domains (without Model
Checkers). Third Workshop on Model-Based
Testing (MBT 2007), March 31 - April 1, 2007, Braga, Portugal.
- Alessio Lomuscio, Charles Pecheur, Franco Raimondi. Automatic Verification of
Knowledge and Time with NuSMV. In:
Twentieth International Joint Conference on Artificial
Intelligence (IJCAI-07), January 6-12 2007, Hyderabad, India.
- Charles Pecheur, Franco Raimondi. Symbolic
Model
Checking of Logics with Actions. In: Workshop on
Model Checking and Artificial Intelligence (MOCHART), Riva del
Garda, Italy, 29 Aug 2006. Lecture Notes in Artificial
Intelligence, vol. 4428, Springer, 2007.
- Charles Pecheur, Reid Simmons, Peter Engrand. Formal Verification of Autonomy
Models: From Livingstone to SMV. In: Rouff, C.; Hinchey, M.; Rash,
J.; Truszkowski, W.; Gordon-Spears, D. (Eds.), Agent
Technology from a Formal Perspective, NASA Monographs in
Systems and Software Engineering, Springer Verlag, 2006.
- Franco Raimondi, Charles Pecheur, Alessio Lomuscio. Applications
of
model checking for multi-agent systems: verification of
diagnosability and recoverability. In: Proceedings of Concurrencey
Specification and Programming (CSP 2005), Ruciane-Nida,
Poland, Sep 2005.
- Tim Menzies and Charles Pecheur. Verification and Validation and
Artificial Intelligence. In: M. Zelkowitz, Ed.,
Advances in Computers, vol. 65, 2005, Elsevier.
- Tony Lindsey and Charles Pecheur. Simulation-Based Verification of
Autonomous Controllers with Livingstone PathFinder.
In: Proceedings of
the Tenth International Conference on Tools And Algorithms For
The Construction And Analysis Of Systems (TACAS'04),
Barcelona, Spain, Mar-Apr 2004. Lecture Notes in
Computer Science, vol. 2988, Springer Verlag.
- A.E. Lindsey and Charles Pecheur. Simulation-Based Verification of
Livingstone Applications. Short paper,
Workshop on Model-Checking for Dependable Software-Intensive
Systems, San Francisco, June 2003.
- Alessandro Cimatti, Charles Pecheur, Roberto Cavada. Formal Verification of Diagnosability
via Symbolic Model Checking. Proceedings of
IJCAI'03, Acapulco, Mexico, August 2003.
- Stacy Nelson, Charles Pecheur. Formal
Verification
of a Next-Generation Space Shuttle. In: Second Goddard
Workshop on Formal Aspects of Agent-Based Systems (FAABS II),
Greenbelt, MD, October 2002. Lecture Notes in Computer
Science, vol. 2699, Springer Verlag.
- Charles Pecheur, Alessandro Cimatti. Formal Verification of Diagnosability
via Symbolic Model Checking. Workshop on Model
Checking and Artificial Intelligence (MoChArt-2002), Lyon,
France, July 22/23, 2002.
- Steven Brown, Charles Pecheur. Model-Based Verification
of Diagnostic Systems. Proceedings of JANNAF
Joint Meeting, Destin, FL, April 8-12, 2002.
- Reid Simmons, Charles Pecheur, Grama Srinivasan. Towards Automatic
Verification of Autonomous Systems. In:
Proceedings of the 2000 IEEE/RSJ International Conference on
Intelligent Robots and Systems, IEEE, 2000.
- Klaus Havelund, Mike Lowry, SeungJoon Park, Charles Pecheur,
John Penix, Willem Visser, Jon L. White. Formal
Analysis of the Remote Agent Before and After Flight.
In: Proceedings of 5th NASA Langley Formal Methods Workshop,
Williamsburg, Virginia, 13-15 June 2000.
- Charles Pecheur, Reid Simmons. From Livingstone to SMV:
Formal Verification for Autonomous Spacecrafts.
In:Proceedings of First Goddard Workshop on Formal Approaches
to Agent-Based Systems, NASA Goddard, April 5-7, 2000. Lecture
Notes in Computer Science, vol. 1871, Springer Verlag.
- Reid Simmons, Charles Pecheur. Automating Model Checking for
Autonomous Systems. Proceedings of AAAI Spring
Symposium on Real-Time Autonomous Systems, Stanford, March
20-22, 2000.
- Daniel Clancy, William Larson, Charles Pecheur, Peter
Engrand, Charles Goodrich. Autonomous
Control of an in-Situ Propellant Production Plant. In:
Proceedings
of the Technology 2009 National Conference, Miami Beach, FL,
November 1-3, 1999.
- Anthony R. Gross, K. R. Sridhar, William E. Larson, Daniel J.
Clancy, Charles Pecheur, and Geoffrey A. Briggs. Information Technology and Control Needs for
In-Situ Resource Utilization. In: Proceedings of
the 50th IAF Congress, Amsterdam, 4-8 October 1999.
- Charles Pecheur. Advanced
Modelling and Verification Techniques Applied to a Cluster
File System. In: Proceedings of the 14th IEEE
International Conference on Automated Software Engineering,
Cocoa Beach, Florida, October 1999. Extended version in: INRIA Research Report RR-3416, May
1998.
- John Penix, Charles Pecheur and Klaus Havelund. Using Model Checking to Validate AI
Planner Domain Models. In:
Proceedings of the 23rd Annual Software Engineering Workshop,
NASA Goddard, December, 1998.
- Charles Pecheur. Specification and
Validation of the CO4 distributed knowledge system using
LOTOS. in: Proceedings of the 12th IEEE
International Conference on Automated Software Engineering,
Incline Village, Nevada, November 1997. Extended version in: INRIA Research Report RR-3259,
September 1997.
- Hubert Garavel, Mark Jorgensen, Radu Mateescu, Charles
Pecheur, Mihaela Sighireanu, Bruno Vivien. CADP'97 --
Status, Applications and Perspectives.In: Ignac
Lovrek (ed.), Proceedings of the 2nd COST 247 International
Workshop on Applied Formal Methods in System Design (Zagreb,
Croatia), June 1997.
- G. Leduc, O. Bonaventure, L. Leonard, E. Koerner, C. Pecheur.
Model-Based Verification of a Security Protocol for the
Conditional Access to Services. Formal Methods in
System Design, Vol. 14, nr 2, March 1999, pp 171-191.
- G. Leduc , O. Bonaventure, E. Koerner, L. Léonard, C.
Pecheur, D. Zanetti. Specification and
verification of a TTP protocol for the conditional access to
services. In: Proceedings of 12th J. Cartier
Workshop. Formal Methods and their Applications:
Telecommunications, VLSI and Real-Time Computerized Control
System, Montreal, Canada, 2-4 Oct. '96.
- Charles Pecheur. VLib: Infinite virtual
libraries for LOTOS. In: A. Danthine, G. Leduc,
P. Wolper (eds.) Proceedings of the IFIP TC6/WG6.1 Thirteenth
International Symposium on Protocol Specification, Testing and
Verification, Liège, Belgium, 25-28 May, 1993 Elsevier
Science Publishers BV (North Holland), 1993, pp 29-44.
- Charles Pecheur. Using LOTOS for
Specifying the CHORUS Distributed Operating System Kernel. In:
Computer
Communications Vol. 15, nr 2, March 1992, pp 93-102.
- Charles Pecheur. Spécification de Systèmes
d'Exploitation en LOTOS: l'Expérience CHORUS. In:
CFIP'91
Ingénierie
des Protocoles, Omar Rafiq (ed.), Hermès, Paris, 1991,
pp. 405-424.
PhD Thesis
- Charles Pecheur. Improving the Specification of Data
Types in LOTOS. Doctorate Thesis, Collection des
Publications de la FSA No. 171, University of Liège,
1996. Abstract.
Selected Technical Reports
- Tony Lindsey, Charles Pecheur. Simulation-Based Verification of a
Propulsion Feed Subsystem via Livingstone PathFinder. RIACS Technical Report 03.11, RIACS,
USRA, September 2003.
- Cavada, Roberto and Pecheur, Charles. Practical Formal Verification
of Diagnosability of Large Models via Symbolic Model
Checking. Technical Report TR03.03, RIACS, USRA,
January 2003.
- Stacy Nelson, Charles Pecheur. NASA processes/methods
applicable to IVHM V&V. Project
report, 2nd Gen RLV Program, NRA 8-30/TA-5/Northrop
Grumman/ARC Task 10. Oct 2001. Available as
NASA/CR-2002-211401, April 2002.
- Stacy Nelson, Charles Pecheur. Methods for V&V of IVHM
intelligent systems. Project report, 2nd Gen RLV
Program, NRA 8-30/TA-5/Northrop Grumman/ARC Task 10. Jan 2002.
Available as NASA/CR-2002-211402, April 2002.
- Stacy Nelson, Charles Pecheur. Diagnostic Model V&V
Plan/Methods for DME. Project report, 2nd Gen
RLV Program, NRA 8-30/TA-5/Northrop Grumman/ARC Task 10. Jan
2002. Available as NASA/CR-2002-211403, April 2002.
- Charles Pecheur. Verification
and Validation of Autonomy Software at NASA.
NASA/TM 2000-209602, August 2000.
- Charles Pecheur. A Proposal for
Data Types in E-LOTOS. Annex H of: Working Draft
on Enhancements to LOTOS, ISO JTC1/SC21/WG1/N1349, November
1994.
- Charles Pecheur. APERO Language
Reference Version 1.0. EC-CA Project 0001:76099
Eucalyptus, EUCA/ULG/05, University of Liege, Systèmes
et Automatique, February 1994.
- Charles Pecheur. APERO Tools
User's Guide Version 2.0. EC-CA Project
0001:76099 Eucalyptus, EUCA/ULG/06, University of Liege,
Systèmes et Automatique, February 1994.
Other Publications
- Charles Pecheur, Jamie Andrews, Elisabetta Di Nitto (Eds.). ASE 2010, 25th IEEE/ACM
International Conference on Automated Software Engineering.
Antwerp, Belgium, September 20-24, 2010. Conference proceedings,
ACM 2010.
- Charles Pecheur. Verification of Embedded
Software: From Mars to Actions. Invited
talk (abstract), FMICS 2007, Berlin, Germany, July 2007.
Lecture Notes in Computer
Sciences, vol. 4916, Springer, 2008.
- Charles Pecheur. Verification of
Intelligent Control Software. Presented at
ASTRA'06, Noordwijk, Netherlands, November 2006.
- Charles Pecheur, Willem Visser, Reid Simmons. RIACS
Workshop on the Verification and Validation of Autonomous and
Adaptive Systems. Conference report, AI Magazine, Fall
2001. Also available as NASA/TM-2001-210927, August 2001.
Tutorials
- Stacy Nelson, Michael Whalen, Charles Pecheur. From
Research to Industry: The Role of Software Engineering
Standards. Tutorial presented at the ASE'02 conference,
Edinburgh, UK, September 2002.
- Charles Pecheur, Willem Visser. Model Checking for
Software. Tutorial presented at the ASE'00 conference,
Grenoble, France, 12 September 2000.
- Klaus Havelund, Charles Pecheur, Reid Simmons, Willem Visser.
Software Model Checking Tools and Trends at NASA. Tutorial
presented at Lfm 2000, Williamsburg, Virginia, June 2000.