зеркало из
https://github.com/iharh/notes.git
synced 2025-11-03 23:26:09 +02:00
63 строки
1.2 KiB
Plaintext
63 строки
1.2 KiB
Plaintext
Super !!!
|
|
MIT - Abstract Interpretation - http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/
|
|
|
|
Logical Relations (Predicates)
|
|
TAPL - 150
|
|
|
|
|
|
Discrete Math
|
|
Selezneva - MSU - Discrete Math
|
|
|
|
|
|
|
|
Logic
|
|
Zaharov - MSU - Math Logic
|
|
Paulson - Logic and Proof - local copy and http://www.cl.cam.ac.uk/teaching/1011/LogicProof/
|
|
|
|
|
|
Software Verification:
|
|
|
|
Meyer at ETH: http://se.inf.ethz.ch/courses/2011b_fall/sv/
|
|
|
|
|
|
Hoare Logic
|
|
|
|
Chakraborty - A Short Introduction to Hoare Logic
|
|
Aldrich - Hoare Logic
|
|
Mu - Program Construction and Reasoning
|
|
Heining - Program Verification using Hoare Logic - An Introduction
|
|
|
|
Java - JML/KeY-Hoare
|
|
|
|
|
|
Separation Logic:
|
|
|
|
Frohardt - A Brief Introduction to Separation Logic
|
|
Calgano - Program Verification using Separation Logic
|
|
Reinolds - An Introduction to Separation Logic
|
|
|
|
Yang - ER04 - Separation Logics And Applications
|
|
|
|
Parkinson - Ribbon Proofs for Separation Logic
|
|
Parkinson - An Introduction to Separation Logic
|
|
VanStaaden - An Introduction to Separation Logic
|
|
|
|
Meyer at ETH: http://se.inf.ethz.ch/courses/2011b_fall/seplogic/
|
|
|
|
OHern - Lectures on Separation Logic
|
|
|
|
|
|
Talks:
|
|
Kolanski - Introduction to Separation Logic 2008
|
|
and others
|
|
|
|
|
|
Tools:
|
|
JML/Key
|
|
jStar
|
|
|
|
|
|
Model Checking
|
|
Zaharov - MSU - Model Checking
|
|
|