Accelerating Interpolants

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.

A metaprogrammer should be able to reason about the semantics of the generated code. Multi-stage programming introduced an elegant and powerful solution to this problem. It follows a semantically driven approach to code generation, where semantics are full ...

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

Modern, statically typed programming languages provide various abstraction facilities at both the term- and type-level. Common abstraction mechanisms for types include parametric polymorphism -- a hallmark of functional languages -- and subtyping -- which ...

dotty is a new, experimental Scala compiler based on DOT, the calculus of Dependent Object Types. Higher-kinded types are a natural extension of first-order lambda calculus, and have been a core construct of Haskell and Scala. As long as such types are jus ...

We present qualified types for Scala, a form of refinement types adapted to the Scala language. Qualified types allow users to refine base types and classes using predicate expressions. We implemented a type checker for qualified types that is embedded in ...

Statically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages ...

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. In particular, objects can contain type members, which can be selected as ...

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Software development has taken a fundamental turn. Software today has gone from simple, closed programs running on a single machine, to massively open programs, patching together user experiences byway of responses received via hundreds of network requests ...

Functional programming (FP) is regularly touted as the way forward for bringing parallel, concurrent, and distributed programming to the mainstream. The popularity of the rationale behind this viewpoint (immutable data transformed by function application) ...

Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes ...

This paper presents a publicly available toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We pres ...

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 ...

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 ...

Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages L that assign to each word w a real number L(w). In the case of infinite words, the value of a run is naturally computed as the ma ...

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexampl ...

Scala is a general-purpose programming language developed at EPFL. It combines the most important concepts found in object-oriented and functional languages. Scala is a statically typed language; in particular it features an advanced type system and suppor ...

We prove several results related to local proofs, interpolation and superposition calculus and discuss their use in predicate abstraction and invariant generation. Our proofs and results suggest that symbol-eliminating inferences may be an interesting alte ...

We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a ...

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this p ...

Accelerating Interpolants

Chat with Graph Search

Scalable Metaprogramming in Scala 3

Verified Functional Programming

Higher-Order Subtyping with Type Intervals

Implementing Higher-Kinded Types in Dotty

SMT-Based Checking of Predicate-Qualified Types for Scala

Decrypting Local Type Inference

Dependent Object Types

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

Language Support for Distributed Functional Programming

Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution

Complete Completion using Types and Weights

A Verification Toolkit for Numerical Transition Systems

Towards Complete Reasoning about Axiomatic Specifications

Building a Calculus of Data Structures

Expressiveness And Closure Properties For Quantitative Languages

Software Verification by Combining Program Analyses of Adjustable Precision

Programming language abstractions for mobile code

Interpolation and Symbol Elimination

Program Analysis with Dynamic Precision Adjustment

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis