Book chapter
Interactively verifying a simple real-time scheduler
Computer Aided Verification: 7th International Conference, CAV '95 Liège, Belgium, July 3–5, 1995 Proceedings, pp.395-408
International Computer Aided Verification, 7th (Liege, Belgium, 03-Jul-1995–05-Jul-1995)
Lecture Notes in Computer Science (LNCS), 939, Springer Berlin Heidelberg
1995
Abstract
This paper describes the interactive verification of a simple interrupt-driven real-time scheduler written in the machine code language of the MIPS R3000 RISC processor. The formal verification was carried out using the interactive theorem prover Ergo.
Details
- Title
- Interactively verifying a simple real-time scheduler
- Authors
- Colin Fidge (Author) - University of QueenslandPeter Kearney (Author) - University of QueenslandMark Utting (Author) - University of Queensland
- Contributors
- Pierre Wolper (Editor)
- Publication details
- Computer Aided Verification: 7th International Conference, CAV '95 Liège, Belgium, July 3–5, 1995 Proceedings, pp.395-408
- Conference details
- International Computer Aided Verification, 7th (Liege, Belgium, 03-Jul-1995–05-Jul-1995)
- Series
- Lecture Notes in Computer Science (LNCS); 939
- Publisher
- Springer Berlin Heidelberg
- Date published
- 1995
- DOI
- 10.1007/3-540-60045-0_65
- ISBN
- 3540600450
- Organisation Unit
- School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
- Language
- English
- Record Identifier
- 99449474102621
- Output Type
- Book chapter
Metrics
699 Record Views