Published on: 08-Jan-2018
Congratulations to (from left) Dr Ki Yung Ahn, Dr Ross Horne, Dr David Sanan, A/P Liu Yang and Asst/P Lin Shang-Wei for receiving the Best Paper Awards.
Researchers in the Cyber Security Lab received three best papers awards from top tier conferences in 2017. Results include a solution to a 30-year-old problem in protocol verification, and techniques for improving the efficiency of verifying safety properties.
Dr Ki Yung Ahn and Dr Ross Horne were awarded best paper at CONCUR 2017 – the première conference on concurrency. Their research was conducted in a project applying a technique called open bisimilarity to the verification of cryptographic protocols. The surprising insight is that there is a fundamentally intuitionistic logical characterisation of open bisimilarity. This insight was used to solve a 30-year-old problem in concurrency theory: logically characterising a robust equivalence technique for protocol verification. This breakthrough provides an improved foundation for tools used to verify cryptographic protocols.
Assistant Professor Lin Shang-Wei, Associate Professor Liu Yang and Dr David Sanán received an ACM Distinguished Paper Award for their paper at the international conference on Automated Software Engineering 2017. Their work presents a new approach to automatically constructing inductive loop invariants. Loop invariant generation is a fundamental problem in the verification of programs involving `while' loops. The key idea is to aggressively squeeze an inductive invariant based on Craig interpolants between forward and backward reachability analysis. The approach was evaluated by a set of loop benchmarks, backing up their technique with experimental evidence.
Assistant Professor Lin Shang-Wei was also awarded best paper at FORTE 2017 – an international conference on Formal Techniques for Distributed Objects, Components, and Systems. His paper concerns the verification of timed concurrent systems with uncertain parameters. His paper showed that most common decision problems are undecidable in this parametric setting. He also provides a methodology for abstraction to improve the verification of reachability properties in the presence of such parameters.
Ki Yung Ahn, Ross Horne and Alwen Tiu. A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. 28th International Conference on Concurrency Theory (CONCUR 2017).Editors: Roland Meyer and Uwe Nestmann; Article No. 7; pp. 7:1-7:17. Leibniz International Proceedings in Informatics.
Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sanán, Henri Hansen: FiB: squeezing loop invariants by interpolation between Forward/Backward predicate transformers. ASE 2017: 793-803.
Étienne André, Shang-Wei Lin: Learning-Based Compositional Parameter Synthesis for Event-Recording Automata. FORTE2017: 17-32.
Back to listing