RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
about
|
people
|
publications
|
research
|
education
|
industry
|
conferences
|
media
|
projects
internal
  
search:
  
  • @inproceedings{RISC4429,
    author = {Wolfgang Schreiner},
    title = {{Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs}},
    booktitle = {{Proceedings First Workshop on CTP Components for Educational Software (THedu'11)}},
    language = {english},
    abstract = {We present an approach to program reasoning which inserts between a program and its verification conditions an additional layer, the denotation of the program expressed in a declarative form. The program is first translated into its denotation from which subsequently the verification conditions are generated. However, even before (and independently of) any verification attempt, one may investigate the denotation itself to get insight into the "semantic essence" of the program, in particular to see whether the denotation indeed gives reason to believe that the program has the expected behavior. Errors in the program and in the meta-information may thus be detected and fixed prior to actually performing the formal verification. More concretely, following the relational approach to program semantics, we model the effect of a program as a binary relation on program states. A formal calculus is devised to derive from a program a logic formula that describes this relation and is subject for inspection and manipulation. We have implemented this idea in a comprehensive form in the RISC ProgramExplorer, a new program reasoning environment for educational purposes which encompasses the previously developed RISC ProofNavigator as an interactive proving assistant.},
    series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
    number = {79},
    pages = {124--142},
    address = {Wroclaw, Poland, July 31, 2011},
    isbn_issn = {ISSN: 2075-2180},
    year = {2012},
    month = {February},
    editor = {Pedro Quaresma and Ralph-Johan Back},
    refereed = {yes},
    keywords = {formal methods, program verification, computer science education},
    length = {19},
    url = {http://dx.doi.org/10.4204/EPTCS.79.8}
    }