Atlas home || Conferences | Abstracts | about Atlas
Homepage: http://afrodite.itc.it:1024/~leaf/rtrv.html
Organizers: Fausto Giunchiglia (IRST, Italy), Wolfgang Goerigk (University of Kiel, Germany), William Pase (Canada), Amir Pnueli (PC chair, Weizmann Institute of Science, Israel), Michael Siegel (University of Kiel, Germany), Eli Singerman (SRI, USA), Paolo Traverso (PC chair, IRST, Italy), Adolfo Villafiorita (local organization, IRST)
Deadline for abstracts: March 28, 1999
Description:
"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.
The aim of the workshop is to bring together active researchers in this emerging research area to discuss scientific issues and industrial applications. The workshop will feature both invited talks and contributed presentations with ample time for discussion. We encourage contributed talks to present both final results and work in progress.
Date received: February 07, 1999
© 2008 Atlas Conferences Inc.