Publication

Automating Verification of Functional Programs with Quantified Invariants

2016
Reports

Abstract

We present the foundations of a verifier for higher-order functional programs with generics and recursive algebraic data types. Our ver- ifier supports finding sound proofs and counterexamples even in the presence of certain quantified invariants and recursive functions. Our approach uses the same language to describe programs and in- variants and uses semantic criteria for establishing termination. Our implementation makes effective use of SMT solvers by encoding first-class functions and quantifiers into a quantifier-free fragment of first-order logic with theories. We are able to specify properties of datastructure operations involving higher-order functions with minimal annotation overhead and verify them with a high degree of automation. Our system is also effective at reporting counterexam- ples, even in the presence of first-order quantification.

Official source

https://infoscience.epfl.ch/entities/publication/722a0bfe-01e3-4901-bc62-4bf1e0c7d7d1

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.

2016
Reports

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/722a0bfe-01e3-4901-bc62-4bf1e0c7d7d1

About this result

Related concepts (32)

First-order logic

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.

Second-order logic

In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence says that for every formula P, and every individual x, either Px is true or not(Px) is true (this is the law of excluded middle).

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.

Related publications (17)

Automating Verification of Functional Programs with Quantified Invariants

Chat with Graph Search

An optimization framework for a dynamic multi-skill workforce scheduling and routing problem with time windows, synchronization constraints, and anticipated tasks

Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization

How employment constrains participation in MOOCs?