Séance de cours

Vérification des programmes avec l'inox : un exemple étendu

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 couvre la vérification des programmes utilisant l'inox, en mettant l'accent sur un exemple étendu lié au format d'image tout à fait OK (QOI). La séance de cours commence par une introduction à QOI, un format de compression d'image sans perte offrant des accélérations significatives. Il se décline ensuite dans l'implémentation de Scala QOI, montrant comment Stainless peut traduire Scala en C. La séance de cours traite également des méthodes d'encodage, des fonctions partielles inverses et du processus de vérification. Les participants sont encouragés à essayer le script de vérification fourni dans le dépôt et à explorer la version entièrement vérifiée pour une compréhension plus approfondie du sujet.

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

Concepts associés (29)

Compression d'image

La compression d'image est une application de la compression de données sur des . Cette compression a pour utilité de réduire la redondance des données d'une image afin de pouvoir l'emmagasiner sans occuper beaucoup d'espace ou la transmettre rapidement. La compression d'image peut être effectuée avec perte de données ou sans perte. La compression sans perte est souvent préférée là où la netteté des traits est primordiale : schémas, dessins techniques, icônes, bandes dessinées.

Compression de données

La compression de données ou codage de source est l'opération informatique consistant à transformer une suite de bits A en une suite de bits B plus courte pouvant restituer les mêmes informations, ou des informations voisines, en utilisant un algorithme de décompression. C'est une opération de codage qui raccourcit la taille (de transmission, de stockage) des données au prix d'un travail de compression. Celle-ci est l'opération inverse de la décompression.

Compression artifact

A compression artifact (or artefact) is a noticeable distortion of media (including , audio, and video) caused by the application of lossy compression. Lossy data compression involves discarding some of the media's data so that it becomes small enough to be stored within the desired or transmitted (streamed) within the available bandwidth (known as the data rate or bit rate). If the compressor cannot store enough data in the compressed version, the result is a loss of quality, or introduction of artifacts.

Algorithme de compression sans perte

vignette|Comparaison de la compression d'image entre les formats JPG (à gauche) et PNG (à droite). PNG utilise une compression sans perte. On appelle algorithme de compression sans perte toute procédure de codage ayant pour objectif de représenter une certaine quantité d'information en utilisant ou en occupant un espace plus petit, permettant ainsi une reconstruction exacte des données d'origine. C'est-à-dire que la compression sans perte englobe les techniques permettant de générer un duplicata exact du flux de données d'entrée après un cycle de compression/expansion.

Lossy compression

In information technology, lossy compression or irreversible compression is the class of data compression methods that uses inexact approximations and partial data discarding to represent the content. These techniques are used to reduce data size for storing, handling, and transmitting content. The different versions of the photo of the cat on this page show how higher degrees of approximation create coarser images as more details are removed. This is opposed to lossless data compression (reversible data compression) which does not degrade the data.

Afficher plus

Séances de cours associées (30)

Compression de données et théorème de Shannon: Compression de perte

Explore la compression des données, y compris les méthodes sans perte et la nécessité de la compression sans perte pour les nombres réels et les signaux.

Compression de l'image

Explore la compression d'image à travers diverses approches telles que la compression de pixel et de niveau de bloc, Discret Cosine Transform, quantification et codage entropie.

Accélérateurs Deep Learning : Stratégies d’optimisation

Explore les stratégies d'optimisation pour les accélérateurs d'apprentissage en profondeur, en mettant l'accent sur la réduction des mouvements de données grâce au batching, à l'optimisation des flux de données et à la compression.

Résolution du cadre: Structure en treillis

Couvre la résolution d'un cadre en tant que structure en treillis, en se concentrant sur la répartition de la charge.

Compression idéale : cycles de puissance et pompes à chaleur

Explore la compression idéale dans les cycles de puissance, en discutant des processus réels, de l'efficacité et de la comparaison.

Afficher plus

Concepts associés (29)

Compression d'image

Compression de données

Compression artifact

Algorithme de compression sans perte

Lossy compression

Afficher plus