107
Voted
VSTTE
2005
Springer
15 years 8 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....
99
Voted
VSTTE
2005
Springer
15 years 8 months ago
2005
Springer
112
Voted
VSTTE
2005
Springer
15 years 8 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...
115
Voted
VSTTE
2005
Springer
15 years 8 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...
84
Voted
VSTTE
2005
Springer
15 years 8 months ago
2005
Springer
137
Voted
VSTTE
2005
Springer
15 years 8 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...
108
Voted
VSTTE
2005
Springer
15 years 8 months ago
2005
Springer
91
Voted
VSTTE
2005
Springer
15 years 8 months ago
2005
Springer
116
Voted
VSTTE
2005
Springer
15 years 8 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...
101
Voted
VSTTE
2005
Springer
15 years 8 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...