Personne

Régis William Blanc

Cette personne n’est plus à l’EPFL

Publications associées (11)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Verification by Reduction to Functional Programs

Régis William Blanc

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

Viktor Kuncak, Régis William Blanc

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

Tree Interpolation in Vampire

Régis William Blanc, Laura Ildiko Kovacs, Ashutosh Gupta

We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of ...

Springer Berlin Heidelberg2013

Techniques for Program Synthesis

Régis William Blanc

Software synthesis is an attractive field of study that can promise a more safe and productive software development process. However, it is notoriously very difficult and few convincing applications have emerged so far. In this report, we present a series ...

2013

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

2013

On Verification by Translation to Recursive Functions

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

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

ACM Press2013

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

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

2013

Interpolation for Synthesis on Unbounded Domains

Viktor Kuncak, Régis William Blanc

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

Verification of Imperative Programs in Scala

Régis William Blanc

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

2012