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