Interactive verification of safety-critical software

A 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, th...

Full description

Bibliographic Details
Main Author: Cruz, Daniela da (author)
Other Authors: Henriques, Pedro Rangel (author), Pinto, Jorge Sousa (author)
Format: conferencePaper
Language:eng
Published: 2013
Subjects:
Program Verification
Verification Conditions
Interactive Verification
Labeled control flow graphs
Strongest postconditions
Weakest preconditions
Science & Technology
Online Access:http://hdl.handle.net/1822/26406
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/26406

Internet

http://hdl.handle.net/1822/26406

Similar Items