Publication

Automating Verification of Functional Programs with Quantified Invariants

Related publications (57)

Graph Chatbot

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.

Programming with Specifications

Philippe Paul Henri Suter

This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative ...

EPFL2012

Deprecating the Observer Pattern with Scala.React

Martin Odersky, Ingo Maier

Programming interactive systems by means of the observer pattern is hard and error-prone yet is still the implementation standard in many production environments. We show how to integrate different reactive programming abstractions into a single framework ...

2012

Towards Complete Reasoning about Axiomatic Specifications

Viktor Kuncak, Swen Jacobs

To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Connected at any cost? The vulnerability of critical infrastructures and crisis management

Valérie November

Critical infrastructures are receiving a great deal of attention, due, on the one hand, to the major malfunctions to which they are subject and their potential as targets of malicious intent on the other. Economic and political impacts are studied; increas ...

2011

Satisfiability Modulo Recursive Programs

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of expressive correctness properties of recursive first-order functional programs. In our approach, both properties and programs are expressed in the same language, a subset of Scala. We impl ...

Springer-Verlag Berlin2011

Decision Procedures for Automating Termination Proofs

Ruzica Piskac

Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current too ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

On Satisfiability Modulo Computable Functions

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...

2010

On Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

2010

Building a Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010