This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
This paper defines the cover of a formula with respect to a set of variables V in theory T to be the strongest quantifier-free formula that is implied by V : in theory T. Cover e...
Abstract. Higher-order abstract syntax (HOAS) refers to the technique of representing variables of an object-language using variables of a meta-language. The standard first-order a...
Abstract. In this article, we present a model and a denotational semantics for hybrid systems. Our model is designed to be used for the verification of large, existing embedded app...
A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, cal...
In this work we address the problem of proving, by static analysis means, that allocating and deallocating regions in the store provides a safe way to achieve memory management. Th...
Abstract. There are many settings in which sensitive information is made available to a system or organisation for a specific purpose, on the understanding that it will be erased o...
Abstract. We survey recent developments in an approach to the verification of higher-order computation based on game semantics. Higherorder recursion schemes are in essence (progra...