ATVA
2015
Springer
8 years 3 months ago
2015
Springer
Abstract. Using game semantics, we investigate the problem of verifying contextual equivalences in Interface Middleweight Java (IMJ), an imperative object calculus in which program...
ATVA
2015
Springer
8 years 3 months ago
2015
Springer
Abstract Infinite games with imperfect information tend to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is ...
POPL
2015
ACM
8 years 3 months ago
2015
ACM
This paper reports on the development of Compositional CompCert, the first verified separate compiler for C. Specifying and proving separate compilation for C is made challengin...
POPL
2015
ACM
8 years 3 months ago
2015
ACM
ion Layers Ronghui Gu Jérémie Koenig Tahina Ramananandro Zhong Shao Newman Wu Shu-Chun Weng Haozhong Zhang1 Yu Guo1 Yale University 1University of Science and Technology of China...
POPL
2015
ACM
8 years 3 months ago
2015
ACM
Security enforcement mechanisms like execution monitors are used to make sure that some untrusted program complies with a policy. Different enforcement mechanisms have different s...
POPL
2015
ACM
8 years 3 months ago
2015
ACM
Hygiene is an essential aspect of Scheme’s macro system that prevents unintended variable capture. However, previous work on hygiene has focused on algorithmic implementation ra...
POPL
2015
ACM
8 years 3 months ago
2015
ACM
The past decades have witnessed an extensive study of structured recursion schemes. A general scheme is the hylomorphism, which captures the essence of divide-and-conquer: a probl...
POPL
2015
ACM
8 years 3 months ago
2015
ACM
We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transi...
POPL
2015
ACM
8 years 3 months ago
2015
ACM
Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are ...
POPL
2015
ACM
8 years 3 months ago
2015
ACM
We propose the first sound and complete learning-based compositional verification technique for probabilistic safety properties on concurrent systems where each component is an ...