Speaker / Predavač : Dr Viktor Kuncak
Title / Naslov: COST Action IC0901: "Rich Model Toolkit"
Abstract / Abstrakt:
I will describe the COST Action "Rich Model Toolkit", which coordinate the development of infrastructures for automated reasoning about Rich Models of computer systems. Rich Models have the expressive power of all practically formalizable mathematics, enabling natural specification of software, hardware, embedded, and distributed systems. Rich Models support modeling at a wide range of abstraction levels, from knowledge bases and system architecture, to software source code and detailed hardware design. Among the specific topics of interests are: 1) Standardization of expressive languages (formats to represent systems, formulas, proofs, counterexamples, translation between specification languages, benchmarks and competitions for automated reasoning, verification, analysis, synthesis). 2) Decision procedures for new classes of constraints, SAT and SMT implementation and certification, encoding synthesis and analysis problems into SMT, description logics and scalable reasoning about knowledge bases. 3) Transition system analysis (abstraction-based approaches and refinement for verification of infinite-state systems, constraint-based program analysis, data-flow analysis for complex domains, extracting transition systems from programming languages and bytecodes). 4) High-level synthesis (new algorithms for synthesis from high-level specifications, extending decision procedures to perform synthesis tasks, connections between invariant generation and code synthesis). Short biography: Viktor Kuncak is the Chair of the COST Action "Rich Model Toolkit". He is an assistant professor in the School of Computer and Communication Sciences at the Swiss Federal Institute of Technology Lausanne (EPFL) where he leads the Lab for Automated Reasoning and Analysis. He received his PhD from MIT in 2007 and his BSc from the University of Novi Sad in 2000. More information: http://richmodels.epfl.ch http://lara.epfl.ch