Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Formal specification

Publications associées (24)

Verification and validation procedures with applications to plasma-edge turbulence simulations

Fabio Riva

Understanding the plasma dynamics in tokamaks is of fundamental importance to reliably predict the performances of future fusion devices. Because of the complex phenomena at play, state-of-the-art simulation codes are needed to investigate the plasma dynam ...

EPFL2017

Towards Proving Optimistic Multicore Schedulers

Willy Zwaenepoel, Baptiste Joseph Eustache Lepers

Operating systems have been shown to waste machine resources by leaving cores idle while work is ready to be scheduled. This results in suboptimal performance for user applications, and wasted power. Recent progress in formal verification methods have led ...

2017

Translating Scala Programs to Isabelle/HOL, Automated Reasoning

Viktor Kuncak

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs ...

2016

Approximate BDD Optimization with Prioritized epsilon-Preferred Evolutionary Algorithm

Mathias Soeken

Approximate computing has gained high attention in various applications that can benefit from a reduction in costs by lowering the accuracy. In this paper we present an optimization approach for functional approximation of Binary Decision Diagrams (BDDs) w ...

Assoc Computing Machinery2016