Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
fv19:top [2019/06/18 22:03] vkuncak |
fv19:top [2019/06/18 22:04] vkuncak [Topics] |
||
---|---|---|---|
Line 31: | Line 31: | ||
===== Topics ===== | ===== 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. | |
- | 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. | |
- | Completeness and Semi-Decidability for First-Order Logic. Inductive Definitions and Proof Trees. Higher-Order Logic and LCF Approach. | + | * Hoare Logic. Inductive Invariants. Well-Founded Relations and Termination Measures |
- | + | * Modeling Hardware: Verilog to Sequential Circuits | |
- | State Machines. Transition Formulas. Traces. Strongest Postconditions and Weakest Preconditions. | + | * Linear Temporal Logic. System Verilog Assertions. Monitors |
- | + | * SAT Solvers and Bounded Model Checking | |
- | Hoare Logic. Inductive Invariants. Well-Founded Relations and Termination Measures | + | * Model Checking using Binary Decision Diagrams |
- | + | * Loop Invariants. Hoare Logic. Statically Checked Function Contracts. Relational Semantics and Fixed-Point Semantics | |
- | Modeling Hardware: Verilog to Sequential Circuits | + | * Symbolic Execution. Satisfiability Modulo Theories |
- | + | * Abstract Interpretation and Predicate Abstraction | |
- | Linear Temporal Logic. System Verilog Assertions. Monitors | + | * Information Flow and Taint Analysis |
- | + | * Verification of Security Protocols | |
- | SAT Solvers and Bounded Model Checking | + | * Dependent and Refinement Types |
- | + | ||
- | 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 | + | |
===== Relevant Textbooks ===== | ===== Relevant Textbooks ===== |