Verification Condition Generation and Variable Conditions in Smallfoot
classification
💻 cs.LO
cs.PL
keywords
conditionssmallfootusedvariableverificationalgorithmanalysisannotated
read the original abstract
These notes are a companion to [1] which describe - the variable conditions that Smallfoot checks, - the analysis used to check them, - the algorithm used to compute a set of verification conditions corresponding to an annotated program, and - the treatment of concurrent resource initialization code.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.