Differences

This shows you the differences between two versions of the page.

--- fv19:top [2019/06/18 21:59]
vkuncak [Introduction]
+++ fv19:top [2019/06/18 22:04]
vkuncak [Topics]
@@ Line 31: / Line 31: @@
 ===== Topics =====
-Importance of Reliable Systems. Methodology of Formal Verification. Soundness and Completeness in Modeling and Tools. Successful Tools and Flagship Case Studies
+  * Importance of Reliable Systems. Methodology of Formal Verification. Soundness and Completeness in Modeling and Tools. Successful Tools and Flagship Case Studies
+  * Review of Sets, Relations, Computability, Propositional and First-Order Logic Syntax, Semantics, Sequent Calculus.
+  * Completeness and Semi-Decidability for First-Order Logic. Inductive Definitions and Proof Trees. Higher-Order Logic and LCF Approach.
+  * State Machines. Transition Formulas. Traces. Strongest Postconditions and Weakest Preconditions.
+  * Hoare Logic. Inductive Invariants. Well-Founded Relations and Termination Measures
+  * Modeling Hardware: Verilog to Sequential Circuits
+  * Linear Temporal Logic. System Verilog Assertions. Monitors
+  * SAT Solvers and Bounded Model Checking
+  * Model Checking using Binary Decision Diagrams
+  * Loop Invariants. Hoare Logic. Statically Checked Function Contracts. Relational Semantics and Fixed-Point Semantics
+  * Symbolic Execution. Satisfiability Modulo Theories
+  * Abstract Interpretation and Predicate Abstraction
+  * Information Flow and Taint Analysis
+  * Verification of Security Protocols
+  * Dependent and Refinement Types
-Review of Sets, Relations, Computability, Propositional and First-Order Logic Syntax, Semantics, Sequent Calculus.
+===== Relevant Textbooks =====
-Completeness and Semi-Decidability for First-Order Logic. Inductive Definitions and Proof Trees. Higher-Order Logic and LCF Approach.
+  * Michael Huth and Mark Rayan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press 2004.
+  * Handbook of Model Checking, https://www.springer.com/de/book/9783319105741 Springer 2018. Including Chapter Model Checking Security Protocols by David Basin.
+  * Tobias Nipkow, Gerwin Klein: Concrete Semantics with Isabelle/HOL. http://concrete-semantics.org/concrete-semantics.pdf
+  * Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
+  * Nielson, Flemming, Nielson, Hanne R., Hankin, Chris: Principles of Program Analysis. ISBN 978-3-662-03811-6. Springer 1999.
+  * Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory (To Truth Through Proof), Springer 2002.
+  * http://logitext.mit.edu/tutorial
-State Machines. Transition Formulas. Traces. Strongest Postconditions and Weakest Preconditions.
+==== Additional Introductions and Background ====
-Hoare Logic. Inductive Invariants. Well-Founded Relations and Termination Measures
+  * Kenneth H. Rosen. Discrete Mathematics and Its Applications. E.g. 8th Edition.
+  * Formally Verified Software in the Real World. Communications of the ACM, October 2018. https://cacm.acm.org/magazines/2018/10/231372-formally-verified-software-in-the-real-world/fulltext
-Modeling Hardware: Verilog to Sequential Circuits
-Linear Temporal Logic. System Verilog Assertions. Monitors
-SAT Solvers and Bounded Model Checking
-Model Checking using Binary Decision Diagrams
-Loop Invariants. Hoare Logic. Statically Checked Function Contracts. Relational Semantics and Fixed-Point Semantics
-Symbolic Execution. Satisfiability Modulo Theories
-Abstract Interpretation and Predicate Abstraction
-Information Flow and Taint Analysis
-Verification of Security Protocols
-Dependent and Refinement Types