Laboratoire Bordelais de Recherche en Informatique

Efficient methods for highly parallel timed systems

PhD opening

supervisors: Srivathsan B. (CMI Chennai, India) and Igor Walukiewicz (CNRS, LaBRI, Bordeaux)

This PhD grant is available from September 2017 with standard French financing for 36 months. The thesis is planned to be a joint thesis with Chennai Mathematical Institute and is supported by Idex of Bordeaux University. The supervisors of the thesis will be Igor Walukiewicz at LaBRI, and Srivathsan at CMI.

The subject of the thesis will be theoretical and practical aspects of analysis of timed systems. The correctness of numerous computer systems not only concerns functional correctness, i.e., whether the system computes the expected output given some input, but also non-functional properties such as execution time or energy consumption. The goal of this thesis is to develop new algorithms and tools for verification of timed systems. We will concentrate on development of partial-order reduction techniques for timed verification. These are very powerful techniques proposed for verification of finite state systems, but their transfer to timed setting remains a challenge. Our recent advances, in particular in on-the-fly approximation techniques, give us hope that we will able to find a partial-order reduction algorithm for some classes of timed systems. This will have a very important impact on verification of systems with many parallel components.

Interested candidates should contact:
Igor Walukiewicz,
e-mail:

The deadline for applications is 26th of June 2017

Bibliography:

Journals:

F. Herbreteau, B. Srivathsan and I. Walukiewicz. Better Abstractions for Timed Automata. Information and Computation, 2016.

F. Herbreteau and B. Srivathsan. Coarse Abstrations Make Zeno Behaviors Difficult to Detect. Logical Methods in Computer Science 9(1), 2013.

F. Herbreteau, B. Srivathsan and I. Walukiewicz Efficient Emptiness Check for Timed Büchi Automata. Formal Methods in System Design, 40(2), pp. 122-146, Springer, 2012.

Conferences:

Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, Igor Walukiewicz: Why Liveness for Timed Automata Is Hard, and What We Can Do About It. FSTTCS 2016

F. Herbreteau, B. Srivathsan and I. Walukiewicz. Lazy abstractions for timed automata CAV'2013.

F. Herbreteau, B. Srivathsan and I. Walukiewicz. Better abstractions for timed automata. LICS'2012.

F. Herbreteau, B. Srivathsan. Coarse abstractions make Zeno behaviors difficult to detect. CONCUR'2011

F. Herbreteau, D. Kini, B. Srivathsan, I. Walukiewicz. Using non convex approximations for efficient analysis of timed automata. FSTTCS 2011

F. Herbreteau, B. Srivathsan. Efficient On-The-Fly Emptiness Check for Timed Büchi Automata. ATVA'2010

F. Herbreteau, B. Srivathsan and I. Walukiewicz. Efficient Emptiness Check for Timed Büchi Automata. CAV'2010


-->
Igor Walukiewicz
Last modified: June 6, 2017