Publication

Supporting Loop Proofs in KeY by using BLAST

Related publications (83)

We propose two expressive and complementary techniques for the verification of safety properties of infinite-state BIP models. Both our techniques deal with the full BIP specification, while the existing approaches impose con- siderable restrictions: they ...

Springer2015

Superlensing using complementary media

Hoài-Minh Nguyên

This paper studies magnifying superlens using complementary media. Superlensing using complementary media was suggested by Veselago in [16] and innovated by Nicorovici et al. in [9] and Pendry in [10]. The study of this problem is difficult due to two fact ...

Gauthier-Villars/Editions Elsevier2015

The SystemC AMS extensions support heterogeneous modeling and make use of several Models of Computation (MoCs) that operate on different time scales in the Discrete Event (DE), Discrete Time (DT), and Continuous Time (CT) domains. The simulation of such he ...

IEEE Conference Publications2015

In the first part, we first introduce steganography (in chapter 1) not in the usual context of information security, but as a method to piggyback data on top of some content. We then focus on audio steganography and propose a new steganographic scheme in c ...

2014

Rigorous software design for nano and micro satellites using BIP framework

Marco Pagnamenta

The CubETH satellite mission, a cooperative Swiss CubeSat mission involving ETH Zurich, EPF Lausanne, several universities of applied sciences, and Swiss companies, will allow technology demonstrations and proof-of-concepts concerning GNSS-based navigation ...

2014

Contracts for Real-Time, Safety Critical Systems

Chandrakana Nandi

Verifying real-time systems goes beyond the verification of functional properties: it also requires the checking of real-time properties. This makes traditional contract-frameworks partially inept for checking real-time programs. This is a major problem be ...

2014

Unlike artificial light sources, which can be calibrated to meet a desired luminous effect regardless of latitude, climate, or time of day, daylight is a dynamic light source, which produces variable shadow patterns and fluctuating levels of brightness. Wh ...

Elsevier2014

Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if ass ...

Springer2014

Verification of Imperative Programs in Scala

Régis William Blanc

Safety-critical software systems can only support a limited number of failures. Extensive testing is good at catching errors, however that will never certify their absence. Formal verification is an alternative to testing that can (automatically) provide a ...

2012

Speculative Linearizability

Rachid Guerraoui, Viktor Kuncak, Giuliano Losa

Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the a ...

Assoc Computing Machinery2012

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.