VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
Abstract. We reflect on the formal development models applicable to embedded control systems in light of our experience with safety-critical applications from the aerospace domain....
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
What You See Is Not What You eXecute: computers do not execute source-code programs; they execute machine-code programs that are generated from source code. Not only can the WYSINW...
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
After some general remarks about program verification, we introduce separation logic, a novel extension of Hoare logic that can strengthen the applicability and scalability of pro...
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
Abstract. The Verifying Compiler checks the correctness of the program it compiles. The workhorse of such a tool is the reasoning engine, which decides validity of formulae in a su...
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
: Verifying design instead of code can be an effective and practical approach to obtaining verified software. This paper argues that proof scores are an attractive method for ver...
VSTTE
2005
Springer
13 years 9 months ago
2005
Springer
Abstract. Many well-established concepts of object-oriented programming work for individual objects, but do not support object structures. The development of a verifying compiler r...