Share this Job

Stage de fin d'études recherche et dévelopement Ocaml H/F

Apply now »

Date: Nov 15, 2022

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.

 

Interprétation abstraite de programmes Scade
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 permettant d'étudier le 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 ; un prototype existant, réalisé en OCaml, sera étendu et complété afin de couvrir l'ensemble du langage Scade.
Mots-clés : Scade, interprétation abstraite, domaines numériques abstraits, langages formels, 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 une extension du 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 valeurs prises par les flots (locaux, sorties) d'un programme Scade en fonction des domaines de définition des entrées qui lui sont choisis.
Le domaine des intervalles, de l'arithmétique affine et les principes d’analyse avant et d’analyse arrière serviront de support initial afin de couvrir les constructions du langage. 
La première partie de l’étude consistera en l'extension d'un prototype existant [9], afin de couvrir les structures haut-niveau de contrôle (machines à états), et d'itérations sur les tableaux.
Dans un second temps, le stage portera sur l'ajout de moyens permettant de spécifier le comportement abstrait d'un opérateur. Cette extension servira d'une part pour les opérateurs importés dont la définition échappe à l'analyse et d'autre part pour des opérateurs définis en Scade mais pour lesquels nous disposons comportement abstrait plus précis que celui déduit automatiquement.
Les productions attendues pour le stage sont :
•    un prototype (en OCaml ) d'un analyseur statique pour le langage Scade couvrant l'ensemble des constructions et permettant d'injecter un comportement abstrait spécifique pour des opérateurs du programme à analyser,
•    une illustration des travaux sur un jeu d’exemples permettant d'apprécier les performances du prototype et la qualité des résultats retournés.
Profil
•    Master ou école d’ingénieurs en informatique
•    Connaissances requises : OCaml
•    Un goût prononcé pour la programmation
Durée du stage
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
8.    O. Bouissou and al., HySon : Set-based simulation of hybrid systems, 2012
9.    P. Vantalon : Abstract interpretation of Scade programs, 2021
10.    A. Auvolat, J.L. Colaço : Étude de l'analyse statique de programmes synchrones par interprétation abstraite, 2014
 
 
 
Summary of the internship in English:
This internship aims to study a theoretical framework and the prototyping of a tool dedicated to the analysis of the digital behavior of Scade programs. Scade is a synchronous data-flow language;
it is based on an extension of the Lustre language (invented by Paul Caspi and Nicolas Halbwachs). Scade is mainly used in the design of critical embedded systems.
The objective is to characterize the domains of values ​​taken by the flows (local, outputs) of a Scade program according to the domains of definition of the inputs which are chosen for it.
The domain of intervals, affine arithmetic and the principles of forward parsing and backward parsing will serve as initial support in order to cover the constructions of the language.
The first part of the study will consist of the extension of an existing prototype, in order to cover the high-level control structures (state machines), and iterations on the arrays.
In a second time, the internship will relate to the addition of means allowing to specify the abstract behavior of an operator. This extension will be used on the one hand for imported operators whose definition
escapes analysis and on the other hand for operators defined in Scade but for which we have more precise abstract behavior than that deduced automatically.
The expected productions for the internship are:
- a prototype (in OCaml) of a static analyzer for the Scade language covering all constructions and allowing to inject a specific abstract behavior for operators of the program to be analyzed,
- an illustration of the work on a set of examples to assess the performance of the prototype and the quality of the results returned.
Profile:
Master or engineering school in computer science
Required knowledge:
OCaml
A strong taste for programming
Training period: 6 months

 

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.