Concept

Hoare logic

Related publications (26)

Automated Formal Verification of Software Network Functions

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

On algebraic array theories

Viktor Kuncak, Rodrigo Raya

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

Timing and spatial selection bias in rapid extreme event attribution

Anthony Christopher Davison, Ophélia Mireille Anna Miralles

Selection bias may arise when data have been chosen in a way that subsequent analysis does not account for. Such bias can arise in climate event attribution studies that are performed rapidly after a devastating "trigger event'', whose occurrence correspon ...

ELSEVIER2023

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

MATHICSE Technical Report : Multi space reduced basis preconditioners for parametrized Stokes equations

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

In this work we introduce a two-level preconditioner for the efficient solution of large scale saddlepoint linear systems arising from the finite element (FE) discretization of parametrized Stokes equations.The proposed preconditioner extends the Multi Spa ...

MATHICSE2018

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 Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017

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

ScalaDyno: Making Name Resolution and Type Checking Fault-tolerant

Martin Odersky, Vlad Ureche, Cédric Bastin

The ScalaDyno compiler plugin allows fast prototyping with the Scala programming language, in a way that combines the benefits of both statically and dynamically typed languages. Static name resolution and type checking prevent partially-correct code from ...

ACM2014

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.