Sciweavers

POST
2012
153views more  POST 2012»
14 years 8 days ago
Towards Incrementalization of Holistic Hyperproperties
A hyperproperty is a set of sets of finite or infinite traces over some fixed alphabet and can be seen as a very generic system specification. In this work, we define the noti...
Dimiter Milushev, Dave Clarke
POST
2012
162views more  POST 2012»
14 years 8 days ago
Revisiting Botnet Models and Their Implications for Takedown Strategies
Abstract. Several works have utilized network models to study peerto-peer botnets, particularly in evaluating the effectiveness of strategies aimed at taking down a botnet. We obs...
Ting-Fang Yen, Michael K. Reiter
POST
2012
181views more  POST 2012»
14 years 8 days ago
Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication
Abstract. We formally analyze the family of entity authentication protocols defined by the ISO/IEC 9798 standard and find numerous weaknesses, both old and new, including some th...
David A. Basin, Cas J. F. Cremers, Simon Meier
POST
2012
218views more  POST 2012»
14 years 8 days ago
A Core Calculus for Provenance
Provenance is an increasing concern due to the revolution in sharing and processing scientific data on the Web and in other computer systems. It is proposed that many computer sys...
Umut A. Acar, Amal Ahmed, James Cheney, Roly Perer...
POPL
2012
ACM
14 years 8 days ago
Static and user-extensible proof checking
Despite recent successes, large-scale proof development within proof assistants remains an arcane art that is extremely timeconsuming. We argue that this can be attributed to two ...
Antonis Stampoulis, Zhong Shao
156
Voted
POPL
2012
ACM
14 years 8 days ago
Towards a program logic for JavaScript
JavaScript has become the most widely used language for clientside web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading t...
Philippa Gardner, Sergio Maffeis, Gareth David Smi...
POPL
2012
ACM
14 years 8 days ago
The ins and outs of gradual type inference
Gradual typing lets programmers evolve their dynamically typed programs by gradually adding explicit type annotations, which confer benefits like improved performance and fewer r...
Aseem Rastogi, Avik Chaudhuri, Basil Hosmer
POPL
2012
ACM
14 years 8 days ago
The marriage of bisimulations and Kripke logical relations
There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages—that is, languages that combine fea...
Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Va...
POPL
2012
ACM
14 years 8 days ago
Playing in the grey area of proofs
Interpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invar...
Krystof Hoder, Laura Kovács, Andrei Voronko...
POPL
2012
ACM
14 years 8 days ago
Higher-order functional reactive programming in bounded space
Functional reactive programming (FRP) is an elegant and successful approach to programming reactive systems declaratively. The high levels of abstraction and expressivity that mak...
Neelakantan R. Krishnaswami, Nick Benton, Jan Hoff...