Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/5022
Full metadata record
DC FieldValueLanguage
dc.contributor.authorda Cruz,Den
dc.contributor.authorHenriques,PRen
dc.contributor.authorJorge Sousa Pintoen
dc.date.accessioned2017-12-28T10:24:15Z-
dc.date.available2017-12-28T10:24:15Z-
dc.date.issued2013en
dc.identifier.urihttp://repositorio.inesctec.pt/handle/123456789/5022-
dc.identifier.urihttp://dx.doi.org/10.1109/compsac.2013.86en
dc.description.abstractA central issue in program verification is the generation of verification conditions (VCs): proof obligations which, if successfully discharged, guarantee the correctness of a program vis-a-vis a given specification. While the basic theory of program verification has been around since the 1960s, the late 1990s saw the advent of practical tools for the verification of realistic programs, and research in this area has been very active since then. Automated theorem provers have contributed decisively to these developments. This paper establishes a basis for the generation of verification conditions combining forward and backward reasoning, for programs consisting of mutually-recursive procedures annotated with contracts and loop invariants. We introduce also a visual technique to verify a program, in an interactive way, using Verification Graphs (VG), where a VG is a Control Flow Graph (CFG) whose edges are labeled with contracts (pre- and postconditions). This technique intends to help a software engineer to find statements that are not valid with respect to the program's specification.en
dc.languageengen
dc.relation5595en
dc.rightsinfo:eu-repo/semantics/openAccessen
dc.titleInteractive Verification of Safety-Critical Softwareen
dc.typeconferenceObjecten
dc.typePublicationen
Appears in Collections:HASLab - Other Publications

Files in This Item:
File Description SizeFormat 
P-008-KC3.pdf491.82 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.