43th InfoBlender Seminar
Date: February 7
Venue: University of Minho, Gualtar campus (Braga) | Informatics Department, Building 07 | Auditorium A2, first floor
Time: 2PM
Presenter: Meng Sun, Peking University, China
Title: Using Coq and Recurrent Neural Network to Model and Verify Timed Connectors
More info HERE
Abstract: Formal modeling and verification of connectors in component-based software systems are getting more interest with recent advancements and evolution in modern software systems. In this work, we use the proof assistant Coq for modeling and verification of timed connectors. Timed channels and the composition operators for constructing timed connectors are defined in Coq. Basic timed channels are interpreted as axioms and inference rules are used for building complex connectors. Timed connectors being built by composing basic timed / untimed channels, are defined as logical predicates which describe the relations between inputs and outputs. Various properties of timed connectors can be specified as high-order logic propositions and verified using theorem proving techniques. Furthermore, we propose an approach based on recurrent neural networks (RNNs) to predict the correct tactics in the proving process. Under this framework, properties of timed connectors can be naturally formalized and semi-automatically proved in Coq.
Short bio: Meng Sun is a professor at Department of Informatics, School of Mathematical Sciences, Peking University. He received Bachelor and PhD degrees in applied mathematics from Peking University in 1999 and 2005. He then spent one year as a postdoctoral researcher at National University of Singapore. From 2006 to 2010, he worked as a scientific staff member at CWI. He has been a faculty member of Peking University since 2010 and became a full professor in 2017. His research interests include software engineering, formal methods, software verification and testing, coordination models and languages, coalgebra theory, cyber-physical systems, service-oriented and cloud computing, big data analysis.