Publication

Counterexample-Guided Focus

Related publications (45)

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.

Bayes Security: A Not So Average Metric

Carmela González Troncoso, Giovanni Cherubin

Security system designers favor worst-case security metrics, such as those derived from differential privacy (DP), due to the strong guarantees they provide. On the downside, these guarantees result in a high penalty on the system's performance. In this pa ...

IEEE2023

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Verified Functional Programming

Nicolas Charles Yves Voirol

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

EPFL2019

Quantifying bacterial structure of aerobic granular sludge using image analysis

Karen Gemayel

This Master’s project entitled ’Quantifying Bacterial Structure of Aerobic Granular Sludge using Image Analysis’ aims to quantitatively describe various aspects of cell activity inside aerobic granular sludge using image analysis. It entails the theory of ...

2019

The Daily Design of the Quantified Self

Alexandre André Robert Rigal, Dario Rodighiero

This article argues how the digital traces that are collected day by day can be used to reshape and improve our personal self. If in the past, we were used to collecting data through diaries, today the task of producing inscriptions is delegated to technol ...

2019

COMPAS Finite Element (FE) Workshop

Aryan Rezaei Rad

The Block Research Group (BRG) at ETH Zurich and the Laboratory for Timber Constructions (IBOIS) gave a collaborative workshop on the Finite Element (FE) analysis using the COMPAS package. ...

2019

Refutation-based synthesis in SMT

Viktor Kuncak, Andrew Joseph Reynolds

We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...

SPRINGER2019

Analysis of the sensitivity of the hydromorphological index of diversity, HMID

Anton Schleiss, Walter Gostner, Mário Jorge Rodrigues Pereira Da Franca, Severin Stähly, Christopher Robinson

Hydromorphological conditions are a key factor for the habitat diversity in riverine ecosystems. The Hydromorphological Index of Diversity (HMID) is a tool to quantify the habitat diversity in a river reach based on local flow depths and flow velocities. T ...

2018

Quantification and Classification of Handprint-based Net Positive Resource Efficiency Measures in the Swiss Industry Sector

Florian Elias Landerer

The task of the master project is to analyse a data set with information of several hundred companies from Switzerland. The goal is to find in the Swiss industry sector a classification/typology for the nature of resource efficiency of innovating companies ...

2018

Extending Safe C Support In Leon

Marco Adriano Antognini

As hardware designs get more robust and efficient, software can solve a wider range of challenges, each one more advanced than the previous one. The direct consequence is that software complexity grows continuously. Despite being used more frequently in de ...

2017