Introducing 

Prezi AI.

Your new presentation assistant.

Refine, enhance, and tailor your content, source relevant images, and edit visuals quicker than ever before.

Loading…
Transcript

int max_seq(int* p, int n) {

int res = *p;

for(int i = 0; i < n; i++) {

if (res < *p) { res = *p; }

p++;

}

return res;

}

Frama-C

Wtyczki

ACSL

INRIA-Saclay

 CEA–LIST

Frama-C

Przeglądanie kodu

Główne

zestaw narzędzi do analizy statycznej

Partnerzy

Zastosowania:

  • przeglądanie skomplikowanego kodu
  • dowodzenie własności
  • Value analysis
  • Jessie
  • Wp

ANSI/ISO C Specification Language

Wtyczki

  • Impact analysis
  • Scope & Data-flow browsing
  • Variable occurrence browsing

requires \valid(p) && \valid(q);

ensures *p <= *q;

Proving

Value

analysis

Frama-C

Inne

Zmienianie kodu

Framework

  • integracja wielu narzędzi
  • dobry start dla nowych rzeczy

Function contract

  • Aoraï (LTL)
  • metryki
  • ...
  • Semantic constant folding
  • Slicing
  • Spare code

void max_ptr(int *p, int* q) {

if (*p > *q) {

int tmp = *p;

*p = *q;

*q = tmp;

}

}

Żywy projekt

pre-condition

(requires)

  • manuale
  • tutoriale
  • blog
  • wiki
  • przykłady
  • grupy dyskusyjne

void max_ptr(int* p, int*q) {

*p = *q = 0;

}

post-condition

(ensures)

requires \valid(p) && \valid(q);

ensures *p <= *q;

ensures (*p == \old(*p) && *q == \old(*q)) ||

(*p == \old(*q) && *q == \old(*p));

int max_seq(int* p, int n);

Weryfikacja bezpieczeństwa

bezpieczeństwo pamięci

Jessie

void max_ptr(int *p, int* q) {

if (*p > *q) {

int tmp = *p;

*p = *q;

*q = tmp;

}

}

  • dereferencja wskaźników
  • dostęp do tablicy

bezpieczeństwo arytmetyki

  • przepełnienie
  • dzielenie przez zero
  • dowodzenie własności
  • specyfikacja w języku ACSL

terminacja

  • pętle
  • funkcje rekurencyjne

int max_seq(int* p, int n);

requires n > 0;

requires \valid(p+ (0..n−1));

ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];

ensures \exists int e; 0 <= e <= n−1 && \result == p[e];

requires n > 0;

requires \valid(p+ (0..n−1));

ensures \forall int i; 0 <= i <= n−1 ==>

\result >= p[i];

ensures \exists int e; 0 <= e <= n−1 &&

\result == p[e];

C + ACSL

ensures \forall int i; 0 <= i <= n−1 ==> p[i] == \old(p[i]);

Frama - C Core

/*

terminates c>0;

assigns \nothing;

*/

JAVA + JML

CIL + annot

Weryfikacja

funkcjonalności

Jessie Plugin

Krakatoa

void f (int c) { while(!c); return;}

requires n > 0;

requires \valid(p+ (0..n−1));

ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];

ensures \exists int e; 0 <= e <= n−1 && \result == p[e];

JESSIE

requires n > 0 &&\valid(p + (0..n−1));

ensures \result == \max(0,n−1,

\lambda integer i; p[i]);

Jessie2Why

  • funkcja robi to co trzeba
  • weryfikacja kontraktów

assigns \nothing;

WHY

VC Generator

/*

requires c!=0;

assigns \nothing;

*/

VC

void f (int c) { while(!c); return;}

Proof Assistants:

  • Coq
  • HOL
  • Isabelle/HOL
  • PVS

Automatic Provers:

  • Alt - Ergo
  • CVC3
  • Simplify
  • Yices
  • Z3

Demo

Learn more about creating dynamic, engaging presentations with Prezi