Abstract. We instantiate an Isabelle/HOL framework for proof carrying code to Jinja bytecode, a downsized variant of Java bytecode featuring objects, inheritance, method calls and ...
JavaScript is a popular language for client-side web scripting. It has a dubious reputation among programmers for two reasons. First, many JavaScript programs are written against a...
We present a statically typed, class-based object oriented language where classes are first class polymorphic values. A main contribution of this work is the design of a type syst...
Abadi-Leino Logic is a Hoare-calculus style logic for a simple imperative and object-based language where every object comes with its own method suite. Consequently, methods need t...
The notion of control dependence underlies many program analysis and transformation techniques used in numerous applications. Despite wide application, existing definitions and ap...
ite-state abstraction scheme such as predicate abstraction. The type system, which is also parametric, type checks exactly those programs that are accepted by the model checker. It...
Are computing systems trustworthy? To answer this, we need to know three things: what the systems are supposed to do, what they are not supposed to do, and what they actually do. A...
We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, cal...
: Fully abstract trace semantics for a core Java language. Alan Jeffrey 1,2 and Julian Rathke3 1 Bell Labs, Lucent Technologies, Chicago, IL, USA 2 DePaul University, Chicago, IL, ...