Skip to main content

Post-doc position in LAAS-CNRS, Toulouse (model checking & testing)

Post-doc position on
Structural analysis of counterexamples

A key issue in model checking is how to locate faults that caused property violation, when a lengthy counterexample is returned. Previous work done in collaboration with Airbus [Boc10] has addressed this issue in the framework of Scade or Simulink design models. The approach is based on a structural analysis that identifies paths of the model that are activated by a counterexample over time. This analysis allows the extraction of relevant information to explain the observed violation. It may also serve to guide the model checker toward the search for different counterexamples, exhibiting new path activation patterns and thus new ways to violate the property. The aim is to give engineers as much usable feedback as possible before a fix is attempted. The approach has been implemented in a tool called STANCE (Structural ANalysis of CounterExamples). It is closely related to path-based analysis techniques developed for structural testing.

The objective of this post-doc is to further elaborate the approach. A first direction concerns the extraction of explanatory information from the execution of a counterexample. The current algorithm focuses on the traversal Boolean and temporal operators. Work will consider an extension to handle numerical operators as well. A second direction is on the definition and comparison of strategies for obtaining new counterexamples. The simple strategy implemented in STANCE provided a first assessment of the feasibility and potential interest of the idea. A systematic investigation of more elaborated path-based strategies is now needed, with possibly a combination of symbolic and heuristic techniques.

[Boc10] T. Bochot, P. Virelizier, H. Waeselynck, V. Wiels. Paths to Property Violation: A Structural Approach for Analyzing Counter-Examples. In Proc. HASE 2010.

Practical information

The post-doctoral position is funded by RTRA STAE, the French space and aeronautic sciences & technologies foundation, as part of the IFSE project on formal system engineering. It is located in Toulouse, a nice city in the heart of Southern France. Toulouse is famous for its aeronautical and space achievements, its university founded in 1229, its laboratories and research centers.

The position is open at LAAS-CNRS, in the "Dependable Computing and Fault Tolerance" Group ( Work will be done in collaboration with ONERA ( Gross salary is between 2500 and 3000 euros per month. Post-doc will start between September and December 2013 for a duration of one year.


PhD in computer science.
Expertise in model checking or testing techniques necessary.
Knowledge of Scade/Simulink or more generally data flow languages welcome.


Candidates should send a resume and recommendation letters via email to: and

Helene Waeselynck           E-mail:
LAAS-CNRS                   tel: +33 (0)5 61 33 64 07
7, Av du Colonel Roche      fax: +33 (0)5 61 33 64 11
F-31400 Toulouse  


Popular posts from this blog

Enrollment caps have been restored for CS courses

As per the course selection policy, enrollment caps for all CS courses have been returned to their actual class size. If the class or section is full then it means that you will need to wait for another student to drop it. You have until 11.59 p.m. on Monday May 14 to add courses.

The following courses still have waiting lists and department consent applied so you will NOT be able to add these courses.

CS 454CS 458CS 486CS 488CS 492

Course enrollment for Spring 2018

Appointments for course enrollment began on Monday 26 March and open enrollment begins on Wednesday 28 March.

For students trying to add CS courses, we encourage you to review the course selection page.

In Computer Science,  we drop the enrolment caps by approximately 15% of the total enrolment number for the course to give advisors room to handle special cases. We will return the enrolment caps to their actual size in the second week of classes after we have had time to deal with the special cases. This will occur on Friday, May 4, 2018, (we don't know the precise time) and remaining space will be available on a first-come-first-served basis only if the section isn't already at its enrolment total. WHAT IS A SPECIAL CASE?
1. Students who selected courses but something went wrong because of: enrollment capacity in a course **a time conflict **an academic enrolment block was applied after course selectiondropping or failing a course after course selection** Please re…

CS/Data Science/Digital Hardware option transfers NOW OPEN

The CS Undergraduate Advising Office has opened applications for CS transfers for Fall 2017. The online application is available at will be open from Tuesday, December 5 until Sunday, December 31, 2017, at 11.59 p.m.

We're accepting applications for:

Transfer from Math to CS - at a minimum, must have taken CS 136 or be taking it in Fall 2017.Transfer from CS to BCS (Data Science) - must have taken STAT 231 or be taking it in Fall 2017.Transfer from CS to CS/Digital HardwareAdding a Joint CS to an out-of-faculty planTransfer from outside of Math to CS (pending approval from Math)Answers to common questions about the transfer process can be found in the CS FAQs (particularly #2 and #151).