资 源 简 介
We consider the problem of inferring expressive safety properties of higher-order functional programs using first-order decision procedures. Our approach encodes higher-order features into first-order logic formula whose solution can be derived using a lightweight counterexample guided refinement loop. To do so, we extract initial verification conditions from dependent typing rules derived by a syntactic scan of the program. Subsequent type-checking and type-refinement phases infer and propagate specifications of higher order functions, which are treated as uninterpreted first-order constructs, via subtyping chains. Popeye provides several benefits not found in existing systems: (1) it enables compositional verification and inference of useful safety properties for functional programs; (2) additionally provides counterexamples that serve as witnesses of unsound assertions: (3) does not entail a complex translation or encoding of the original source program into a first-order represe
文 件 列 表
build
._.DS_Store
.DS_Store
bin
lib
testcase
a-cppr.sml
a-init.sml
a-prod.sml
apply.sml
fhnhn.sml
hors.sml
hrec.sml
intro1.sml
intro2.sml
intro3.sml
mc91-with-error.sml
mult-with-error.sml
mult.sml
r-file.sml
r-lock-error.sml
r-lock.sml
repeat-with-error.sml
repeat.sml
simple.sml
sum-with-error.sml
sum.sml
test-array-with-error.sml
test-array.sml
test-constraint-propagation.sml
test-contextsensitivity.sml
test-from-suresh.sml
test-function-as-value.sml
test-imperative-program.sml
test-max.sml
test-partial-application.sml
testzip.sml
