Studying Verification Conditions for Imperative Programs

Lourenço, Cláudio Belo; Pinto, Jorge Sousa; Lamraoui, Si-Mohamed; Nakajima, Shin

Studying Verification Conditions for Imperative Programs

Citation:: Lourenço CB, Lamraoui S-M, Nakajima S, Pinto JS. 2015. Studying Verification Conditions for Imperative Programs. ECEASSTvv. 72

Abstract:

n/a

Notes:

n/a

Website

Citation Key:

DBLP:journals/eceasst/LourencoLNP15

Preview	Attachment	Size
	1011-3093-1-pb.pdf	434.46 KB

Recent Publications

Lourenço CB, Lamraoui S-M, Nakajima S, Pinto JS. 2015. Studying Verification Conditions for Imperative Programs. ECEASSTvv. 72 Abstract1011-3093-1-pb.pdf

n/a

Lourenço CB, Frade MJ, Pinto JS. 2014. A Bounded Model Checker for SPARK Programs. Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis. Abstracttool-paper-atva2014.pdf

This paper discusses the design and implementation of a bounded model checker for SPARK code, and provides a proof of concept of the utility and practicality of bounded verification for SPARK.

publications

Cláudio Belo Lourenço

Software Engineering

Studying Verification Conditions for Imperative Programs

Abstract:

Notes:

Citation Key:

Recent Publications