plt formal methods resources
1.0.0
이미지 제공: Forsyte 그룹
형식적 방법은 소프트웨어 및 하드웨어 문제의 설계, 검증 및 사양에 사용되는 수학적 기술입니다. 이는 본질적으로 복잡한 컴퓨터 과학 문제를 연구하는 데 사용되는 프로그래밍 언어 이론 연구 의 하위 집합입니다.
형식적 방법에 의한 분석에는 기본적으로 다음 단계가 포함됩니다.
Formal SpecificationFormal ProofsModel CheckingAbstraction형식적 증명 개발 및 모델 확인은 주로 증명 보조 도구라고 불리는 대화형 정리 증명자를 사용하여 수행됩니다. 추상화는 모델의 부분들 사이에 구조적으로 건전한 관계를 생성하는 것입니다.
다음은 해당 분야에서 다가오는 과제와 함께 유용한 읽기 자료, 비디오 및 도구 목록을 선별하려는 시도입니다.
나는 현재의 연구와 산업적 응용에 더욱 초점을 맞춘 내용을 만들려고 노력했습니다. 순수 학술 컬렉션을 찾는 사람들은 교육의 형식적 방법(Formal Methods in Education - Jeremy Avigad)을 참조해야 합니다.
독자는 유형 이론 에 대한 기본 지식을 갖고 있어야 합니다. 더 많은 학문적 통찰력은 여기 learn-tt에서 찾을 수 있습니다.
소프트웨어 기초 : 이 분야에 깊이 빠져들기 위한 출발 자료로서 이 책을 적극 권장합니다. 이 책은 기본 개념을 구축하는 데 매우 도움이 되며 해당 분야에 대한 매우 건전한 소개 역할을 합니다. 연습할 수 있는 예제와 함께 아름답게 설명된 개념이 전체적으로 제공되어 학습 재미를 입증하는 대화형 정리를 만듭니다.
FRAP - Adam Chlipala : 프로그램의 형식적 정확성을 이해하고 추론하는 데 도움이 되는 책입니다. 명령형 언어( C )에서 영감을 받은 데이터 구조 및 알고리즘의 예는 공식 검증에 대해 생각하는 데 엄청난 도움이 됩니다.
종속 유형을 사용한 인증 프로그래밍 - Adam Chlipala : coq를 사용하여 증명하는 정리를 배울 수 있는 최고의 theoretical books 중 하나입니다.
형식 검증 - Jacques Fleuriot : SAT 및 SMT 솔버와 같은 좀 더 발전된 도구를 사용하여 정리를 증명하는 과정입니다.
추상 해석 - Patrick Cousot 추상 해석 이론에 관한 최고의 자료입니다. 이는 프로그램 돌연변이에 대한 완전하고 순수한 수학적 분석을 제공합니다. 서로 다른 추상적인 수학적 구조 사이의 관계를 지속적으로 수정하는 프로그램 동작이 설명되고 증명되었습니다!!
Logic and Proof - CMU & Lean 입문 : CMU에서 고안한 강좌이며, Lean에서 정리 증명을 위한 입문 자료로도 사용됩니다.
더 많은 이론적 통찰력이 필요하다고 생각되면 위의 참고를 참조하세요.
coq: 가장 유명하고 널리 사용되는 정리 증명자입니다. ML 추출, 프로젝트 패키징(프로젝트 및 Makefile 생성)을 포함한 많은 기능을 지원합니다. 공식화를 위해 coq를 사용하는 how-to 자료가 많이 있습니다. 누구나 Coq에서 매우 흥미로운 100가지 정리를 발견할 수 있습니다.
Lean: Microsoft Research 의 상당히 새로운 정리 증명자(Theorem Prover)입니다. 훌륭한 대화형 튜토리얼이 있어 시작하기 쉽습니다.
PRISM 모델 검사기 : 옥스포드 대학에서 개발한 모델 검사기입니다.
Nuprl : 증명 개선 논리 프로젝트 하에 Cornell 이 제작한 정리 증명자.
아그다: 꽤 성숙한 증거 보조자입니다. Coq과 유사한 기능을 가지고 있습니다. coq에 대한 경험을 쌓은 후에는 쉽게 배울 수 있습니다.
Isabelle: 그것은 오래된 정리 Prover입니다. 핵심 로직을 훌륭하게 구현했지만 다른 UX 관련 기능이 부족합니다.
VCC : Microsoft의 동시 C 프로그램에 대한 기계적 검증기입니다.
TLA+ : 모델링 언어 및 시스템(특히 동시 및 분산)을 위한 고급 언어입니다.
Z3
CVC4
수학SAT5
SMT인터폴
공주
Proof Assistant는 프로그램 로직을 매우 강력하게 구현합니다. 때로는 복잡한 증명을 사용하는 것만으로는 전술적으로 불가능할 수도 있습니다. 따라서 현재 연구에서는 강력한 논리 기반 추론 원리를 강력한 SMT 및 SMC 솔버와 결합하여 증명 개발을 용이하게 합니다. 몇 가지 예는 다음과 같습니다.
에프스타(F*)
SMTCoq
대부분의 프로젝트는 각각의 정리 증명자 또는 SAT/SMT/SMC/솔버의 개발이므로 여기서 찾아볼 수 있습니다. 다음은 적극적으로 개발된 다른 프로젝트 중 일부입니다.
DeepSpec은 검증된 소프트웨어 시스템 구축에 초점을 맞춘 포괄적인 프로젝트입니다. 다음과 같은 주요 하위 프로젝트가 활발히 진행되고 있습니다.
ikos는 추상 해석 이론을 기반으로 하는 신뢰할 수 있는 버그 없는 C 컴파일러입니다.
프로젝트 에베레스트(Project Everest): 안전하고 검증된 HTTPS 생태계 조성을 목표로 하는 연구 프로젝트입니다.
CertiCrypt: coq 증명 도우미를 사용하여 공개 키 암호화를 모델링하는 데 중점을 둔 프로젝트입니다.
Iris: Iris는 증명 도우미 Coq에서 구현되고 검증된 고차 동시 분리 논리 프레임워크입니다.
VeriDeep - 심층 신경망의 안전성 검증
VeHICal: 인간 사이버 물리 시스템에 대한 인터페이스 및 제어의 검증된 공동 설계 기반을 개발하는 데 중점을 둔 프로젝트입니다.
FastSMT - 공식 데이터 세트에 대한 성능을 최적화하는 방법을 학습하여 SMT 솔버를 강화하는 도구입니다. 이는 Z3 SMT 솔버를 기반으로 구축된 SRI 연구소인 ETH Zurich에서 개발되었습니다.
fm4cps - 사이버 물리 시스템을 위한 공식 방법, INRIA와 ECNU 상하이의 공동 노력.
블록체인을 위한 정형적 방법론 : 블록체인 기술에서 정형적 방법을 사용하는 것에 초점을 맞춘 최초의 워크숍입니다. 2019년 10월 11일 에 진행됩니다.
CertiK : 블록체인의 보안을 검증하기 위해 공식적인 방법을 사용하는 데 중점을 둔 스타트업입니다.
FLoC 2018 - 머신러닝 서밋이 형식적 방법을 충족합니다.
검증된 기계 학습 - Radboud University Nijmegen : 기계 학습에서 검증 방법을 사용하는 대학 과정입니다.
형식적 방법과 기계 학습의 만남 - RWTH Aachen University : 형식적 방법을 사용한 검증 가능하게 안전한 기계 학습의 발전에 관한 2018년 세미나.
독서
비디오
VeHICal : 인간 사이버 물리 시스템에 대한 인터페이스 및 제어의 검증된 공동 설계 기반을 개발하는 데 중점을 둔 프로젝트입니다.
fm4cps - 사이버 물리 시스템을 위한 공식 방법, INRIA와 ECNU 상하이의 공동 노력.
이는 특히 기존 프로그래밍 언어의 특정 속성(병렬성 및 동시성 등)을 개선하는 작업을 다룹니다. 결국 이것이 PL 이론을 연구하는 유일한 가장 중요한 이유이기 때문에 이와 관련하여 많은 것을 쉽게 찾아볼 수 있습니다. 여기에 나열된 모든 컨퍼런스 ACM SIGPLAN에는 프로그래밍 언어 개발에 관한 대부분의 연구 논문이 포함되어 있습니다.
어떤 제안이라도 환영합니다. 마음에 드신다면 풀 리퀘스트 제출을 고려해 보세요!!
