Software Languages & Systems Laboratory

• The main research themes are programming languages, compilers, and software engineering. The laboratory has studied on the design and implementation of programming languages, program analysis, and software testing for efficient development of defect free software, particularly, in the areas of Android applications and Internet-of-Things computing environments.

Research Areas

• Foundation technologies: Programming languages, Type systems, Compiler, Software Engineering, Program Analysis/Testing/Verification
• Applied technologies : Web, IoT, Android-based Mobile, Coding education

Major Research Results (~2019)

• Web programming languages
  • The design and implementation of unified/multi-tier programming languages
    1. A theory of RPC(Remote Procedure Call) calculi for Client-Server Model, 2019 (PDF , SLIDE)
    2. A Polymorphic RPC calculus, 2019, (PDF available soon)
• Android mobile applications
  • The design and implementation of a component-level exception handling mechanism
    1. A new Android-component-level exception mechanism for robustness of Android apps, 2015. (PDF)
  • A fuzz testing/a model-based testing for vulnerabilities
    1. Fuzz testing for Intent vulnerabilities on Android, 2018. (LINK)
    2. An Android BLE(Bluetooth Low Energy) Emulator for Testing Android Wearable Apps, 2018. (PDF)
  • A static analysis for component activation flows
    1. A type-based activation flow analysis of Android components for static analyses on Android apps, 2014. (PDF)
•  IoT Applications
  • The static analysis for SmartApps on Samsung SmartThings
    1. An Evaluation of the Quality of IoT Applications on the SmartThings Platform Using Static Analysis, 2019. (PDF available soon)
    2. SmartVisual: An event-flow based visualization for IoT applications on SmartThings platforms using static analysis, 2019. (PDF available soon)
  • The design and implementation of visual programming environment for SmartApps
    1. SmartBlock: A Visual Block Language and its Programming Environment for IoT, 2019. (PDF available soon)
  • The design and implementation of unified programming languages for IoT
    1. UniPy: A Unified Programming Language for Multiple-Tiered IoT Applications, 2019. (PDF)
• Coding Education
  • An open-source software for SmallBasic)
    1. A Java-based Small Basic programming environment for everyone, MySmallBasic (LINK)

Selected Publications

• Kwanghoon Choi, Byeong-Mo Chang, A Theory of RPC Calculi for Client-Server Model, Journal of Functional Programming (JFP), Vol.29, pp.1-39, Cambridge University Press, March 2019.
• Kwanghoon Choi, James Cheney, Simon Fowler, Sam Lindley, A Polymorphic RPC Calculus, 22th Brazilian Symposium on Formal Methods (SBMF), São Paulo, Brazil, November 27-29, 2019.
• Kwanghoon Choi, Myungpil Ko, Byeong-Mo Chang, A Practical Intent Fuzzing Tool for Robustness of Inter-Component Communication in Android Apps, KSII Transactions on Internet and Information Systems, Vol.12, Issue 9, pp.4248-4270, September 30, 2018.
• Byeong-Mo Chang, Kwanghoon Choi, A Review on Exception Analysis, Information and Software Technology, Vol.77, pp.1-16, September 2016.
• Kwanghoon Choi, Byeong-Mo Chang, A Lightweight Approach to Component-Level Exception Mechanism for Robust Android Apps, Computer Languages, Systems, and Structures, Vol.44, Part C, P.283-298, December 2015.
• Kwanghoon Choi, Byeong-Mo Chang, A Type and Effect System for Activation Flow of Components in Android Programs, Information Processing Letters, 114(11):620-627, November 2014.
• Kwanghoon Choi and Seog Park, Typing Zinc Machine with Generalized Algebraic Data Types, IEICE Transactions on Information and Systems, Vol.E94-D, No.6, pp.1190-1200, June 2011.
• Kwanghoon Choi and Atsushi Ohori, A Type Theory for Krivine-style Evaluation and Compilation, The Second Asian Symposium on Programming Languages and Systems (APLAS2004), Taipei, Taiwan, Volume 3302 of Lecture Notes in Computer Science, Springer-Verlag, pages 213-228, November 4-6, 2004.
• Kwanghoon Choi, Hyun-il Lim, and Taisook Han, Compiling Lazy Functional Programs Based on the Spineless Tagless G-machine for the Java Virtual Machine, Fifth International Symposium on Functional and Logic Programming (FLOPS), Waseda University, Tokyo, Japan, Volume 2024 of Lecture Notes in Computer Science, Springer-Verlag, pages 92-107, March 7-9, 2001.

소프트웨어언어 및 시스템 연구실

• 프로그래밍언어, 컴파일러, 소프트웨어공학에 관한 전공 분야를 연구합니다. 특히 소프트웨어 버그를 줄이거나 제거하는 소프트웨어를 만드는 기술을 연구합니다.
  1. 새로운 프로그래밍언어를 설계해서(타입시스템 기술) 버그 발생을 원천적으로 막기
  2. 프로그램을 실행하고 테스트하면서 버그를 찾기
  3. 프로그램을 실행하지 않고, 마치 사람이 눈으로 살피듯이 프로그램 소스를 훑어보는 정적 프로그램 분석 기술로 버그를 찾기.
• 이러한 기술들을 모바일, 웹, 사물인터넷, 클라우드와 같은 최신 컴퓨팅 환경에서의 소프트웨어 개발에 응용하는 프로젝트를 수행하고 있습니다.
• 연구학생 모집 공고 참고