Paper Info
Title
Certificate translation for the verification of concurrent programs
Abstract
The increasing presence of multicore execution environments is stimulating the development of concurrent software, an inherently error-prone task that affects the trust on the reliability of third-party code. There is thus a pressing need of providing verifiable evidence on a concurrent software correctness. Certificate Translation provides a means to generate verification certificates for complex functional properties. This technique, consists on progressively transferring verification results for source programs along a sequence of compilation steps. In previous work, we have shown how to transform certificates of a sequential program in the presence of compiler optimizations. In this article, we have shown that it is possible to extend certificate translation to the verification of concurrent programs, based on an Owicki/Gries-like proof system for a shared memory model.
Year
DOI
Venue
2010
10.1007/978-3-642-15640-3_16
TGC
Keywords
Field
DocType
increasing presence,gries-like proof system,verification result,concurrent program,compiler optimizations,concurrent software,compilation step,certificate translation,verification certificate,concurrent software correctness,compiler optimization,shared memory
Programming language,Shared memory model,Computer science,Software correctness,Optimizing compiler,Software,Verifiable secret sharing,Proof obligation,Multi-core processor,Certificate
Conference
Volume
ISSN
ISBN
6084
0302-9743
3-642-15639-8
Citations 
PageRank 
References 
3
0.39
12
Authors
1
Name
Order
Citations
PageRank
César Kunz116710.81