== Synthesis and Verification of Real-time Logic (4 years FNRS PDR research project, 2015-2019) ==
* Position * One Post-Doc position is open at the Université libre de Bruxelles (ULB). The position is funded by a PDR collaborative research project of the Belgian National Fund for Scientific Research (FNRS), under the lead of Prof. Gilles Geeraerts (ULB) and Prof. Thomas Brihaye (UMons). * Summary of the research project * Computers pervade indisputably our everyday life (plane autopilots, airbags…). Clearly enough, ensuring the correctness of these critical computer systems is imperative. Today, the use of formal methods is widely advocated as adequate methodologies to obtain the strong guarantees that are requested by critical applications. In the current state of the art, those methods can be split in two categories: verification and synthesis methods. Roughly speaking, verification techniques are a posteriori methods, which allow to detect bugs in already existing models of a controller; and synthesis techniques are a priori methods which output a model of the controller that is guaranteed to be correct by construction. The development of those two families of techniques is nowadays quite advanced when the models and properties are purely qualitative. Nevertheless in order to faithfully model computer systems and their specifications, real-time aspects are of capital importance. Unfortunately, the theoretical and practical results are still partial when real-time aspects of the system must be taken into account. In the untimed case, the success of verification and synthesis methods can arguably be attributed to the fact that they rely on (Büchi) automata as an adequate model to express the system's behaviours, and on powerful yet natural languages to specify the properties (e.g. LTL). In the timed case, and while timed automata are a well-established and well-studied automaton model, the picture is not so clear. Real-time extensions of LTL are either highly undecidable (MTL), or studied mainly from a theoretical point of view (ECL, MITL), and the algorithms to perform verification with those logics are not easily amenable to implementation. Thus, the present research project aims at defining efficient algorithmic techniques to solve verification and synthesis problems when the specification languages are real-time linear logics. * Starting dates * From September, 2017 * Salary * Annual net salary (after all taxes) starts at €2,347.32/months for a Post-Doc student, in addition, advantages include complete health insurance. * The research environment * ULB (http://www.ulb.ac.be) is a complete university located in the city of Brussels at the center of Europe (25.000+ students with 30% coming from abroad). The Formal Methods and Veri cation group is part of the Computer Science Department of the Faculty of Sciences. The group maintains a large number of active collaborations with other research groups in computer- aided veri cation across Europe and the USA. The group is also part of the Belgian Federated Center for Veri cation (http://cfv.ulb.ac.be) that gathers all the Belgian research groups active in computer aided veri cation and hosts a monthly seminar with renowned guest speakers. The working language is English. The project is a joint project with the University of Mons (http://www.umons.ac.be/), which is located 70km south of Brussels. * Further information and application * Potential candidates can contact Prof. Geeraerts (gigeerae [at] ulb [dot] ac [dot] be) and Prof. Brihaye (thomas [dot] brihaye [at] umons [dot] ac [dot] be). -- Gilles GEERAERTS Université libre de Bruxelles (ULB) Home Page: http://www.ulb.ac.be/di/verif/ggeeraer Federated Center in Verification: http://cfv.ulb.ac.be Belgian olympiad of computer science: http://www.be-oi.be ---- [[ Petri Nets World: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies: ]] [[ [email protected] ]]
