APLAS
2010
ACM
14 years 9 months ago
2010
ACM
We describe an approach to using one logic to reason about specifications written in a second logic. One level of logic, called the "reasoning logic", is used to state th...
78
Voted
APLAS
2010
ACM
14 years 9 months ago
2010
ACM
Abstract. We propose a new method to verify that a higher-order, treeprocessing functional program conforms to an input/output specification. Our method reduces the verification pr...
49
Voted
APLAS
2010
ACM
14 years 9 months ago
2010
ACM
APLAS
2010
ACM
14 years 9 months ago
2010
ACM
Abstract. The type system of Objective Caml has many unique features, which make ensuring the correctness of its implementation difficult. One of these features is structurally pol...
64
Voted
APLAS
2010
ACM
14 years 9 months ago
2010
ACM
APLAS
2010
ACM
14 years 9 months ago
2010
ACM
Abstract. By combining algorithmic learning, decision procedures, predicate abstraction, and simple templates, we present an automated technique for finding quantified loop invaria...
APLAS
2010
ACM
14 years 9 months ago
2010
ACM
Abstract. Through foreign function interfaces (FFIs), software components in different programming languages interact with each other in the same address space. Recent years have w...
APLAS
2010
ACM
14 years 9 months ago
2010
ACM
Semantic preorders between processes are usually applied in practice to model approximation or implementation relationships. For interactive models these preorders depend crucially...
70
Voted
APLAS
2010
ACM
14 years 9 months ago
2010
ACM
This paper studies the problem of statically determining upper bounds on the resource consumption of first-order functional programs. A previous work approached the problem with an...