Publication

Verification of Imperative Programs in Scala

2012
Student Projects

Abstract

Safety-critical software systems can only support a limited number of failures. Extensive testing is good at catching errors, however that will never certify their absence. Formal verification is an alternative to testing that can (automatically) provide a mathematical proof of correctness of programs. In this thesis, we present a verification procedure for imperative programs. Our procedure reduces imperative programming to functional programming and uses a semi-decision procedure that can reason modulo recursive functions. As a complementary method, we propose an algorithm to generate test cases that attain a high coverage of the program statements or can force the execution of some very refined control paths. We have implemented these algorithms and have integrated them in the Leon verification system. Leon can be used to verify programs written in a proper subset of Scala.

Official source

https://infoscience.epfl.ch/entities/publication/aa70a546-7f24-434c-9b0b-ce848db7ea4c

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

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.

2012
Student Projects

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/aa70a546-7f24-434c-9b0b-ce848db7ea4c

About this result

Related concepts (32)

Functional programming

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program. In functional programming, functions are treated as first-class citizens, meaning that they can be bound to names (including local identifiers), passed as arguments, and returned from other functions, just as any other data type can.

Declarative programming

In computer science, declarative programming is a programming paradigm—a style of building the structure and elements of computer programs—that expresses the logic of a computation without describing its control flow. Many languages that apply this style attempt to minimize or eliminate side effects by describing what the program must accomplish in terms of the problem domain, rather than describing how to accomplish it as a sequence of the programming language primitives (the how being left up to the language's implementation).

Procedural programming

Procedural programming is a programming paradigm, derived from imperative programming, based on the concept of the procedure call. Procedures (a type of routine or subroutine) simply contain a series of computational steps to be carried out. Any given procedure might be called at any point during a program's execution, including by other procedures or itself. The first major procedural programming languages appeared circa 1957–1964, including Fortran, ALGOL, COBOL, PL/I and BASIC. Pascal and C were published circa 1970–1972.

Related publications (1)

Verification of Imperative Programs in Scala

Chat with Graph Search

Unreliable Failure Detectors via Operational Semantics