FAV
: Informace pro studenty (zimní semestr 2018/2019)



Informace, termíny:

Zde se objevují upozornění na nové závažné informace, blížící se termíny apod.


  • Projekt: Bližší informace k projektu viz popis kurzu. Do 23. 11. 2018 je nutno registrovat nástroje, na které se jednotliví studenti zaměří. Registraci proveďte zasláním emailu na mou adresu. Termín odevzdání vypracovaného eseje v pdf přes IS FIT je 14. 12. 2017 23:59 CET.
  • Průběžně doplněnovaný seznam zaregistrovaných studentů pro řešení projektu je uveden ZDE.


Přednášky



Monografie, přehledové články




Některé příbuzné kursy




Nástroje - experimentální i průmyslové


Upozornění: (1) Níže jsou uvedeny jen některé příklady existujících nástrojů, v žádném případě se nejedná o úplný seznam! (2) Uvedené krátké charakteristiky nebyly vždy získány na základě vlastní zkušenosti s příslušným nástrojem a nemusí být přesné -- naleznete-li nějakou nepřesnost či rozpor, prosím napište mi.

Competition on Software Verification (SV-COMP) -- mezinárodní soutěž ve verifikaci SW

Model checking

  • Spin -- verifikace (nejen) distribuovaných SW systémů, vstupem je specializovaný modelovací jazyk Promela (existují překladače do Promely z některých dalších jazyků)

  • CPAchecker -- konfigurovatelný nástroj pro verifikaci software, zahrnuje model checking založený na predikátové abstrakci a interpolaci
  • CBMC -- omezený model checking C programů
  • ESBMC -- omezený model checking C programů
  • Smack -- omezený model checking C programů v kombinaci s řadou dalších analýz
  • Blast -- verifikace C programů (již starší nástroj), základem je predikátová abstrakce a interpolace, nová verze je dostupná zde v rámci projektu Linux Driver Verification
  • Divine -- model checking v paralelním a distribuovaném prostředí s využitím řady vstupních formátů (včetně C/C++)
  • 2LS -- open source analyzátor spojující principy omezeného model checkingu, k-indukce a abstraktní interpretace
  • DiffBlue -- firma stojící za komercionalizací a dalším rozvojem např. CBMC či 2LS
  • Ultimate Automizer -- C model checker využívající predikátové abstrakce a teorie automatů

  • CHESS -- systematické testování, tedy v zásadě omezený model checking paralelních programů v C, Microsoft

  • Java PathFinder -- JPF -- verifikace (i testování) Java programů
  • JBMC -- omezený model checking Java programů

  • JKind -- nekonečně stavový model checking synchronních systémů popsaných v jazyce Lustre

  • NuSMV a NuXMV -- symbolický model checking (nejen) HW
  • ABC -- systém pro syntézu a verifikace HW (zahrnuje omezený model checking, včetně různých pokročilých technik vycházejících ze základních myšlenek BMC)
  • Incisive Formal Analysis -- komerční nástroj pro verifikaci hardware od Cadence
  • RuleBase -- verifikace HW, IBM
  • Questa Formal Verification Apps -- verifikace HW, Mentor Graphics
  • Static and Formal Verification at Synopsys -- verifikace HW, Synopsys
  • Jasper -- verifikace HW, Cadence
  • Oski -- společnost neprodukuje přímo nástroj, ale nabízí verifikaci s využitím model checkingu

  • Uppaal -- model checking RT systémů popsaných časovanými automaty

  • Prism -- pravděpodobnostní model checker nad Markovskými systémy
  • Storm -- pravděpodobnostní model checker nad Markovskými systémy

  • TTool -- simulační i formální verifikace spolehlivosti (safety), bezpečnosti (security) i výkonnosti vestavěných systémů modelovaných pomocí SysML/UML s využitím model checkingu i automatizovaného dokazování teorémů (security, kryptografie)

  • ...

Statická analýza, analýza toku dat, abstraktní interpretace, ...

  • Přehled nástrojů pro statickou/dynamickou analýzu C kódu
  • Seznam nástrojů pro statickou analýzu na Wikipedii
  • Zajímavé srovnání některých nástrojů pro statickou analýzu

  • FindBugs -- volně dostupný nástroj pro statickou analýzu Javy (chybové vzory, analýza toku dat)
  • SpotBugs -- nástupce FindBugs

  • Coverity -- komerční nástroje pro statickou analýzu C/C++/Java (chybové vzory, analýza toku dat, vylučování nereálných chyb)
  • Klocwork -- komerční nástroje pro statickou analýzu C/C++/Java/C# (chybové vzory, analýza toku dat, vylučování nereálných chyb)
  • CodeSonar -- komerční nástroje pro statickou analýzu C/C++ (chybové vzory, analýza toku dat, vylučování nereálných chyb)
  • PolySpace -- komerční nástroje pro statickou analýzu vestavěných systémů reálného času v C, C++, Adě (abstraktní interpretace)
  • Microsoft Code analysis for C/C++ -- statická analýza vestavěná do VisualStudia, (zřejmě) chybové vzory a symbolická exekuce založená na využití SMT (Z3), možnost anotací
  • Parfait -- interní nástroj v rámci Oracle, analýza toku dat, chybové vzory, ...
  • FramaC -- nástroj zahrnující abstraktní interpretaci pro C i deduktivní verifikaci C kódu anotovaného ACSL od francouzské agentury pro atomovou energii (CEA)
  • Facebook Infer -- komerční (ale open source) nástroj založený na abstraktní interpretaci zaměřený na vybrané typy chyb
  • Sparrow -- abstraktní interpretace, různé techniky pro zajištění korektnosti při zachování maxima škálovatelnosti

  • AbsInt a Astrée -- komerční nástroje pro statickou analýzu (abstraktní interpretaci) vestavěných systémů, zejména analýzu časování, práce se zásobníkem a ověřování absence runtime chyb (spolehlivá)

  • Daisy -- analýza toku dat a analýza založená na optimalizačních problémech pro analýzu a optimalizaci numerických programů

  • TAJS -- statická analýza pro JavaScript

  • gdfa: A Generic Data Flow Analyzer for GCC -- jednoduché generické prostředí pro tvorbu analýz toku dat (demonstrující principy z knihy Uday P. Khedker, Amitabha Sanyal, Bageshri Karkare: Data Flow Analysis: Theory and Practice)

  • Clang Static Analyzer -- statický analyzátor pro C a Objective C, využívá chybové vzory, analýzu toku dat
  • SonarQube -- analýza toku dat a chybové vzory pro vybrané chyby v kódu i zranitelnosti z hlediska bezpečnosti nad řadou různých jazyků
  • Cppcheck -- statický analyzátor pro C/C++, relativně jednoduché vyhledávání chybových vzorů v toku řízení
  • cppclean -- statická analýza programu v C++, vyhledávání chybových vzorů nad AST
  • Sparse -- statická analýza pro jádro Linuxu

  • Predator -- nástroj pro verifikaci C programů zaměřený na manipulaci s dynamickými datovými strukturami z FIT VUT (využívá grafy, v principu založen na separační logice)
  • Forester -- nástroj pro verifikaci C programů zaměřený na manipulaci s dynamickými datovými strukturami z FIT VUT (založen na stromových automatech)

  • AProVE -- kombinace abstraktní interpretace pro ověření korektnosti práce s pamětí a vystavění abstraktního modelu, následovaná různými technikami pro dokazování konečnosti běhu (s využitím SMT)

  • Weverca -- prostředí kombinující různé statické analýzy v podobě abstraktní interpretace pro potřeby verifikace PHP programů

  • Slam a Static Driver Verifier -- verifikace driverů v MS Windows, dříve s využitím predikátové abstrakce, nyní s využitím symbolické exekuce založené na SMT
  • KLEE -- kombinace statické analýzy založené na symbolickém provádění a testování
  • Symbiotic -- kombinuje instrumentaci kódu o monitory sledující verifikované vlastnosti, slicing a symbolickou exekuci

  • SPEED -- symbolická analýza časových a prostorových nároků programů (tj. automatická analýza složitosti)
  • Loopus -- statická analýza zaměřená na automatickou analýzu složitosti u celočíselných programů v C

  • ...

Theorem proving, SAT solving, SMT solving, rozhodovací procedury

Přehled nástrojů pro statickou analýzu C kódu
Další seznam nástrojů pro formální analýzu a verifikaci

Dynamická analýza, pokročilé testování

  • RoadRunner -- nástroj pro dynamickou analýzu paralelních Java programů
  • ANaConDA -- nástroj pro dynamickou analýzu paralelních C/C++ programů na binární úrovni vyvíjený na FIT VUT
  • Valgrind -- dynamická analýza (založená na interpretaci) korektní práce s pamětí, vlákny, ...

  • CSmith -- nástroj pro fuzz testování překladačů



Poslední modifikace: 3. December 2018
Připomínky k obsahu stránky posílejte na e-mail: vojnar@fit.vutbr.cz