Loading...
Share this Job

Stage: Interprétation abstraite de programmes Scade

Apply now »

Date: Mar 23, 2021

Location: Toulouse, FR, 31100

Company: Ansys

Ansys is the global leader in engineering simulation, helping the world's most innovative companies deliver radically better products to their customers. By offering the best and broadest portfolio of engineering simulation software, Ansys helps companies solve the most complex design challenges and engineer products limited only by imagination.

 

Contexte

Dans le cadre de son activité d’édition logicielle d’outils d’aide à la conception de systèmes embarqués critiques, Ansys propose de participer à l’étude de faisabilité d’un analyseur statique du comportement numérique d’une application réalisée avec le langage Scade. Le cadre théorique de cette étude est celui de l’interprétation abstraite et un prototype sera réalisé en OCaml.

Mots-clés : Scade, interprétation abstraite, simulation abstraite, domaines numériques abstraits, OCaml

Sujet

Ce stage a pour objectif l’étude d’un cadre théorique et le prototypage d’un outil dédié à l’analyse du comportement numérique des programmes Scade. Scade est un langage synchrone à flots de données ; il est fondé sur le langage Lustre (inventé par Paul Caspi et Nicolas Halbwachs). Scade est principalement utilisé dans la conception de systèmes embarqués critiques.

L’objectif est de caractériser les domaines des calculs arithmétiques dans un programme Scade en fonction des domaines de définition des entrées qui lui sont choisis.

Le domaine des intervalles et les principes d’analyse avant et d’analyse arrière serviront de support initial afin de couvrir les constructions du langage. Ce cadre sera ensuite étendu à d’autres domaines abstraits garantissant un bon compromis performance/précision, tels que l’arithmétique affine.

Les productions attendues pour le stage sont :

  • La formalisation d’une sémantique abstraite de la partie du langage Scade considérée,
  • un prototype (en OCaml) destiné à l’interprétation et la simulation abstraite de programmes Scade suivant les principes formalisés et
  • un benchmark représentatif permettant de comparer les domaines numériques abordés.

Profil

  • Master ou école d’ingénieurs en informatique
  • Connaissances requises : OCaml
  • Un goût prononcé pour la programmation

Durée du stage

4 à 6 mois

Bibliographie

  1. J.L. Colaço and al., Scade 6: A Formal Language for Embedded Critical Software Development, 2017
  2. P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, 1977
  3. A. Mine, Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation, 2017
  4. M. Pelleau and al., A Constraint Solver Based on Abstract Domains, 2013
  5. J. Stolfi, L. Figueiredo, An Introduction to Affine Arithmetic, 2003
  6. K. Ghorbal, Static Analysis of Numerical Programs: Constrained Affine Sets Abstract Domain, 2011
  7. F. Benhamou and al., Revising hull and box consistency, 1999

 

CULTURE AND VALUES
Culture and values are incredibly important to Ansys. They inform us of who we are, of how we act. Values aren't posters hanging on a wall or about trite or glib slogans. They aren't about rules and regulations. They can't just be handed down the organization. They are shared beliefs – guideposts that we all follow when we're facing a challenge or a decision. Our values tell us how we live our lives; how we approach our jobs. Our values are crucial for fostering a culture of winning for our company:

  • Customer focus
  • Results and Accountability
  • Innovation
  • Transparency and Integrity
  • Mastery
  • Inclusiveness
  • Sense of urgency
  • Collaboration and Teamwork

 
WORKING AT ANSYS
At Ansys, you will find yourself among the sharpest minds and most visionary of leaders, collectively aiming to change the world with innovative technology and remarkable solutions.  With the prestigious reputation in servicing well-known, world-class companies, standards at Ansys are high, met by those willing to rise to the occasion and meet those challenges head-on.  Because at Ansys, it’s about the learning, the discovery and the collaboration.  It’s about the “what’s next” as much as the “mission accomplished”.  It’s about the melding of disciplined intellect with strategic direction and results that have, can and will impact real people in real ways, forged within a working environment built on respect, autonomy and ethics.
 
At Ansys, you will find yourself among those eager to drive the world towards the next best thing with hands planted firmly on the wheel.
Our team is passionate about pushing the limits of world-class simulation technology so our customers can turn their design concepts into successful, innovative products faster and at lower cost.  As a measure of our success in attaining these goals, Ansys has been recognized as one of the world's most innovative companies by prestigious publications such as Bloomberg Businessweek and FORTUNE magazines.
 
Ansys is an S&P 500 company and a component of the NASDAQ-100.
 
For more information, please visit us at www.ansys.com
 
Ansys is an Equal Opportunity Employer. All qualified applicants will receive consideration for employment without regard to race, color, religion, sex, sexual orientation, gender identity, national origin, disability, veteran status, and other protected characteristics.
 
Ansys does not accept unsolicited referrals for vacancies, and any unsolicited referral will become the property of Ansys.  Upon hire, no fee will be owed to the agency, person, or entity.