Séance de cours

Synthèse des programmes de manipulation de pointeurs sûrs

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Dans cours

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and ...

Description

Cette séance de cours de l'instructeur se concentre sur la synthèse des programmes de manipulation de pointeur de bas niveau sûrs en utilisant la technologie de synthèse de programme. L'exposé présente SuSLik, un synthétiseur de programme qui génère des programmes C sûrs à partir de spécifications logiques, mettant en valeur ses capacités à gérer les structures de données liées. La séance de cours couvre la synthèse déductive des programmes de manipulation de pointeurs, l'utilisation de la logique de séparation et l'application de la logique de séparation synthétique dans l'élaboration de programmes corrects par construction. Des exemples tels que l'échange des valeurs des pointeurs et l'élimination des listes sont démontrés, soulignant l'importance d'une synthèse correcte du programme dans l'élimination des bogues de sécurité de la mémoire.

Enseignant·e

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Source officielle

Proximité ontologique

Informatique théorique

Théorie des langages de programmation: Langage de programmation de haut niveau

Concepts associés (31)

Memory safety

Memory safety is the state of being protected from various software bugs and security vulnerabilities when dealing with memory access, such as buffer overflows and dangling pointers. For example, Java is said to be memory-safe because its runtime error detection checks array bounds and pointer dereferences. In contrast, C and C++ allow arbitrary pointer arithmetic with pointers implemented as direct memory addresses with no provision for bounds checking, and thus are potentially memory-unsafe.

Structure de données

En informatique, une structure de données est une manière d'organiser les données pour les traiter plus facilement. Une structure de données est une mise en œuvre concrète d'un type abstrait. Pour prendre un exemple de la vie quotidienne, on peut présenter des numéros de téléphone par département, par nom, par profession (comme les Pages jaunes), par numéro téléphonique (comme les annuaires destinés au télémarketing), par rue et/ou une combinaison quelconque de ces classements.

Linked data structure

In computer science, a linked data structure is a data structure which consists of a set of data records (nodes) linked together and organized by references (links or pointers). The link between data can also be called a connector. In linked data structures, the links are usually treated as special data types that can only be dereferenced or compared for equality. Linked data structures are thus contrasted with arrays and other data structures that require performing arithmetic operations on pointers.

Sûreté du typage

La sûreté du typage est un principe permettant d'améliorer la qualité de la programmation. Dans les langages à typage statique, l'un des objectifs est d'intercepter les erreurs de type de données lors de la compilation. Un type peut être vu comme un ensemble de valeurs et un ensemble d'opérateurs. La programmation objet a introduit les notions d'objets, messages, classes, héritage. Il est tentant de faire coller les classes à des types.

Structure de données persistante

En informatique, une structure de données persistante est une structure de données qui préserve ses versions antérieures lorsqu'elle est modifiée ; une telle structure est immuable, car ses opérations ne la modifient pas en place (de manière visible) mais renvoient au contraire de nouvelles structures. Une structure est partiellement persistante si seule sa version la plus récente peut être modifiée, les autres n'étant accessibles qu'en lecture. La structure est dite totalement persistante si chacune de ses versions peut être lue ou modifiée.

Afficher plus

Séances de cours associées (64)

Pointeurs et tableaux: Gestion de la mémoire en C

Explique la relation entre les pointeurs et les tableaux en C, en se concentrant sur la gestion de la mémoire et l'arithmétique du pointeur.

Arrays dynamiques en C: Membres flexibles Array

Couvre les membres flexibles du tableau en C, en se concentrant sur l'allocation dynamique de la mémoire et les applications pratiques dans la programmation système.

Pointeur Arithmétique: Comprendre la gestion de la mémoire en C

Explique l'arithmétique du pointeur en C, en se concentrant sur la manipulation de la mémoire et les pièges courants.

Python : dictionnaires et tuples

Explore les dictionnaires, les tuples, les objets mutables et les arguments de longueur variable en Python.

Chaînes en C : Initialisation et gestion de la mémoire

Couvre la représentation et la gestion des chaînes en C, en soulignant les principales différences par rapport aux autres langages de programmation.

Afficher plus

Concepts associés (31)

Memory safety

Structure de données

Linked data structure

Sûreté du typage

Structure de données persistante

Afficher plus