 |
|
|
W3
Run-Time Result VerificationJuly 6,
1999 - Room 7-L |
|
|
"Run-Time
Result Verification" is a novel approach to the verification of digital systems:
the idea is to verify formally the correctness of the results of each run of the system
rather than the correctness of the system algorithm or code. For instance, rather than
proving in advance that (the code implementing) a compiler is correct, each individual run
of the compiler is followed by a validation phase which verifies that the target is a
correct compilation of the source program on this run. This approach is known as
"Translation Validation".
Run-Time Result Verification is robust to implementation changes and can be often used to
verify systems which are not available for examination or simply too difficult and
expensive to verify with standard practice in formal verification. Moreover, it can detect
run-time execution errors which cannot be detected with traditional formal verification
techniques. It has been recently applied with success to the certification of industrial
compilers (e.g. for translators for synchronous languages), mobile code and safety
critical software
Aim of the workshop
Program
Organizers
Invited and keynote speakers
Accepted
Papers
Registration
|
|
|
|
|
 |
