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

Concept

Vérification de modèles

Publications associées (23)

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

Synthesizing efficient systems in probabilistic environments

Barbara Jobstmann

We present a formalism, algorithms and tools to synthesise reactive systems that behave efficiently, i.e., which achieve an optimal trade-off between a given cost and reward model. Synthesis aims to automatically generate a program from a specification. Mo ...

Springer2016

A High-Level Synthesis Flow for the Implementation of Iterative Stencil Loop Algorithms on FPGA Devices

David Atienza Alonso, Ivan Beretta, Alessandro Antonio Nacci

The automatic generation of hardware implementations for a given algorithm is generally a difficult task, especially when data dependencies span across multiple iterations such as in iterative stencil loops (ISLs). In this paper, we introduce an automatic ...

IEEE/ACM Press2013