| 1 |
1
적어도 하나의 불변식 후보를 포함하는 불변식 후보군을 생성하는 불변식 처리부; 및컨트랙트의 적어도 하나의 검증 대상을 획득하고, 상기 불변식 후보를 이용하여 상기 적어도 하나의 검증 대상 각각에 대한 검증 조건을 생성하는 검증부를 포함하고,상기 검증부는 상기 적어도 하나의 검증 대상 중에서 반환 대상을 검출하여 상기 불변식 처리부로 전달하되, 상기 반환 대상은 타당하지 않은 검증 조건에 대응하는 검증 대상을 포함하는,스마트 컨트랙트 검증 장치
|
| 2 |
2
제1항에 있어서,상기 불변식 처리부는 상기 적어도 하나의 반환 대상을 기반으로 상기 불변식 후보를 정제하여 새로운 불변식 후보군을 생성하고, 상기 새로운 불변식 후보군을 상기 검증부에 전달하는,스마트 컨트랙트 검증 장치
|
| 3 |
3
제2항에 있어서,상기 불변식 처리부는 미리 정의된 패턴의 수식을 포함하는 불변식을 검출하여 상기 불변식 후보로 결정함으로써 상기 불변식 후보를 정제하는,스마트 컨트랙트 검증 장치
|
| 4 |
4
제1항에 있어서,상기 검증부는 상기 검증 조건을 타당성 판단부로 전달하고, 상기 타당성 판단부는 상기 검증 조건에 대한 타당성을 판단한 후 판단 결과를 상기 검증부로 전달하고, 상기 검증부는 상기 판단 결과를 기반으로 상기 반환 대상을 검출하는 스마트 컨트랙트 검증 장치
|
| 5 |
5
제1항에 있어서,상기 검증부는 자유 변수 집합의 포함 관계 또는 미리 정의된 템플릿을 기반으로 상기 검증 조건의 타당성을 판단하는,스마트 컨트랙트 검증 장치
|
| 6 |
6
제4항 또는 제5항에 있어서,상기 검증부는 상기 검증 조건을 타당성 판단부로 전달하기 전에 또는 상기 검증 조건의 타당성을 판단하기 전에 상기 검증 조건을 간략화하는,스마트 컨트랙트 검증 장치
|
| 7 |
7
제1항에 있어서,상기 검증부는 상기 반환 대상이 부재한 경우 검증이 성공한 것으로 판단하는,스마트 컨트랙트 검증 장치
|
| 8 |
8
적어도 하나의 불변식 후보를 포함하는 불변식 후보군을 생성하는 단계;컨트랙트의 적어도 하나의 검증 대상을 획득하는 단계;상기 불변식 후보를 이용하여 상기 적어도 하나의 검증 대상 각각에 대한 검증 조건을 생성하는 단계; 상기 적어도 하나의 검증 대상 중에서 반환 대상을 검출하되, 상기 반환 대상은 타당하지 않은 검증 조건에 대응하는 검증 대상을 포함하는 단계를 포함하는 스마트 컨트랙트 검증 방법
|
| 9 |
9
제8항에 있어서,상기 적어도 하나의 반환 대상을 기반으로 상기 불변식 후보를 정제하여 새로운 불변식 후보군을 생성하는 단계를 더 포함하는,스마트 컨트랙트 검증 방법
|
| 10 |
10
제9항에 있어서,상기 적어도 하나의 반환 대상을 기반으로 상기 불변식 후보를 정제하여 새로운 불변식 후보군을 생성하는 단계는 미리 정의된 패턴의 수식을 포함하는 불변식을 검출하여 상기 불변식 후보로 결정하는 단계를 포함하는, 스마트 컨트랙트 검증 방법
|
| 11 |
11
제8항에 있어서,상기 적어도 하나의 검증 대상 중에서 반환 대상을 검출하는 단계는,상기 검증 조건에 대한 타당성을 판단하는 단계; 및상기 타당성의 판단 결과를 기반으로 상기 반환 대상을 검출하는 단계를 포함하는,스마트 컨트랙트 검증 방법
|
| 12 |
12
제8항에 있어서,자유 변수 집합의 포함 관계 또는 미리 정의된 템플릿을 기반으로 상기 검증 조건의 타당성을 판단하는 단계를 더 포함하는,스마트 컨트랙트 검증 방법
|
| 13 |
13
제11항 또는 제12항에 있어서,상기 검증 조건을 간략화하는 단계를 더 포함하는,스마트 컨트랙트 검증 방법
|
| 14 |
14
제8항에 있어서,상기 반환 대상이 부재한 경우 검증이 성공한 것으로 판단하는 단계를 더 포함하는,스마트 컨트랙트 검증 방법
|
