I am interested in designing secure-guaranteed systems using multiple formal techniques. I am actively looking for students (undergraduate and graduate) who are interested in all techniques and researches (testing, fuzzing, abstract interpretation, static analysis, formal verification) related to software (distributed systems, operating systems, and block chain) and neural network reliability, programming language related researches, system software securities, and machine learning model optimization framework techniques.

저는 다수의 형식 기법을 사용하여 보안이 보장된 시스템을 설계하는 데 관심이 있습니다. 소프트웨어(분산 시스템, 운영 체제 및 블록체인) 및 신경망 신뢰성과 관련된 모든 기법 및 연구(테스팅, 퍼징, 추상 해석, 정적 분석, 정형 검증), 프로그래밍 언어 관련 연구, 시스템 소프트웨어 보안, 머신러닝 모델 최적화 프레임워크 기법에 관심 있는 학생(학부 및 대학원)을 적극적으로 찾고 있습니다.

CertiKOS: an extensible architecture for building certified concurrent OS kernels

Certified concurrent abstraction layers

Building certified concurrent OS kernels

Safety and Liveness of MCS Lock—Layer by Layer

Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems

WormSpace

Adore: atomic distributed objects with certified reconfiguration

LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs

The Effect of College Students’ Mentoring on Adaptation to Campus Life and Satisfaction: with Focus on Difference Comparison by Trust on Mentor of Students with Food Service Major

AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects

Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance

A Study on How Barista's Ethical-Consumption Consciousness Effects to Sale of Fair-Trading Coffee

Fine-Grained Function Visibility for Multiple Dispatch with Multiple Inheritance

A study on how the catering service menus made with local food effects of consumer’s satisfaction – Focused on university students in Jeonju -

<mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si240.svg" display="inline" id="d1e223"> <mml:mi mathvariant="normal">SimplMM</mml:mi> </mml:math> : A simplified and abstract multicore hardware model for large scale system software formal verification

The Effect of Mentoring Functions in Foodservice Company on Organizational Commitment - Focused on Mediating Effect of Trust toward Supervisor -

Behavioral Intention Analysis Applying Confucian Culture Consumer Behavior Model: A Focus on Starbucks

Impacts of Sub-elements in Instagramming by Restaurant Service Providers on the Impression and Purchase Choice

Application of Fractal Dimension Analysis to Dance Evaluation

{CertiKOS}: An extensible architecture for building certified concurrent {OS} kernels

Safety and liveness of MCS lock—layer by layer

WormSpace: A modular foundation for simple, verifiable distributed systems

ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol

SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification

Fine-grained function visibility for multiple dispatch with multiple inheritance

Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness

Compositional Model-Driven Verification of Weakly Consistent Distributed Systems

ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions

Proving FFMM type safety using coq

PROMISE: Proof Automation as Structural Imitation of Human Reasoning.

On the Decompositionality of Neural Networks.

ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol.

Adore: Atomic Distributed Objects with Certified Reconfiguration

Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems

WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems

Certified Concurrent Abstraction Layers

CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels

ThreadAbs: A Template for Building Verified Thread-local Interfaces with Software Scheduler Abstractions

SimplMM: A Simplified and Abstract Multicore Hardware Model for Large Scale System Software Formal Verification

Building Certified Concurrent OS Kernels

Write-Once-Registers: A Modular Foundation for Simple, Verifiable Distributed Systems

정형 검증을 통한 동시성 소프트웨어의 추상화 명세 제공 (Provide abstracted specifications for concurrent software with formal verification)

Formal Computing and AI Lab.

교수님 소개

Jieung Kim

연구실 소개

연구실 키워드

알럼나이가 간 회사

연구실 지원 방법

대우 조건

연도별 논문 인용수

저널 & 학회 논문 출판 수

연구실 논문 목록

PROMISE: Proof Automation as Structural Imitation of Human Reasoning.

On the Decompositionality of Neural Networks.

ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol

연구실 보유 특허

대학별 입시끈

우리 연구실 모집

교수님 소개

Jieung Kim

연구실 키워드

알럼나이가 간 회사

연구실 지원 방법

대우 조건

연도별 논문 인용수

저널 & 학회 논문 출판 수

연구실 논문 목록

PROMISE: Proof Automation as Structural Imitation of Human Reasoning.

On the Decompositionality of Neural Networks.

ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol

연구실 보유 특허

최근 3년간 연구실적 높은 연구실

대학별 입시끈

우리 연구실 모집