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.
http://doi.ieeecomputersociety.org/10.1109/HASE.2010.15


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 (http://www.laas.fr/TSF-EN/). Work will be done in collaboration with ONERA (http://www.onera.fr/dtim-en/critical-systems/index.php). 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.

Qualifications

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

Application

Candidates should send a resume and recommendation letters via email to: Helene.Waeselynck@laas.fr and Virginie.Wiels@onera.fr

--------------------------------------------------------------
Helene Waeselynck           E-mail: Helene.Waeselynck@laas.fr
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            http://homepages.laas.fr/waeselyn/
--------------------------------------------------------------

Comments

  1. Though my writing skill is good my paragraph is not enough. I have observed lots of sites to get tricks but not satisfied. The verbose sentence generator is really requisite for my writing to make the sentence longer. http://www.academicghostwriter.org/academic-writing-services/ finding the review about these apps are also worthy.

    ReplyDelete
  2. When I go for submitting the resume to requisition in any company. They always look the best MBA marketing programs but I couldn't clear on this topic before knowing here. This information helps me to achieve the best marketing MBA degree ever in my life. This process should be ranked top for all. http://www.reactionpaper.net/our-professional-response-writing-help/ for more information just take a look here maybe you will get some best information.

    ReplyDelete
  3. I want to do my MBA in this season. But I don't know which is suitable for me to grow my career. Perhaps Physician Assistant programs may be demandable to take me in higher place. Now I decided to take this program as my career. http://www.personalstatementpsychology.com/all-about-the-social-psychology-personal-statement-writing/ take a look back on this site to get desirable info about PA program.

    ReplyDelete
  4. Direction is the course toward discernment and finding a few solutions concerning everything that we use in our well ordered life combine our mentality with various individuals. You can try this to get new ideas. Direction is just a singular factor that influence encourage or roundabout on our life.

    ReplyDelete
  5. Good post, On the off chance that the understudy have beginning at now data about any area, it will be essential for them to comprehend the course without burden. Check this nursingpaper.com site to manage your work. We give an emerge association material in each game plan.

    ReplyDelete

Post a Comment

Popular posts from this blog

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  https://oat.uwaterloo.ca/forms   and 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 Hardware Adding a Joint CS to an out-of-faculty plan Transfer 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).

Grad students needed to mark reports for PD2

WatPD is currently seeking graduate students to mark reports for PD2: Critical Reflection and Report Writing from late-March to early-April. Students in this course must write a 16-20 page report which is worth 50% of their final grade. With over 1500 reports expected to be submitted, we need your help! Strong candidates for this position will have: ·          a desire to support students in an online learning environment ·          previous marking and/or teaching experience (preferably post-secondary) ·          strong written communication skills ·          an ability to correct quality of writing errors ·          a good understanding of English grammar and syntax To be eligible for this position, you must be available for training sessions in March that are held on campus at the University of Waterloo. Those who demonstrate a high level of competence will be offered additional marking opportunities. Successful candidates will be given about 20-30 hours ov

Radix Trading - opportunities

RADIX TRADING - QUANTITATIVE TECHNOLOGIST WaterlooWorks ID: 78067 Deadline 11PM FRIDAY, SEPT 21 http://radix-trading.com/ Radix Trading is a research-­driven, proprietary trading startup (~50 people) in Chicago and Amsterdam led by Michael Rauchman and Ben Blander.  -------------------------- Michael Rauchman - formerly GETCO's CTO, head of Americas equities, and global head of ForEx. As a hands-on leader, Michael was instrumental in the development of many trading strategies as well as the underlying architecture and code. Ben Blander - former head of Citadel’s high frequency group and a key contributor in growing their P&L from $75 million in 2005 to $1.15 billion in 2008 (Source: http://www.cnbc.com/id/39099331 )  Previously Ben earned a PhD in Math from the University of Chicago. Our culture of openness (you'd have complete access to our code, data, and strategies) enables fast turnaround from idea inception to execution, and continuous enhancem