Sciweavers

TLDI
2010
ACM
190views Formal Methods» more  TLDI 2010»
14 years 8 months ago
Distributed programming with distributed authorization
We propose a programming language, called PCML5, for building distributed applications with distributed access control. Target applications include web-based systems in which prog...
Kumar Avijit, Anupam Datta, Robert Harper
TLDI
2010
ACM
247views Formal Methods» more  TLDI 2010»
14 years 8 months ago
F-ing modules
ML modules are a powerful language mechanism for decomposing programs into reusable components. Unfortunately, they also have a reputation for being “complex” and requiring fa...
Andreas Rossberg, Claudio V. Russo, Derek Dreyer
TLDI
2010
ACM
225views Formal Methods» more  TLDI 2010»
14 years 8 months ago
Race-free and memory-safe multithreading: design and implementation in cyclone
We present the design of a formal low-level multi-threaded language with advanced region-based memory management and synchronization primitives, where well-typed programs are memo...
Prodromos Gerakios, Nikolaos Papaspyrou, Konstanti...
TLDI
2010
ACM
218views Formal Methods» more  TLDI 2010»
14 years 8 months ago
Pointwise generalized algebraic data types
In the GADT (Generalized Algebraic Data Types) type system, a pattern-matching branch can draw type information from both the scrutinee type and the data constructor type. Even th...
Chuan-kai Lin, Tim Sheard
TLDI
2010
ACM
210views Formal Methods» more  TLDI 2010»
14 years 8 months ago
Effects for cooperable and serializable threads
Reasoning about the correctness of multithreaded programs is complicated by the potential for unexpected interference between threads. Previous work on controlling thread interfer...
Jaeheon Yi, Cormac Flanagan
SOFSEM
2010
Springer
14 years 8 months ago
Practically Applicable Formal Methods
Abstract. Formal methods are considered to be highly expensive. Therefore, they are currently applied almost only in high risk software development. In this paper, we show that for...
Jedrzej Fulara, Krzysztof Jakubczyk

0
posts
with
0
views
270profile views
francieResearch Scientist, PhD
University of Limerick
francie
CAV
2009
Springer
176views Hardware» more  CAV 2009»
15 years 4 days ago
PAT: Towards Flexible Verification under Fairness
Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing ...
Jun Sun 0001, Yang Liu 0003, Jin Song Dong, Jun Pa...
CAV
2009
Springer
215views Hardware» more  CAV 2009»
15 years 4 days ago
Homer: A Higher-Order Observational Equivalence Model checkER
We present HOMER, an observational-equivalence model checker for the 3rd-order fragment of Idealized Algol (IA) augmented with iteration. It works by first translating terms of the...
David Hopkins, C.-H. Luke Ong
CAV
2009
Springer
155views Hardware» more  CAV 2009»
15 years 4 days ago
Better Quality in Synthesis through Quantitative Objectives
Abstract. Most specification languages express only qualitative constraints. However, among two implementations that satisfy a given specification, one may be preferred to another....
Roderick Bloem, Krishnendu Chatterjee, Thomas A. H...