ESOP
2010
Springer
14 years 8 months ago
2010
Springer
Proving software free of security bugs is hard. Languages that ensure that programs correctly enforce their security policies would help, but, to date, no security-typed language h...
ESOP
2010
Springer
14 years 8 months ago
2010
Springer
Abstract. We present a framework that automatically produces suggestions to resolve type errors in security-typed programs, enabling legacy code to be retrofit with comprehensive s...
ESOP
2010
Springer
14 years 8 months ago
2010
Springer
Detailed memory models that expose individual fields are necessary to precisely analyze code that makes use of low-level aspects such as, pointers to fields and untagged unions. Ye...
ESOP
2010
Springer
14 years 8 months ago
2010
Springer
Type-based amortised resource analysis following Hofmann and Jost--where resources are associated with individual elements of data structures and doled out to the programmer under ...
ESOP
2010
Springer
14 years 8 months ago
2010
Springer
ESOP
2010
Springer
14 years 8 months ago
2010
Springer
Affine type systems manage resources by preventing some values from being used more than once. This offers expressiveness and performance benefits, but difficulty arises in intera...
ESOP
2010
Springer
14 years 8 months ago
2010
Springer
The specification of the Java Memory Model (JMM) is phrased in terms of acceptors of execution sequences rather than the standard generative view of operational semantics. This cre...
ESOP
2010
Springer
14 years 8 months ago
2010
Springer
Formal reasoning about concurrent programs is usually done with the assumption that the underlying memory model is sequentially consistent, i.e. the execution outcome is equivalen...
ESOP
2010
Springer
14 years 8 months ago
2010
Springer
In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a trace-based big-step semantics for W...
ESOP
2010
Springer
14 years 8 months ago
2010
Springer