Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Browse by topic Browse by titles Authors Reviewers Browse by issue Browse Help
ACM Press
  1-10 of 92 reviews Date Reviewed 
  Proof search for propositional abstract separation logics via labelled sequents
Hóu Z., Clouston R., Goré R., Tiu A.  ACM SIGPLAN Notices 49(1): 465-476, 2014. Type: Article

Pointers and sharing have always been difficult problems in program verification, and several extensions to Hoare logic have been proposed and investigated over the decades....

May 12 2014
  Formal verification of object layout for C++ multiple inheritance
Ramananandro T., Dos Reis G., Leroy X.  ACM SIGPLAN Notices 46(1): 67-80, 2011. Type: Article

Efficient language translation, optimized code generation, and runtime memory layout are cornerstones of modern computer language compilers. Squeezing a user’s data structures, especially with C++ multiple inheritance, into fewer but efficie...

Dec 13 2011
  Specifying and verifying sparse matrix codes
Arnold G., Hölzl J., Köksal A., Bodík R., Sagiv M.  ACM SIGPLAN Notices 45(9): 249-260, 2010. Type: Article

It is increasingly recognized that the heroics involved in coding efficient, low-level, imperative programs for various tasks are not sustainable. While the gain in efficiency might be quite real, the loss of certainty (with respect to correctness...

Nov 7 2011
  A typed store-passing translation for general references
Pottier F.  ACM SIGPLAN Notices 46(1): 147-158, 2011. Type: Article

It is a challenging task to create a well-typed semantic model for a programming language that supports references to dynamically allocated memory cells that may hold values of any type, such as functions or addresses of other cells. The essence o...

Nov 1 2011
  Total parser combinators
Danielsson N.  ACM SIGPLAN Notices 45(9): 285-296, 2010. Type: Article

Parser combinators are one of the best-known examples of the advantages of functional programming, as they make essential use of functions as arguments and results of functions. They are also one of the longest standing examples, going back to Bur...

Oct 13 2011
  A parametric segmentation functor for fully automatic and scalable array content analysis
Cousot P., Cousot R., Logozzo F.  ACM SIGPLAN Notices 46(1): 105-118, 2011. Type: Article

Precise and scalable static analysis of realistic software is challenging due to several complex features used in software. One of these features, which has been the focus of attention in recent times, is an array. In spite of several proposals fo...

Jun 1 2011
  Regular, shape-polymorphic, parallel arrays in Haskell
Keller G., Chakravarty M., Leshchinskiy R., Peyton Jones S., Lippmeier B.  ACM SIGPLAN Notices 45(9): 261-272, 2010. Type: Article

Algorithms that work on arrays are very common in science and engineering, and range from finding connected components in a graph to complex atmospheric simulations. Supporters of purely functional languages claim that these algorithms are often e...

May 18 2011
  Program verification through characteristic formulae
Charguéraud A.  ACM SIGPLAN Notices 45(9): 321-332, 2010. Type: Article

Charguéraud presents a tool for the verification of purely functional programs consisting of two parts. The first part is used to generate characteristic formulas, and the second part is used to formulate a set of lemmas, notations, and tacti...

Apr 18 2011
  Dynamic multirole session types
Deniélou P., Yoshida N.  ACM SIGPLAN Notices 46(1): 435-446, 2011. Type: Article

Session types have been introduced to provide global static descriptions of multi-process systems by specifying abstractions of the interaction patterns among a fixed set of participants. Deniélou and Yoshida’s paper extends this approa...

Apr 7 2011
  Mathematizing C++ concurrency
Batty M., Owens S., Sarkar S., Sewell P., Weber T.  ACM SIGPLAN Notices 46(1): 55-66, 2011. Type: Article

Integrating multi-threading into a programming language such as C++ is an error-prone task: the intuitive expectation of a “sequentially consistent” program that behaves as if concurrent memory reads and writes were put into some linea...

Apr 5 2011
Display per column
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2017 ThinkLoud, Inc.
Terms of Use
| Privacy Policy