Share this Job

Stage recherche et dévelopement Ocaml H/F

Apply now »

Date: May 8, 2023

Location: Toulouse, FR, 31100

Company: Ansys

When visionary companies need to know how their world-changing ideas will perform, they close the gap between design and reality with Ansys simulation. For more than 50 years, Ansys software has enabled innovators across industries to push boundaries by using the predictive power of simulation. From sustainable transportation to advanced semiconductors, from satellite systems to life-saving medical devices, the next great leaps in human advancement will be powered by Ansys.

 

Take a leap of certainty … with Ansys.

 

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

 

At Ansys, we know that changing the world takes vision, skill, and each other. We fuel new ideas, build relationships, and help each other realize our greatest potential in the knowledge that every day is an opportunity to observe, teach, inspire, and be inspired. Together as One Ansys, we are powering innovation that drives human advancement.

 

Our Commitments:

  • Amaze with innovative products and solutions
  • Make our customers incredibly successful
  • Act with integrity
  • Ensure employees thrive and shareholders prosper

Our Values:

  • Adaptability: Be open, welcome what’s next
  • Courage: Be courageous, move forward passionately
  • Generosity: Be generous, share, listen, serve
  • Authenticity: Be you, make us stronger

 

Our Actions:

  • We commit to audacious goals
  • We work seamlessly as a team
  • We demonstrate mastery
  • We deliver outstanding results

 

OUR ONE ANSYS CULTURE HAS INCLUSION AT ITS CORE
We believe diverse thinking leads to better outcomes. We are committed to creating and nurturing a workplace that fuels this by welcoming people, no matter their background, identity, or experience, to a workplace where they are valued and where diversity, inclusion, equity, and belonging thrive.


TAKE A LEAP OF CERTAINTY IN YOUR CAREER AT ANSYS

At Ansys, you will find yourself among the sharpest minds and most visionary leaders across the globe. Collectively we strive to change the world with innovative technology and transformational solutions. With a prestigious reputation in working with 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. Our team is passionate about pushing the limits of world-class simulation technology, empowering our customers to turn their design concepts into successful, innovative products faster and at a lower cost.

 

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.” And it’s about the melding of disciplined intellect with strategic direction and results that have, can, and do impact real people in real ways. All this is forged within a working environment built on respect, autonomy, and ethics.
 

CREATING A PLACE WE’RE PROUD TO BE 
Ansys is an S&P 500 company and a member of the NASDAQ-100. We are proud to have been recognized for the following more recent awards, although our list goes on: America’s Most Loved Workplaces, Gold Stevie Award Winner, America’s Most Responsible Companies, Fast Company World Changing Ideas, Great Place to Work Certified (China, Greece, France, India, Japan, Korea, Spain, Sweden, Taiwan, U.K.).

 
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.