A generalized program verification workflow based on loop elimination and SA form

This paper presents a minimal model of the functioning of program verification and property checking tools based on (i) the encoding of loops as non-iterating programs, either conservatively, making use of invariants and assume/assert commands, or in a bounded way; and (ii) the use of an intermediat...

Full description

Bibliographic Details
Main Author: Belo Lourenco, Claudio (author)
Other Authors: Frade, M. J. (author), Pinto, Jorge Sousa (author)
Format: conferencePaper
Language:eng
Published: 2019
Subjects:
bounded verification
deductive verification
hoare logic
loop encoding
single assignment programs
Science & Technology
Online Access:http://hdl.handle.net/1822/66206
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/66206

Internet

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

Similar Items