Sound, modular and compositional verification of the input/output behavior of programs
We present a sound verification approach for verifying input/output properties of programs. Our approach supports defining high-level I/O actions on top of low-level ones (compositionality), defining input/output actions without taking into account which other actions exist (modularity), and other features.
Tue 14 AprDisplayed time zone: Azores change
14:00 - 16:00
|Segment Abstraction for Worst-Case Execution Time Analysis|
|Automatic Static Cost Analysis for Parallel Programs|
|Sound, modular and compositional verification of the input/output behavior of programs|
|Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs|