default search action
Yunja Choi
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j19]Yoel Kim
, Yunja Choi
PBE-Based Selective Abstraction and Refinement for Efficient Property Falsification of Embedded Software. Proc. ACM Softw. Eng. 1(FSE): 293-315 (2024) - [c27]Youngsul Shin, Seok-Won Lee, Yunja Choi:
Non-Functional Requirements Discovery and Quality Assurance Using Goal Model for Earthquake Warning System in Operation. RE 2024: 275-286 - 2023
- [j18]Yunja Choi
OS-in-the-Loop verification for multi-tasking control software. Softw. Test. Verification Reliab. 33(1) (2023) - 2020
- [j17]Yunja Choi
OS-Aware Interaction Model for the Verification of Multitasking Embedded Software. IEEE Access 8: 134987-134999 (2020) - [c26]Mingyu Park, Hoon Jang
Property-based testing for LG home appliances using accelerated software-in-the-loop simulation. ICSE (SEIP) 2020: 120-129
2010 – 2019
- 2019
- [c25]Dongwoo Kim, Yunja Choi:
Model Checking Embedded Control Software using OS-in-the-Loop CEGAR. ASE 2019: 565-576 - 2018
- [j16]Yunja Choi:
A configurable V&V framework using formal behavioral patterns for OSEK/VDX operating systems. J. Syst. Softw. 137: 563-579 (2018) - [j15]Dongwoo Kim, Yunja Choi:
A two-step approach for pattern-based API-call constraint checking. Sci. Comput. Program. 163: 19-41 (2018) - [c24]Yunho Kim, Yunja Choi, Moonzoo Kim:
Precise concolic unit testing of C programs using extended units and symbolic alarm filtering. ICSE 2018: 315-326 - [c23]Yunja Choi:
Automated Validation of IoT Device Control Programs Through Domain-Specific Model Generation. SEFM 2018: 254-268 - 2017
- [j14]Yunja Choi, Dongwoo Kim:
A Toolset for Validation and Verification of Automotive Control Software Using Formal Patterns. IEICE Trans. Inf. Syst. 100-D(7): 1526-1529 (2017) - [j13]Yunja Choi, Taejoon Byun:
Constraint-based test generation for automotive operating systems. Softw. Syst. Model. 16(1): 7-24 (2017) - [c22]Yoohee Chung, Dongwoo Kim, Yunja Choi:
Modeling OSEK/VDX OS Requirements in C. APSEC 2017: 398-407 - 2016
- [c21]Dongwoo Kim, Yoohee Chung, Yunja Choi:
Model-Based API-Call Constraint Checking for Automotive Control Software. APSEC 2016: 217-224 - [c20]Dongwoo Kim, Yunja Choi:
Light-Weight API-Call Safety Checking for Automotive Control Software Using Constraint Patterns. ICITCS 2016: 1-5 - 2015
- [j12]Yunja Choi, Mingyu Park, Taejoon Byun, Dongwoo Kim:
Efficient safety checking for automotive operating systems using property-based slicing and constraint-based environment generation. Sci. Comput. Program. 103: 51-70 (2015) - [c19]Taejoon Byun, Yunja Choi:
Automated system-level safety testing using constraint patterns for automotive operating systems. SAC 2015: 1815-1822 - 2014
- [j11]Yunja Choi:
Model checking Trampoline OS: a case study on safety analysis for automotive software. Softw. Test. Verification Reliab. 24(1): 38-60 (2014) - [c18]Yunja Choi, Min Zhang
Evaluation of Maude as a Test Generation Engine for Automotive Operating Systems. APSEC (1) 2014: 295-302 - [c17]Min Zhang
A Formal Semantics of the OSEK/VDX Standard in $${\mathbb {K}}$$ Framework and Its Applications. WRLA 2014: 280-296 - 2013
- [j10]Youngsul Shin, Yunja Choi, Woo Jin Lee:
Integration testing through reusing representative unit test cases for high-confidence medical software. Comput. Biol. Medicine 43(5): 434-443 (2013) - [j9]Yunja Choi:
Model Checking an OSEK/VDX-Based Operating System for Automobile Safety Analysis. IEICE Trans. Inf. Syst. 96-D(3): 735-738 (2013) - [c16]Yunja Choi:
Constraint Specification and Test Generation for OSEK/VDX-Based Operating Systems. SEFM 2013: 305-319 - 2012
- [j8]Moonzoo Kim, Yunho Kim, Yunja Choi:
Concolic testing of the multi-sector read operation for flash storage platform software. Formal Aspects Comput. 24(3): 355-374 (2012) - [j7]Yunja Choi, Moonzoo Kim:
Controlled composition and abstraction for bottom-up integration and verification of abstract components. Inf. Softw. Technol. 54(1): 119-136 (2012) - [j6]Christian Bunse, Yunja Choi, Hans-Gerhard Gross:
Evaluation of an Abstract Component Model for Embedded Systems Development. J. Inf. Process. Syst. 8(4): 539-554 (2012) - [c15]Mingyu Park, Taejoon Byun, Yunja Choi:
Property-based Code Slicing for Efficient Verification of OSEK/VDX Operating Systems. FTSCS 2012: 69-84 - 2011
- [j5]Yunja Choi, Christian Bunse:
Design verification in model-based μ-controller development using an abstract component. Softw. Syst. Model. 10(1): 91-115 (2011) - [c14]Yunja Choi:
Safety Analysis of Trampoline OS Using Model Checking: An Experience Report. ISSRE 2011: 200-209 - 2010
- [c13]Yunja Choi:
Systematic Composition and Verification of Abstract Components. COMPSAC 2010: 525-530 - [c12]Yunja Choi, Hoon Jang:
Reverse Engineering Abstract Components for Model-Based Development and Verification of Embedded Software. HASE 2010: 122-131
2000 – 2009
- 2009
- [c11]Yunja Choi:
Verification of an abstract component using communication patterns. MOMPES 2009: 42-52 - 2008
- [c10]Yunja Choi, Christian Bunse:
Towards Component-Based Design and Verification of a µ-Controller. CBSE 2008: 196-211 - [c9]Moonzoo Kim, Yunja Choi, Yunho Kim, Hotae Kim:
Pre-testing Flash Device Driver through Model Checking Techniques. ICST 2008: 475-484 - [c8]Moonzoo Kim, Yunja Choi, Yunho Kim, Hotae Kim:
Formal Verification of a Flash Memory Device Driver - An Experience Report. SPIN 2008: 144-159 - 2007
- [j4]Yunja Choi:
From NuSMV to SPIN: Experiences with model checking flight guidance systems. Formal Methods Syst. Des. 30(3): 199-216 (2007) - [j3]Yunja Choi:
Early Safety Analysis: from Use Cases to Component-based Software Development. J. Object Technol. 6(8): 185-203 (2007) - [c7]Yunja Choi:
Checking Interaction Consistency in MARMOT Component Refinements. SOFSEM (1) 2007: 832-843 - 2005
- [j2]Mats Per Erik Heimdahl, Yunja Choi, Michael W. Whalen:
Deviation Analysis: A New Use of Model Checking. Autom. Softw. Eng. 12(3): 321-347 (2005) - 2004
- [c6]Yunja Choi, Mats Per Erik Heimdahl:
Combination Model Checking: Approach and a Case Study. ASE 2004: 354-357 - [c5]Yunja Choi:
Model Checking Flight Guidance Systems: from Synchrony to Asynchrony. FMICS 2004: 61-79 - 2003
- [c4]Yunja Choi, Mats Per Erik Heimdahl:
Model Checking Software Requirement Specifications using Domain Reduction Abstraction. ASE 2003: 314-317 - 2002
- [j1]Yunja Choi, Sanjai Rayadurgam, Mats Per Erik Heimdahl:
Toward Automation for Model-Checking Requirements Specifications with Numeric Constraints. Requir. Eng. 7(4): 225-242 (2002) - [c3]Yunja Choi, Mats Per Erik Heimdahl:
Model Checking RSML-e Requirements. HASE 2002: 109-118 - [c2]Mats Per Erik Heimdahl, Yunja Choi, Michael W. Whalen:
Deviation Analysis Through Model Checking. ASE 2002: 37-46 - 2001
- [c1]Yunja Choi, Sanjai Rayadurgam, Mats Per Erik Heimdahl:
Automatic abstraction for model checking software systems with interrelated numeric constraints. ESEC / SIGSOFT FSE 2001: 164-174
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:22 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: