PV3 ⊧ Starlingchecks user-specified specifications for concurrent algorithms in a C-like language
Automated verification tool for concurrent programs.Application domain/field
- Concurrency
- Concurrent algorithms
Expected input
- Program
- Annotations, expressed as Concurrent Views Framework-style assertions
- Constraints binding assertions to concrete facts
Format:
- Program: C-like language
- Annotations: ?
- Constraints: ?