Explicit information flow properties in JML (2009)
Christian Haack, Erik Poll, Aleksy Schubert
Abstract This paper considers how explicit information flow properties can be expressed and verified in a traditional program logic, using pre- and postconditions. As concrete specification language...
ESC/Java2 as a Tool to Ensure Security in the Source Code of Java Applications ⋆ (2008)
Aleksy Schubert, Jacek Chrząszcz
Abstract. The paper shows how extended static checking tools like ESC/Java2 can be used to ensure source code security properties of Java applications. It is demonstrated in a case study on a simple...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, Julien Charles, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, David Cok, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
Verifying an implementation of SSH (2007)
Abstract. We present a case study in the formal verification of an open source Java implementation of SSH. We discuss the security flaws we found and fixed by means of formal specification and...
Algebraic Higher-Order Matching (2002)
The decidability of algebraic higher-order matching is proved. Algebraic higher-order matching is a matching where the constant term in equation is built of first-order constants and constants of a...
A Note on Observational Equivalence in the Simply Typed lambda-calculus (2002)
A theory of observational equivalence for simply typed -calculus is developed. This allows to establish a reduction of the higher-order matching problem to the dual interpolation problem.
Second-order unification and type inference for Church-style polymorphism (1998)
We present a proof of the undecidability of type inference for the Church-style system F --- an abstraction of polymorphism. A natural reduction from the second-order unification problem to type...
Linear Interpolation for the Higher Order Matching Problem (1996)
We present here a particular case of the higher order matching problem --- the linear interpolation problem. The problem consists in solving a collection of higher order matching equations of the...