In object-oriented programming, unique permissions to object references are useful for checking correctness properties such as consistency of typestate and noninterference of conc...
Karl Naden, Robert Bocchino, Jonathan Aldrich, Kev...
We present a formal operational semantics and its Coq mechanization for the C++ object model, featuring object construction and destruction, shared and repeated multiple inheritan...
Tahina Ramananandro, Gabriel Dos Reis, Xavier Lero...
The ideal software contract fully specifies the behavior of an operation. Often, in particular in the context of scripting languages, a full specification may be cumbersome to s...
Phillip Heidegger, Annette Bieniusa, Peter Thieman...
There has been great interest in creating probabilistic programming languages to simplify the coding of statistical tasks; however, there still does not exist a formal language th...
Sooraj Bhat, Ashish Agarwal, Richard W. Vuduc, Ale...
This paper describes an executable formal semantics of C. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes 99....
JavaScript has become a central technology of the web, but it is also the source of many security problems, including cross-site scripting attacks and malicious advertising code. ...
It is becoming increasingly important for applications to protect sensitive data. With current techniques, the programmer bears the burden of ensuring that the application’s beh...
We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, writte...
Formal models serve in many roles in the programming language community. In its primary role, a model communicates the idea of a language design; the architecture of a language to...
Casey Klein, John Clements, Christos Dimoulas, Car...