Publications de Régis William Blanc

Verification by Reduction to Functional Programs

In this thesis, we explore techniques for the development and verification of programs in a high-level, expressive, and safe programming language. Our programs can express problems over unbounded domains and over recursive and mutable data structures. We p ...

EPFL2017

Sound reasoning about integral data types with a reusable SMT solver interface

Régis William Blanc, Viktor Kuncak

We extend the Leon verification system for Scala with support for bit-vector reasoning, thus addressing one of its fundamental soundness limitation with respect to the treatment of integers primitives. We leverage significant progresses recently achieved i ...

ACM Press2015

Interpolation for Synthesis on Unbounded Domains

Régis William Blanc, Viktor Kuncak

Synthesis procedures compile relational specifications into functions. In addition to bounded domains, synthesis procedures are applicable to domains such as mathematical integers, where the domain and range of relations and synthesized code is unbounded. ...

Ieee2013

An overview of the Leon verification system: verification by translation to recursive functions

Philippe Paul Henri Suter, Régis William Blanc, Etienne Kneuss, Viktor Kuncak

We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Bo ...

2013

CafeSat: a Modern SAT Solver for Scala

Régis William Blanc

We present CafeSat, a SAT solver written in the Scala programming language. CafeSat is a modern solver based on DPLL and featuring many state-of-the-art techniques and heuristics. It uses two-watched literals for Boolean constraint propagation, conflict-dr ...

ACM Press2013

ABC: Algebraic Bound Computation for Loops

Thibaud Hottelier, Régis William Blanc, Laura Ildiko Kovacs

We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of nested program loops. The system combines static analysis of programs with symbolic summation techniques to derive loop invariant relations bet ...

Springer Berlin Heidelberg2010