Software Verification and Validation - Segédanyagok

Félév: 2019. ősz
Title	Egyedi szöveg
L06 (10.02): Checking LTL properties	Checking LTL properties
L07 (10.03): Checking CTL properties	Checking CTL properties
L08 (10.09): Handling large state space in model checking	Symbolic model checking Bounded model checking
L09 (10.10): Model checking examples	Introductory examples Scheduling of tasks The Meltdown vulnerability Example models (ZIP)
L10 (10.16): Formal verification of time-dependent behavior	Formal verification of time-dependent behavior
L11 (10.17) Formal verification of stochastic properties	Formal verification of stochastic properties Reliability modeling with stochastic model checking
L12 (10.24): Model checkers and applications	Model checkers: SPIN and NuSMV Case study: Model checking PLC programs at CERN
L13 (10.30): Equivalence checking between models	Equivalence checking between models
L14 (10.31): Verification of the source code	Verification of the source code
L15 (11.06): Proof of program correctness (part 1)	Proof of program correctness for simple programs
L16 (11.07): Proof of program correctness (part 2)	Proof of program correctness for structured programs
L17 (11.13) Software model checking	Software model checking with abstraction
L18 (11.14) Software module testing	Software module testing (component testing)
L19 (11.20) Code-based test generation	Code-based test generation
L20 (11.21) Integration testing, system testing, validation testing	Integration testing, system testing, validation testing
L21 (11.27) Model-based testing (part 1)	Model based testing (part 1)
L22 (11.28) Model based testing (part 2)	Model based testing (part 2)
L23 (12.04): Verification during maintenance	Verification during maintenance

Félév: 2018. ősz
Title	Egyedi szöveg
L01: Introduction	Course overview Introduction to software V&V
L02: Verification of the requirements specification	Verification of the requirements specification
L03: Verification of the architecture design	Verification of the architecture design
L04: Verification of the detailed design	Verification of the detailed design Basic formalisms for formal verification
L05: Formalization of properties using temporal logics. Checking HML properties.	Temporal logics and checking HML properties
L06: Checking LTL properties	Checking LTL properties
L07: Checking CTL properties	Checking CTL properties