Publication

Automatic Verification of Parametric Specifications with Complex Topologies

Publications associées (23)

Convergence Of Variance-Reduced Learning Under Random Reshuffling

Several useful variance-reduced stochastic gradient algorithms, such as SVRG, SAGA, Finito, and SAG, have been proposed to minimize empirical risks with linear convergence properties to the exact minimizers. The existing convergence results assume uniform ...

IEEE2018

Algorithmic Verification of Component-based Systems

Qiang Wang

This dissertation discusses algorithmic verification techniques for concurrent component-based systems modeled in the Behavior-Interaction-Priority (BIP) framework with both bounded and unbounded concurrency. BIP is a component framework for mixed software ...

EPFL2017

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Aikaterini Argyraki, 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

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

Formal verification of infinite-state BIP models

Simon Bliudze, Wajeb Saab

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

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

Simon Bliudze, Qiang Wang

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Springer2015

Applying model checking to industrial-sized PLC programs

Simon Bliudze, Jean-Charles Tournier, Borja Fernandez Adiego

Programmable Logic Controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the ...

Institute of Electrical and Electronics Engineers2015

Timber Folded Plate Structures – Topological and Structural Considerations

Yves Weinand, Andrea Stitic

This paper analyses the potential of different possible folded form topologies for generating timber folded surface structures. The main advantage of such structures lies primarily in the realm of ecology and sustainability. By offering an integral way of ...

2015

A deployable tensegrity footbridge that connects at mid-span

Ian Smith, Nicolas Willy Veuve, Seif Dalil Safaei

This paper describes a near full-scale deployable tensegrity footbridge that deploys from both sides and connects at mid-span. Tensegrity structures are pre-stressed structures composed of tension elements (cables) surrounded by compression elements (strut ...

2015