HOME / 연구센터소개 / 산학연구실 소개










SMT-based Verification for Multithreaded Java with Java Memory Model
Under Approximation Refinement with SPIN Model Checker
Checking Well-Formedness Rules of AUTOSAR Model
SMT 해결기를 이용한 자바 메모리 모델 시뮬레이션
만족가능성 처리기를 이용한 이진 변수 서브시퀀스 추출
이진 기수 조건에서 인접성 표현을 위한 최적화된 CNF 변환
병행성 분석을 위한 액션 기반의 LTS 바운드 모델 체커
모델 검증 도구를 이용한 극단 인터리빙 분석
모델 체킹에서 하위 근사화 적용 경험
Japanese Puzzle as a SAT Problem
Using Boolean Cardinality Constraint for LTS Bounded Model Checking
수도쿠 퍼즐을 통해서 살펴본 SAT에서 전처리 효과
자바 메모리 모델을 이용한 멀티 스레드 자바 코드 검증
Bounded Model Checking for Labeled Transition System


안전성 검증 기술
본 연구실은 소프트웨어의 안전성 검증에 사용되는 다양한 테스팅 기법 및 모델 검증 기술을 확보하고 있다. 또한 모델 검증 도구인 SMV, SPIN 등에 대한 풍부한 활용 경험을 갖고 있다.
만족가능성 판정 기술
실 세계의 많은 문제들을 만족가능성 문제로 풀이할 수 있다. 본 연구실은 만족가능성 판정 기술을 수도쿠, 네모라이즈, 지뢰 찾기 등의 다양한 문제에 적용한 경험을 갖고 있다. 또한 만족가능성 판정 도구인 SAT solver 및 SMT solver 들에 대한 풍부한 활용 경험을 갖고 있다.
UML 모델링 및 분석 기술
UML은 산업계에서 사용되는 모델링 표준 언어이다. 본 연구실에서는 UML2.0 및 프로파일을 이용한 모델 작성 및 모델 분석 기술을 확보하고 있다. 또한 UML을 지원하는 상용 및 오픈 소스 기반의 CASE 도구에 대한 풍부한 활용 경험을 갖고 있다.