Sciweavers

VMCAI
2010
Springer
14 years 6 months ago
Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction
Yungbum Jung, Soonho Kong, Bow-Yaw Wang, Kwangkeun...
VMCAI
2010
Springer
14 years 6 months ago
An Analysis of Permutations in Arrays
This paper is concerned with the synthesis of invariants in programs with arrays. More specifically, we consider properties concerning array contents up to a permutation. For inst...
Valentin Perrelle, Nicolas Halbwachs
TLDI
2009
ACM
122views Formal Methods» more  TLDI 2009»
14 years 8 months ago
Towards type-theoretic semantics for transactional concurrency
We propose a dependent type theory that integrates programming, specifications, and reasoning about higher-order concurrent programs with shared transactional memory. The design ...
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
TLDI
2009
ACM
111views Formal Methods» more  TLDI 2009»
14 years 8 months ago
A generic type-and-effect system
Type-and-effect systems are a natural approach for statically reasoning about a program’s execution. They have been used to track a variety of computational effects, for example...
Daniel Marino, Todd D. Millstein
TLDI
2009
ACM
108views Formal Methods» more  TLDI 2009»
14 years 8 months ago
Secure compilation of a multi-tier web language
Storing state in the client tier (in forms or cookies, for example) improves the efficiency of a web application, but it also renders the secrecy and integrity of stored data vul...
Ioannis G. Baltopoulos, Andrew D. Gordon
TLDI
2009
ACM
169views Formal Methods» more  TLDI 2009»
14 years 8 months ago
Relational parametricity for references and recursive types
We present a possible world semantics for a call-by-value higherorder programming language with impredicative polymorphism, general references, and recursive types. The model is o...
Lars Birkedal, Kristian Støvring, Jacob Tha...
TLDI
2009
ACM
140views Formal Methods» more  TLDI 2009»
14 years 8 months ago
Design patterns in separation logic
Object-oriented programs are notable for making use of both rder abstractions and mutable, aliased state. Either feature alone is challenging for formal verification, and the com...
Neelakantan R. Krishnaswami, Jonathan Aldrich, Lar...
TLDI
2009
ACM
142views Formal Methods» more  TLDI 2009»
14 years 8 months ago
Static extraction of sound hierarchical runtime object graphs
For many object-oriented systems, it is often useful to have a runtime architecture that shows networks of communicating objects. But it is hard to statically extract runtime obje...
Marwan Abi-Antoun, Jonathan Aldrich
TLDI
2009
ACM
155views Formal Methods» more  TLDI 2009»
14 years 8 months ago
Opis: reliable distributed systems in OCaml
The importance of distributed systems is growing as computing devices become ubiquitous and bandwidth becomes plentiful. Concurrency and distribution pose algorithmic and implemen...
Pierre-Évariste Dagand, Dejan Kostic, Vikto...
TLDI
2009
ACM
100views Formal Methods» more  TLDI 2009»
14 years 8 months ago
Typed transformations of typed abstract syntax
Syntax Arthur Baars Doaitse Swierstra Technical Report UU-CS-2008-021 July 2008 Department of Information and Computing Sciences Utrecht University, Utrecht, The Netherlands www.cs...
Arthur I. Baars, S. Doaitse Swierstra, Marcos Vier...