FAV: Informace pro studenty (zimní semestr 2011/2012)

Informace, termíny:

• Projekt: Do 30.10. je nutno registrovat nástroje, na které se jednotliví studenti zaměří. Bližší informace k projektu viz popis kurzu. 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.2011 23:59 CET.
• Průběžně doplněnovaný seznam zaregistrovaných studentů pro řešení projektu je uveden ZDE.

Přednášky

• Úvod, základní pojmy
• Logiky CTL*, CTL, LTL
• Explicitní model checking pro logiku CTL
• Binární rozhodovací diagramy (BDD)
• Symbolický model checking CTL
• LTL model checking, Büchiho automaty
• Partial Order Reduction
• Predicate Abstraction
• Abstract Interpretation
• Dataflow Analysis, Pointer Analyses
• SAT and SMT Solving

  Dodatečné přednášky (nejsou součástí zkoušky):

• Static analysis tools in the open source world (P. Muller)
• Shape analysis in Forester (J. Šimáček)
• Shape analysis in Predator (K. Dudka)

Monografie, přehledové články

• C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
• E.M. Clarke, O. Grumberg, D.A. Peled. Model Checking. MIT Press, 2000.
• A. Valmari. The State Explosion Problem. Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science 1491, Springer-Verlag 1998, pp. 429-528. (již poněkud starší, ale stále zajímavé)
• G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.
• M. Ben-Ari. Principles of the Spin Model Checker. Springer, 2008.

• F. Nielson, H.R. Nielson, C. Hankin. Principles of Program Analysis. Springer-Verlag, 2005.
• U. Khedker, A. Sanyal, B. Sathe. Data Flow Analysis: Theory and Practice. CRC Press, 2009.
• M.I. Schwartzbach. Lecture Notes on Static Analysis. BRICS, Department of Computer Science, University of Aarhus, Denmark, 2006.
• A.V. Aho, S. Lam, R. Sethi, J.D. Ullman.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. Část věnovaná statické analýze.
• B. Chess, J. West: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.

• A.R. Bradley, Z. Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.
• D. Kroening, O. Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2008.

• Y. Bertot, P. Castéran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer, 2010.
• B.C. Pierce. Types and Programming Languages. The MIT Press, 2002.
• B.C. Pierce (Ed.). Advanced Topics in Types and Programming Languages. The MIT Press, 2004.

Některé příbuzné kursy

• E.M. Clarke. Model Checking and Abstract Interpetation, 2011. Bug Catching: Automated Program Verification and Testing, 2011. Carnegie Mellon.
• J.-P. Katoen. Introduction to Model Checking, 2010. Advanced Model Checking, 2010. RWTH Aachen.
• T. Noll, C. Jansen, J. Heinen. Static Program Analysis, 2011. RWTH Aachen.
• A. Rybalchenko. Model Checking, 2011. TU Munich.
• A. Biere. Model Checking, 2010. Advanced Model Checking, 2011. JKU Linz.
• G. Holzmann. Logic Model Checking, 2011. Caltech.
• D. Kroening. Software Verification, 2011. Oxford University.
• H. Wehrheim. Model Checking. University of Paderborn, 2009.
• M.I. Schwartzbach. Static Analysis. BRICS, 2009.
• T. Henzinger. Model Checking. EPFL, 2007.

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.

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ů)

• Slam a Static Driver Verifier -- verifikace driverů v MS Windows s využitím predikátové abstrakce
• CPAchecker -- konfigurovatelný nástroj pro verifikaci software, zahrnuje model checking založený na predikátové abstrakci a interpolaci
• SatAbs -- verifikace programů v C s využitím predikátové abstrakce založené na SAT a zachovávající sémantiku operací v C prováděných na úrovni bitových vektorů
• Wolverine -- verifikace programů v C s využitím predikátové abstrakce založené na interpolaci
• CBMC -- omezený model checking C programů
• Threader -- predikátová abstrakce a modulární verifikace pro jednoduchou paralelní nadstavbu nad C programy
• Blast -- verifikace C programů (již starší nástroj), základem je predikátová abstrakce a interpolace
• Copper -- model checking paralelních C programů se sdílenými proměnnými a komunikací pomocí zasílání zpráv

• ARMC -- predikátová abstrakce nad C programy pro potřeby ověřování bezpečnosti i živosti (konečnosti)
• Terminator -- predikátová abstrakce pro potřeby ověřování konečnosti programů

• CHESS -- omezený model checking paralelních programů v C, Microsoft (na pomezí testování)
• dBug -- systematické testování (omezený model checking) paralelních programů v C využívajících pthreads i programů distribuovaných

• Kratos -- predikátová abstrakce pro potřeby verifikace HW v SystemC

• Java PathFinder -- JPF -- verifikace (i testování) Java programů

• SMV -- verifikace (nejen) HW (specializovaný vstupní jazyk, překladač z Verilogu) využívající BDD
• NuSMV -- reimplementace a rozšířeni SMV
• Uclid -- omezený model checking, ověřování ekvivalence a invariantů HW
• Incisive Formal Analysis -- komerční nástroj pro verifikaci hardware od Cadence
• RuleBase -- verifikace HW, IBM
• O-in -- verifikace HW, Mentor Graphics
• Magellan -- verifikace HW, Synopsys
• Jasper -- verifikace HW
• 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

• ...

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)

• 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 Insight -- 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++
• PolySpace -- komerční nástroje pro statickou analýzu vestavěných systémů reálného času v C, C++, Adě
• PREfast a další -- statická analýza u Microsoftu
• 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í a práce se zásobníkem

• Clang Static Analyzer -- statický analyzátor pro C a Objective C, využívá chybové vzory, analýzu toku dat
• 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 vzoru nad AST
• Splint -- statická analýza C programu, vyhledávání chybových vzorů v toku řízení, anotace pro zpřesnění analýzy
• Sparse -- statická analýza pro jádro Linuxu
• Stanse -- statická analýza nad C (chybové vzory, zamykání, uváznutí) vyvíjený na FI MU

• Space Invader -- nástroj pro verifikaci C programů zaměřený na manipulaci s dynamickými datovými strukturami (již starší nástroj)
• Predator -- nástroj pro verifikaci C programů zaměřený na manipulaci s dynamickými datovými strukturami vyvíjený na FIT VUT
• SLAyer -- nástroj pro verifikaci C programů zaměřený na manipulaci s dynamickými datovými strukturami vyvíjený v Microsoft Research
• jStar -- nástroj pro verifikaci Java programů zaměřený na manipulaci s dynamickými datovými strukturami
• CINV -- experimentální systém pro verifikaci komplexních vlastností programů se seznamy obsahujícími užitečná data

• KLEE -- kombinace statické analýzy založené na symbolickém provádění a testování
• Yogi -- statická analýza založená na symbolickém provádění a predikátové abstrakci

• SPEED -- symbolická analýza časových a prostorových nároků programů (tj. automatická analýza složitosti)

• ...

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

• PVS -- interaktivní theorem prover
• Coq -- interaktivní theorem prover
• HOL -- interaktivní theorem prover
• ACL2 -- interaktivní theorem prover

• SAT Competition -- soutěž o nejlepší nástroj pro řešení SAT problému
• Glucose -- SAT solver

• SMT-Comp -- soutěž o nejlepší nástroj pro řešení problémů SMT (SAT modulo teorie)
• Z3 -- SMT solver
• Barcelogic -- SMT solver
• CVC3 -- SMT solver
• Hampi -- nástroj pro řešení vztahů nad řetězci (využitelný např. při analýze webových útoků apod.)

• VCC -- verifikace anotovaných programů v C
• ESC/Java2 -- verifikace anotovaných programů v Javě

• ...

Další seznam nástrojů pro formální analýzu a verifikaci

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

• Přehled nástrojů pro statickou/dynamickou analýzu C kódu

• ConTest -- testování paralelních Java programů (kombinováno s výzkumem možností automatického sebe-opravování a využití formálních metod: projekt Shadows)
• SearchBestie -- prostředí pro testování paralelních Java programů založené na prohledávání prostoru parametrů testů vyvíjené na FIT VUT

• Valgrind -- dynamická analýza (založená na interpretaci) koretní práce s pamětí vlákny

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