Concept

Predicate transformer semantics

Related publications (16)

On algebraic array theories

Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. T ...

New York2023

Multi space reduced basis preconditioners for parametrized Stokes equations

Alfio Quarteroni, Simone Deparis, Andrea Manzoni, Niccolò Dal Santo

We introduce a two-level preconditioner for the efficient solution of large scale saddle point linear systems arising from the finite element (FE) discretization of parametrized Stokes equations. This preconditioner extends the Multi Space Reduced Basis (M ...

PERGAMON-ELSEVIER SCIENCE LTD2019

An adaptive primal-dual framework for nonsmooth convex minimization

Volkan Cevher, Quoc Tran Dinh, Ahmet Alacaoglu

We propose a new self-adaptive and double-loop smoothing algorithm to solve composite, nonsmooth, and constrained convex optimization problems. Our algorithm is based on Nesterov’s smoothing technique via general Bregman distance functions. It self-adaptiv ...

2019

Multi space reduced basis preconditioners for parametrized partial differential equations

Niccolò Dal Santo

The multiquery solution of parametric partial differential equations (PDEs), that is, PDEs depending on a vector of parameters, is computationally challenging and appears in several engineering contexts, such as PDE-constrained optimization, uncertainty qu ...

EPFL2018

A Theory Agenda for Component-Based Design

Joseph Sifakis, Simon Bliudze

The aim of the paper is to present a theory agenda for component-based design based on results that motivated the development of the BIP component framework, to identify open problems and discuss further research directions. The focus is on proposing a sem ...

Springer International Publishing2015

Deciding Conditional Termination

We address the problem of conditional termination, which is that of defining the set of initial configurations from which a given program always terminates. First we define the dual set, of initial configurations from which a non-terminating execution exis ...

Tech Univ Braunschweig2014

Diffusive-type of double diffusion in lakes - a review

Alfred Johny Wüest, Martin Schmid

This chapter is a contribution in honour of Gerhard H Jirka, who has been fascinated by the amazing variety of small-scale structures that nature surprises us with, particularly in stratified natural waters. Here, we focus on the diffusive regime of double ...

CRC Press2012

Fluid-Structure Interaction Problems in Hemodynamics

Paolo Crosetto

In this work we aim at the description, study and numerical investigation of the fluid-structure interaction (FSI) problem applied to hemodynamics. The FSI model considered consists of the Navier-Stokes equations on moving domains modeling blood as a visco ...

EPFL2011

On Delayed Choice Execution for Falsification

Viktor Kuncak, Tihomir Gvero, Milos Gligoric

We present an approach for finding errors in programs and specifications. We formulate our approach as an execution mechanism for a non-deterministic guarded-command language. Guarded commands have already proved useful for verification-condition generatio ...

2008

Runtime Checking for Separation Logic

Viktor Kuncak

Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using static analysis techniques. Checking data structure specifications du ...

Springer2008

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.