Publication

The TL Compiler

Related publications (60)

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.

Formal Verification of Rust with Stainless

Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of ...

2021

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

EPFL2020

Verifying Software Network Functions with No Verification Expertise

George Candea, Solal Vincenzo Pirelli, Rishabh Ramesh Iyer, Luis David Figueiredo Mascarenhas Moreira Pedrosa, Matteo Rizzo

We present the design and implementation of Vigor, a software stack and toolchain for building and running software network middleboxes that are guaranteed to be correct, while preserving competitive performance and developer productivity. Developers write ...

ACM2019

Exact Synthesis of LTL Properties from Traces

Heinz Riener

We present an exact approach to synthesize temporal-logic formulas in linear temporal logic (LTL) from a set of given positive and negative example traces. Our approach uses topology structures, in particular partial DAGs, to partition the search space int ...

IEEE2019

From Uncertainty Data to Robust Policies for Temporal Logic Planning

Maryam Kamgarpour, Tony Alan Wood

We consider the problem of synthesizing robust disturbance feedback policies for systems performing complex tasks. We formulate the tasks as linear temporal logic specifications and encode them into an optimization framework via mixed-integer constraints. ...

ACM2018

Robust Control Policies Given Formal Specifications in Uncertain Environments

Maryam Kamgarpour, Tony Alan Wood

We consider robust control synthesis for linear systems with complex specifications that are affected by uncertain disturbances. This letter is motivated by autonomous systems interacting with partially known, time-varying environments. Given a specificati ...

2017

Secure numerical and logical multi party operations

Bin Lu

We derive algorithms for efficient secure numerical and logical operations in the semi-honest model ensuring statistical or perfect security for secure multi-party computation (MPC). To derive our algorithms for trigonometric functions, we use basic mathem ...

Elsevier Science Bv2017

Applying model checking to industrial-sized PLC programs

Jean-Charles Tournier, Simon Bliudze, 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

Animation-Based Service Specification, Verification and Validation

Biljana Bajic-Bizumic

[Context] With the expansion of services and service science, service systems have become an important abstraction for the service revolution. Service is defined as the application of resources (including competences, skills, and knowledge) to make changes ...

EPFL2015

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