Lecture

Verifying Programs with Stainless: Part 2

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

In course

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

This lecture covers the usage of Stainless for program verification, focusing on verifying programs and ensuring correctness. The instructor demonstrates the process of using Stainless to verify programs, including defining specifications, ensuring postconditions, and checking termination. The lecture also includes examples of verifying functions, such as nonEmptyListSize and zip, using Stainless and SMT solvers. The importance of defining postconditions and measures for recursive functions is highlighted, along with the significance of ensuring the correctness of the verification conditions. The lecture concludes with a discussion on the power of Stainless in accurately verifying programs and the contributions of various researchers and collaborators to the project.

Instructor

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.

Official source

Ontological neighbourhood

Theoretical computer science

Programming language theory: High-level programming languages

Related concepts (30)

F Sharp (programming language)

F# (pronounced F sharp) is a functional-first, general-purpose, strongly typed, multi-paradigm programming language that encompasses functional, imperative, and object-oriented programming methods. It is most often used as a cross-platform Common Language Infrastructure (CLI) language on .NET, but can also generate JavaScript and graphics processing unit (GPU) code. F# is developed by the F# Software Foundation, Microsoft and open contributors. An open source, cross-platform compiler for F# is available from the F# Software Foundation.

Scala (programming language)

Scala (ˈskɑːlə ) is a strong statically typed high-level general-purpose programming language that supports both object-oriented programming and functional programming. Designed to be concise, many of Scala's design decisions are aimed to address criticisms of Java. Scala source code can be compiled to Java bytecode and run on a Java virtual machine (JVM). Scala can also be compiled to JavaScript to run in a browser, or directly to a native executable.

Chisel (programming language)

The Constructing Hardware in a Scala Embedded Language (Chisel) is an open-source hardware description language (HDL) used to describe digital electronics and circuits at the register-transfer level. Chisel is based on Scala as an embedded domain-specific language (DSL). Chisel inherits the object-oriented and functional programming aspects of Scala for describing digital hardware. Using Scala as a basis allows describing circuit generators. High quality, free access documentation exists in several languages.

String interpolation

In computer programming, string interpolation (or variable interpolation, variable substitution, or variable expansion) is the process of evaluating a string literal containing one or more placeholders, yielding a result in which the placeholders are replaced with their corresponding values. It is a form of simple template processing or, in formal terms, a form of quasi-quotation (or logic substitution interpretation). The placeholder may be a variable name, or in some languages an arbitrary expression, in either case evaluated in the current context.

Kotlin (programming language)

Kotlin (ˈkɒtlɪn) is a cross-platform, statically typed, general-purpose high-level programming language with type inference. Kotlin is designed to interoperate fully with Java, and the JVM version of Kotlin's standard library depends on the Java Class Library, but type inference allows its syntax to be more concise. Kotlin mainly targets the JVM, but also compiles to JavaScript (e.g., for frontend web applications using React) or native code via LLVM (e.g., for native iOS apps sharing business logic with Android apps).

Related lectures (32)

Verifying Compiler: Spec# Approach

Explores the Spec# programming system, focusing on a verifying compiler for C# 2.0.

Gitlab Agent for Kubernetes (`agentk`)

Covers the setup of a Gitlab agent for Kubernetes, focusing on installation, version control, and troubleshooting.

Practical Engineering 1: Signal Processing

Explores advanced software engineering topics and signal processing using lazy lists to build a sound synthesizer from scratch.

Type Checking Lab

Focuses on implementing a type checker for Amy, covering name and type analysis, typing constraints generation, and the importance of type checking in compilation.

Memory Management & Crash Programs