Sciweavers

Share
VMCAI
2012
Springer
8 years 1 months ago
Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
We describe a course on the semantics of a simple imperative programming language and on applications to compilers, type systems, static analyses and Hoare logic. The course is ent...
Tobias Nipkow
PLPV
2011
ACM
8 years 8 months ago
Local actions for a curry-style operational semantics
Soundness proofs of program logics such as Hoare logics and type systems are often made easier by decorating the operational semantics with information that is useful in the proof...
Gordon Stewart, Andrew W. Appel
CORR
2010
Springer
111views Education» more  CORR 2010»
9 years 5 months ago
Reducing the Number of Annotations in a Verification-oriented Imperative Language
Abstract. Automated software verification is a very active field of research which has made enormous progress both in theoretical and practical aspects. Recently, an important amou...
Guido de Caso, Diego Garbervetsky, Daniel Gor&iacu...
POPL
1998
ACM
9 years 10 months ago
Secure Information Flow in a Multi-Threaded Imperative Language
Previously, we developed a type system to ensure secure information flow in a sequential, imperative programming language [VSI96]. Program variables are classified as either hig...
Geoffrey Smith, Dennis M. Volpano
PPPJ
2003
ACM
9 years 11 months ago
JVM versus CLR: a comparative study
We present empirical evidence to demonstrate that there is little or no difference between the Java Virtual Machine and the .NET Common Language Runtime, as regards the compilati...
Jeremy Singer
CSFW
2006
IEEE
9 years 11 months ago
Information-Flow Security for Interactive Programs
Abstract. Interactive programs allow users to engage in input and output throughout execution. The ubiquity of such programs motivates the development of models for reasoning about...
Kevin R. O'Neill, Michael R. Clarkson, Stephen Cho...
ICTAC
2009
Springer
10 years 7 days ago
A Deadlock-Free Semantics for Shared Memory Concurrency
Abstract. We design a deadlock-free semantics for a concurrent, functional and imperative programming language where locks are implicitly and univocally associated with pointers. T...
Gérard Boudol
books