Publications

In the following, we list bibliographic data of papers produced by members of the System Analysis and Verification Group, including DOI links and PDF postprints where available.

Please note: we are still in the process of adding older (pre-2016) papers to this list.

2017

  • A. Kolesnichenko, C. M. Poskitt, and S. Nanz. SafeGPU: contract- and library-based GPGPU for object-oriented languages. Computer Languages, Systems & Structures, vol. 48, pp. 68-88, 2017.
    [PDF] [DOI] [Bibtex]
    @article{Kolesnichenko-Poskitt-Nanz17a,
    author = {Alexey Kolesnichenko and Christopher M. Poskitt and Sebastian Nanz},
    title = {{SafeGPU}: Contract- and Library-Based {GPGPU} for Object-Oriented Languages},
    journal = {{Computer Languages, Systems & Structures}},
    volume = {48},
    pages = {68--88},
    year = {2017},
    doi = {10.1016/j.cl.2016.08.002},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Kolesnichenko-Poskitt-Nanz.COMLAN.2016.pdf},
    }
  • C. Jegourel, J. Sun, and J. S. Dong. Sequential schemes for frequentist estimation of properties in statistical model checking. In Proc. International Conference on Quantitative Evaluation of SysTems (QEST 2017), LNCS, Springer, 2017.
    [PDF] [Bibtex]
    @inproceedings{Jegourel-Sun-Dong17a,
    author = {Cyrille Jegourel and Jun Sun and Jin Song Dong},
    title = {Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking},
    booktitle = {{Proc. International Conference on Quantitative Evaluation of SysTems (QEST 2017)}},
    year = {2017},
    series = {LNCS},
    publisher = {Springer},
    note = {To appear},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/QEST17_extended_version.pdf},
    }
  • Q. L. Le, T. Makoto, J. Sun, and W. Chin. A decidable fragment in separation logic with inductive predicates and arithmetic. In Proc. International Conference on Computer Aided Verification (CAV 2017), LNCS, Springer, 2017.
    [PDF] [Bibtex]
    @inproceedings{Le-Makoto-Sun-Chin17a,
    author = {Quang Loc Le and Tatsuta Makoto and Jun Sun and Wei-Ngan Chin},
    title = {A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic},
    booktitle = {{Proc. International Conference on Computer Aided Verification (CAV 2017)}},
    year = {2017},
    series = {LNCS},
    publisher = {Springer},
    note = {To appear},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/cav2017.pdf},
    }
  • Y. Lin, J. Sun, Y. Xue, Y. Liu, and J. Dong. Feedback-based debugging. In Proc. International Conference on Software Engineering (ICSE 2017), ACM, 2017.
    [Bibtex]
    @inproceedings{Lin-et_al17a,
    author = {Yun Lin and Jun Sun and Yinxing Xue and Yang Liu and Jinsong Dong},
    title = {Feedback-Based Debugging},
    booktitle = {{Proc. International Conference on Software Engineering (ICSE 2017)}},
    year = {2017},
    publisher = {ACM},
    note = {To appear},
    }
  • J. Wang, J. Sun, Q. Yuan, and J. Pang. Should we learn probabilistic models for model checking? A new approach and an empirical study. In Proc. International Conference on Fundamental Approaches to Software Engineering (FASE 2017), volume 10202, LNCS, Springer, 2017, pp. 3-21.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Wang-Sun-Yuan-Pang17a,
    author = {Jingyi Wang and
    Jun Sun and
    Qixia Yuan and
    Jun Pang},
    title = {Should We Learn Probabilistic Models for Model Checking? {A} New Approach and An Empirical Study},
    booktitle = {{Proc. International Conference on Fundamental Approaches to Software Engineering (FASE 2017)}},
    series = {LNCS},
    volume = {10202},
    publisher = {Springer},
    pages = {3--21},
    year = {2017},
    doi = {10.1007/978-3-662-54494-5_1},
    pdf = {http://arxiv.org/abs/1605.08278},
    }

2016

  • L. D. X. Bach, Q. L. Le, D. Lo, and C. Le Goues. Enhancing automated program repair with deductive verification. In Proc. IEEE International Conference on Software Maintenance and Evolution (ICSME 2016), IEEE, 2016.
    [PDF] [Bibtex]
    @inproceedings{Bach-Le-Lo-LeGoues16a,
    author = {Le Dinh Xuan Bach and Quang Loc Le and David Lo and Claire {Le Goues}},
    title = {Enhancing Automated Program Repair with Deductive Verification},
    booktitle = {{Proc. IEEE International Conference on Software Maintenance and Evolution (ICSME 2016)}},
    publisher = {IEEE},
    year = {2016},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/icsme16-repair.pdf},
    note = {To appear},
    }
  • Y. Chen, C. M. Poskitt, and J. Sun. Towards learning and verifying invariants of cyber-physical systems by code mutation. In Proc. International Symposium on Formal Methods (FM 2016), volume 9995, LNCS, Springer, 2016, pp. 155-163.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Chen-Poskitt-Sun16a,
    author = {Yuqi Chen and Christopher M. Poskitt and Jun Sun},
    title = {Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation},
    booktitle = {{Proc. International Symposium on Formal Methods (FM 2016)}},
    series = {LNCS},
    volume = {9995},
    pages = {155--163},
    publisher = {Springer},
    year = {2016},
    doi = {10.1007/978-3-319-48989-6_10},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Chen-Poskitt-Sun.FM_.2016.pdf},
    }
  • M. Chen, T. H. Tan, J. Sun, J. Wang, Y. Liu, J. Sun, and J. S. Dong. Service adaptation with probabilistic partial models. In Proc. International Conference on Formal Engineering Methods (ICFEM 2016), volume 10009, LNCS, Springer, 2016, pp. 122-140.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Chen_et-al16a,
    author = {Manman Chen and
    Tian Huat Tan and
    Jun Sun and
    Jingyi Wang and
    Yang Liu and
    Jing Sun and
    Jin Song Dong},
    title = {Service Adaptation with Probabilistic Partial Models},
    booktitle = {{Proc. International Conference on Formal Engineering Methods (ICFEM 2016)}},
    pages = {122--140},
    series = {LNCS},
    volume = {10009},
    publisher  = {Springer},
    year = {2016},
    doi = {10.1007/978-3-319-47846-3_9},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/icfem2016-jingyi.pdf},
    }
  • C. Corrodi, A. Heußner, and C. M. Poskitt. A graph-based semantics workbench for concurrent asynchronous programs. In Proc. International Conference on Fundamental Approaches to Software Engineering (FASE 2016), volume 9633, LNCS, Springer, 2016, pp. 31-48.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Corrodi-HP16a,
    author = {Claudio Corrodi and Alexander Heu{\ss}ner and Christopher M. Poskitt},
    title = {A Graph-Based Semantics Workbench for Concurrent Asynchronous Programs},
    booktitle = {{Proc. International Conference on Fundamental Approaches to Software Engineering (FASE 2016)}},
    volume = {9633},
    series = {LNCS},
    pages = {31-48},
    publisher = {Springer},
    year = {2016},
    doi = {10.1007/978-3-662-49665-7_3},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Corrodi-HP.FASE_.2016.pdf},
    }
  • P. Kong, Y. Li, X. Chen, J. Sun, M. Sun, and J. Wang. Towards concolic testing for hybrid systems. In Proc. International Symposium on Formal Methods (FM 2016), volume 9995, LNCS, Springer, 2016, pp. 460-478.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Kong-et_al16a,
    author = {Pingfan Kong and Yi Li and Xiaohong Chen and Jun Sun and Meng Sun and Jingyi Wang},
    title = {Towards Concolic Testing for Hybrid Systems},
    booktitle = {{Proc. International Symposium on Formal Methods (FM 2016)}},
    series = {LNCS},
    volume = {9995},
    pages = {460--478},
    publisher = {Springer},
    year = {2016},
    doi = {10.1007/978-3-319-48989-6_28},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/HyChecker-FM2016.pdf},
    }
  • Q. L. Le, J. Sun, and W. Chin. Satisfiability modulo heap-based programs. In Proc. International Conference on Computer Aided Verification (CAV 2016), volume 9779, LNCS, Springer, 2016, pp. 382-404.
    [PDF] [DOI] [Bibtex]
    @inproceedings{LeSC16,
    author = {Quang Loc Le and
    Jun Sun and
    Wei-Ngan Chin},
    title = {Satisfiability Modulo Heap-Based Programs},
    booktitle = {{Proc. International Conference on Computer Aided Verification (CAV 2016)}},
    pages = {382--404},
    year = {2016},
    series = {LNCS},
    volume = {9779},
    publisher = {Springer},
    doi = {10.1007/978-3-319-41528-4_21},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/CAV16.pdf},
    }
  • L. Li, J. Sun, and J. S. Dong. Automated verification of timed security protocols with clock drift. In Proc. International Symposium on Formal Methods (FM 2016), volume 9995, LNCS, Springer, 2016, pp. 513-530.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Li-Sun-Dong16a,
    author = {Li Li and Jun Sun and Jin Song Dong},
    title = {Automated Verification of Timed Security Protocols with Clock Drift},
    booktitle = {{Proc. International Symposium on Formal Methods (FM 2016)}},
    series = {LNCS},
    volume = {9995},
    pages = {513--530},
    publisher = {Springer},
    year = {2016},
    doi = {10.1007/978-3-319-48989-6_31},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Li-Sun-Dong.FM_.2016.pdf},
    }
  • A. W. Lin, T. K. Nguyen, P. Rümmer, and J. Sun. Regular symmetry patterns. In Proc. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016), volume 9583, LNCS, Springer, 2016, pp. 455-475.
    [PDF] [DOI] [Bibtex]
    @inproceedings{LinNR016,
    author = {Anthony W. Lin and
    Truong Khanh Nguyen and
    Philipp R{\"{u}}mmer and
    Jun Sun},
    title = {Regular Symmetry Patterns},
    booktitle = {{Proc. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)}},
    pages = {455--475},
    series = {LNCS},
    volume = {9583},
    publisher = {Springer},
    year = {2016},
    doi = {10.1007/978-3-662-49122-5_22},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/VMCAI16.pdf},
    }
  • T. K. Nguyen, T. H. Tan, J. Sun, J. Li, Y. Liu, M. Chen, and J. S. Dong. Scaling BDD-based timed verification with simulation reduction. In Proc. International Conference on Formal Engineering Methods (ICFEM 2016), volume 10009, LNCS, Springer, 2016, pp. 363-382.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Nguyen_et-al16a,
    author  = {Truong Khanh Nguyen and Tian Huat Tan and Jun Sun and Jiaying Li and Yang Liu and Manman Chen and Jin Song Dong},
    title = {Scaling {BDD}-based Timed Verification with Simulation Reduction},
    booktitle  = {{Proc. International Conference on Formal Engineering Methods (ICFEM 2016)}},
    pages = {363--382},
    volume = {10009},
    series = {LNCS},
    publisher = {Springer},
    year = {2016},
    doi = {10.1007/978-3-319-47846-3_23},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/icfem2016-jiaying.pdf},
    }
  • X. Peng, J. Gu, T. H. Tan, J. Sun, Y. Yu, B. Nuseibeh, and W. Zhao. CrowdService: serving the individuals through mobile crowdsourcing and service composition. In Proc. International Conference on Automated Software Engineering (ASE 2016), ACM, 2016, pp. 214-219.
    [DOI] [Bibtex]
    @inproceedings{PengGT0YNZ16,
    author = {Xin Peng and
    Jingxiao Gu and
    Tian Huat Tan and
    Jun Sun and
    Yijun Yu and
    Bashar Nuseibeh and
    Wenyun Zhao},
    title = {{CrowdService}: serving the individuals through mobile crowdsourcing
    and service composition},
    booktitle = {{Proc. International Conference on Automated
    Software Engineering (ASE 2016)}},
    pages = {214--219},
    year = {2016},
    publisher = {ACM},
    doi = {10.1145/2970276.2970334},
    }
  • M. Schill, C. M. Poskitt, and B. Meyer. An interference-free programming model for network objects. In Proc. International Conference on Coordination Models and Languages (COORDINATION 2016), volume 9686, LNCS, Springer, 2016, pp. 227-244.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Schill-PM16a,
    author = {Mischael Schill and Christopher M. Poskitt and Bertrand Meyer},
    title = {An Interference-Free Programming Model for Network Objects},
    booktitle = {{Proc. International Conference on Coordination Models and Languages (COORDINATION 2016)}},
    volume = {9686},
    series = {LNCS},
    pages = {227-244},
    publisher = {Springer},
    year = {2016},
    doi = {10.1007/978-3-319-39519-7_14},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Schill-PM.Coordination.2016.pdf},
    }
  • S. Song, J. Hao, Y. Liu, J. Sun, H. Leung, and J. Zhang. Improved EGT-based robustness analysis of negotiation strategies in multiagent systems via model checking. IEEE Transactions on Human-Machine Systems, vol. 46, iss. 2, pp. 197-208, 2016.
    [PDF] [DOI] [Bibtex]
    @article{SongH00L016,
    author = {Songzheng Song and
    Jianye Hao and
    Yang Liu and
    Jun Sun and
    Ho-fung Leung and
    Jie Zhang},
    title = {Improved {EGT}-Based Robustness Analysis of Negotiation Strategies in
    Multiagent Systems via Model Checking},
    journal = {{IEEE Transactions on Human-Machine Systems}},
    volume = {46},
    number = {2},
    pages = {197--208},
    year = {2016},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/thms.pdf},
    doi = {10.1109/THMS.2015.2429573},
    }
  • S. Song, J. Zhang, Y. Liu, M. Auguston, J. Sun, J. S. Dong, and T. Chen. Formalizing and verifying stochastic system architectures using Monterey Phoenix. Software and System Modeling, vol. 15, iss. 2, pp. 453-471, 2016.
    [DOI] [Bibtex]
    @article{SongZLASDC16,
    author = {Songzheng Song and
    Jiexin Zhang and
    Yang Liu and
    Mikhail Auguston and
    Jun Sun and
    Jin Song Dong and
    Tieming Chen},
    title = {Formalizing and verifying stochastic system architectures using {Monterey}
    {Phoenix}},
    journal = {{Software and System Modeling}},
    volume = {15},
    number = {2},
    pages = {453--471},
    year = {2016},
    doi = {10.1007/s10270-014-0411-7},
    }
  • T. H. Tan, M. Chen, J. Sun, Y. Liu, É. André, Y. Xue, and J. S. Dong. Optimizing selection of competing services with probabilistic hierarchical refinement. In Proc. International Conference on Software Engineering (ICSE 2016), ACM, 2016, pp. 85-95.
    [PDF] [DOI] [Bibtex]
    @inproceedings{TanCSLAXD16,
    author = {Tian Huat Tan and
    Manman Chen and
    Jun Sun and
    Yang Liu and
    {\'{E}}tienne Andr{\'{e}} and
    Yinxing Xue and
    Jin Song Dong},
    title = {Optimizing selection of competing services with probabilistic hierarchical
    refinement},
    booktitle = {{Proc. International Conference on Software Engineering (ICSE 2016)}},
    pages = {85--95},
    year = {2016},
    doi = {10.1145/2884781.2884861},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/ICSE2016.pdf},
    publisher = {ACM},
    }
  • M. Tatsuta, Q. L. Le, and W. Chin. Decision procedure for separation logic with inductive predicates and presburger arithmetic. In Proc. Asian Symposium on Programming Languages and Systems (APLAS 2016), LNCS, Springer, 2016.
    [PDF] [Bibtex]
    @inproceedings{Tatsuta-Le-Chin16a,
    author = {Makoto Tatsuta and Quang Loc Le and Wei-Ngan Chin},
    title = {Decision Procedure for Separation Logic with Inductive Predicates and Presburger Arithmetic},
    booktitle = {{Proc. Asian Symposium on Programming Languages and Systems (APLAS 2016)}},
    series = {LNCS},
    publisher = {Springer},
    year = {2016},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/satsla-aplas16.pdf},
    note = {To appear},
    }

2015

  • G. Bai, J. Sun, J. Wu, Q. Ye, L. Li, J. S. Dong, and S. Guo. All your sessions are belong to us: Investigating authenticator leakage through backup channels on android. In Proc. International Conference on Engineering of Complex Computer Systems (ICECCS 2015), IEEE Computer Society, 2015, pp. 60-69.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Bai-et_al15a,
    author = {Guangdong Bai and
    Jun Sun and
    Jianliang Wu and
    Quanqi Ye and
    Li Li and
    Jin Song Dong and
    Shanqing Guo},
    title = {All Your Sessions Are Belong to Us: {Investigating} Authenticator Leakage
    through Backup Channels on Android},
    booktitle = {{Proc. International Conference on Engineering of Complex Computer Systems
    (ICECCS 2015)}},
    pages = {60--69},
    year = {2015},
    publisher = {IEEE Computer Society},
    doi = {10.1109/ICECCS.2015.17},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/ICECCS2015a.pdf},
    }
  • J. Hao, J. Sun, D. Huang, Y. Cai, and C. Yu. Heuristic collective learning for efficient and robust emergence of social norms. In Proc. International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2015), ACM, 2015, pp. 1647-1648.
    [PDF] [Bibtex]
    @inproceedings{Hao-et_al15a,
    author = {Jianye Hao and
    Jun Sun and
    Dongping Huang and
    Yi Cai and
    Chao Yu},
    title = {Heuristic Collective Learning for Efficient and Robust Emergence of
    Social Norms},
    booktitle = {{Proc. International Conference on Autonomous Agents
    and Multiagent Systems (AAMAS 2015)}},
    pages = {1647--1648},
    year = {2015},
    publisher = {ACM},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/AAMAS15.pdf},
    }
  • L. Li, J. Sun, Y. Liu, and J. S. Dong. Verifying parameterized timed security protocols. In Proc. International Symposium on Formal Methods (FM 2015), volume 9109, LNCS, Springer, 2015, pp. 342-359.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Li-Sun-Liu-Dong15a,
    author = {Li Li and
    Jun Sun and
    Yang Liu and
    Jin Song Dong},
    title = {Verifying Parameterized Timed Security Protocols},
    booktitle = {{Proc. International Symposium on Formal Methods (FM 2015)}},
    pages = {342--359},
    series = {LNCS},
    volume = {9109},
    publisher = {Springer},
    year = {2015},
    doi = {10.1007/978-3-319-19249-9_22},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Li-Sun-Liu-Dong15a.pdf},
    }
  • T. Wang, J. Sun, X. Wang, Y. Liu, Y. Si, J. S. Dong, X. Yang, and X. Li. A systematic study on explicit-state non-zenoness checking for timed automata. IEEE Transactions on Software Engineering, vol. 41, iss. 1, pp. 3-18, 2015.
    [PDF] [DOI] [Bibtex]
    @article{Wang-et_al15a,
    author = {Ting Wang and
    Jun Sun and
    Xinyu Wang and
    Yang Liu and
    Yuanjie Si and
    Jin Song Dong and
    Xiaohu Yang and
    Xiaohong Li},
    title = {A Systematic Study on Explicit-State Non-Zenoness Checking for Timed
    Automata},
    journal = {{IEEE Transactions on Software Engineering}},
    volume = {41},
    number = {1},
    pages = {3--18},
    year = {2015},
    doi = {10.1109/TSE.2014.2359893},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/tse2015.pdf},
    }
  • Z. Wu, Y. Liu, J. Sun, J. Shi, and S. Qin. GPU accelerated on-the-fly reachability checking. In Proc. International Conference on Engineering of Complex Computer Systems, (ICECCS 2015), IEEE Computer Society, 2015, pp. 100-109.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Wu-Liu-Sun-Shi-Qin15a,
    author = {Zhimin Wu and
    Yang Liu and
    Jun Sun and
    Jianqi Shi and
    Shengchao Qin},
    title = {{GPU} Accelerated On-the-Fly Reachability Checking},
    booktitle = {{Proc. International Conference on Engineering of Complex Computer Systems,
    (ICECCS 2015)}},
    pages = {100--109},
    year = {2015},
    publisher = {IEEE Computer Society},
    doi = {10.1109/ICECCS.2015.21},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/ICECCS2015b.pdf},
    }

2014

  • L. Li, J. Sun, Y. Liu, and J. S. Dong. TAuth: Verifying timed security protocols. In Proc. International Conference on Formal Engineering Methods (ICFEM 2014), volume 8829, LNCS, Springer, 2014, pp. 300-315.
    [PDF] [DOI] [Bibtex]
    @inproceedings{Li-Sun-Liu-Dong14a,
    author = {Li Li and
    Jun Sun and
    Yang Liu and
    Jin Song Dong},
    title = {{TAuth}: {Verifying} Timed Security Protocols},
    booktitle = {{Proc. International Conference on Formal Engineering Methods (ICFEM 2014)}},
    pages = {300--315},
    series = {LNCS},
    volume = {8829},
    publisher = {Springer},
    year = {2014},
    doi = {10.1007/978-3-319-11737-9_20},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/Li-Sun-Liu-Dong14a.pdf},
    }