In March 2010, Nguyen Van Tang (a post-doc at AIST/CVS, Japan)
made his first visit to the Department of Computer Science, The
University of Bath, for three weeks (from March 6 - March 26). His main
activities of the visit were as follows:
1) In the first week: He and Kitamura-san attend some semniars and classes of
John Power for final year students on category theory and computational
complexity. These classes an seminars were interesting and useful for
him. He can study from John how to give a lecture and how to make a
stimulating atmostphere for students in the class. He also attended a
seminar of a PhD student on multi-category theory (from Cambridge
University) in Department of Computer Science, Bath University.
2) In the second week: He attended the fourth workshop between Bath-AIST/CVS
on March 18. He also gave a talk on the joint project of AIST/CVS with a
company in a video conferencing seminar between Department Computer
Science of Bath and the Depertment Computer Science, The University of
Swansea. The title of the talk was: A Hybrid Approach to Verify A Train
Fare Caculation System Using Testing and Theorem Proving.
3) In the third week: He attend the firth workshop of Bath-AIST/CVS-Swansea. In
this workshop, he had discussed with researchers (Anton, Monika, Karim,
Andy, Tasaki, Martin) on possibility of combining Agda and an automatic
model checking tools such as SAT solve. The group at Swansea lead by
Anton also has a joint project research (with a railway company) of
verification for railway interlocking system. Their techniques are based
on SAT solver, SCADE model checker, and Agda. These discussions will be
useful for him to apply Agda and model checking for the project at AIST.
He also gave a talk on his academic research related to
automata-theoretic based verification and model checking.
4) Additional work: He spended some time on refining a paper to submit to a journal.
In addtion, he also had discussons with researchers and PhD students in
Bath on the topic of verification and answer set programming such as
Owen Cliff, Martin Brain, Ana, Martin.
Final Conclusion: The visit was very sucessful, and he had obtained many
valuable comments, and suggestions from researchers at Bath, Swansea on the
research topics. He hope in the future, Bath-AIST/CVS-Swansea will have
more collaboration in research. He really wish to have occasion to meet
researchers from Bath and Swansea at AIST/CVS, as well as, wish to have
chance to visit Bath again in the future.
Nguyen Van Tang, Hitoshi Ohsaki, and et al. Formal Verification of A Train Fare
Calculation System by The Agda Proof Assistant. In the Proceedings of the first
International Workshop on Simulation Based Development of Certified Embedded
Systems (SBDCES¿09), Awaji, October 2009. To submit to International Journal.
Nguyen Van Tang. A Tighter Bound for Determinization of Visibly Pushdown Automata.
In the Proceedings of the 11th International Workshop on Verification of
Infinite-State Systems (INFINITY¿09). A Satellite Event of the 20th International
Conference on Concurrency Theory (CONCUR¿09), Bologna, Italy, September 2009.
Electronic Proceedings of Theoretical Computer Science, Volume. 10, pp. 62-76,