Embedded Files
Introduction to Formal Methods
Introduction to Formal Methods
Următoarele doua referințe oferă o vedere generală despre ce sunt metodele formale și de ce sunt importante:
IOANA RODHE, MARTIN KARRESAND. Overview of formal methods in software engineering. FOI-R--4156--SE.
Formal Methods for Software Specification and Analysis: An Overview. MIT
Many Sorted Logic
Many Sorted Logic
Some General Logic-Related Concepts
Many-sorted First-Order Logic
Syntax
Semantics
A Hilbert-style Proof System
msl.pdfInduction and Recursion
Induction and Recursion
A Common Framework for Induction and Coinduction
Motivation
Theoretical Foundation
Inductive Sets Defined by Ground Rules
Induction at Work
Natural Numbers
Lists
Trees
Functions (and Predicates) Recursively Defined
induction-and-recursion.pdfCoinduction and Corecursion
Coinduction and Corecursion
Recap: A Common Framework for Induction and Coinduction
Motivation
Coinductive Sets Defined by Ground Rules
Coinduction at Work
Conatural Numbers
Finite and Infinite Lists
Streams (Infinite Lists)
Functions (and Predicates) Corecursively Defined
coinduction-and-corecursion.pdfFormal Definition of Programming Languages
Formal Definition of Programming Languages
Syntax
Semantics
Big-Step SOS
Small-Step SOS
formal-def-prog-lang.pdf Floyd-Hoare Logic
Floyd-Hoare Logic
Program Specification
The Proof System
Total Correctness
Weakest Precondition Calculus
Proof Tableaux and Verification Condition
Examples
Strongest Postcondition
Possible Extensions
History
floyd-hoare-logic.pdfSpecification and Verification of Classes (Design by Contracts)
Specification and Verification of Classes (Design by Contracts)
Extending the Language with Functions
Extending Floyd-Hoare Logic with Functions
Classes
contracts.pdfSpecification and Verification of Classes in Dafny
Specification and Verification of Classes in Dafny
This is a demo-based presentation
Liskov Substitution Principle
Liskov Substitution Principle
The Liskov Substitution Principle (LSP), Intuitively
Behavioral Type of a Class
The Liskov Substitution Principle, More Formally
The Liskov Substitution Principle in Dafny
liskov.pdfStatic Program Analysis - Collecting Semantics
Static Program Analysis - Collecting Semantics
Motivation
2Demo
DFA Framework
Control Flow Graph (CFG)
Collecting Semantics
spa-colsem.pdfStatic Program Analysis - Abstract Interpretation and Abstract Semantics
Static Program Analysis - Abstract Interpretation and Abstract Semantics
Motivation
Abstract Interpretation
Abstract Semantics
spa-ai.pdfStatic Program Analysis - Dataflow Analysis
Static Program Analysis - Dataflow Analysis
Motivation
Dataflow Framework
Extensions
spa-df.pdfStatic Program Analysis - Inter-Procedural Analysis
Static Program Analysis - Inter-Procedural Analysis
Motivation
Inter-procedural Control Flow Graph (CFG)
Context Sensitive Analysis
spa-interp.pdfPage updated
Google Sites
Report abuse