Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Modular product programs
Eilers M., Müller P., Hitz S. ACM Transactions on Programming Languages and Systems42 (1):1-37,2019.Type:Article
Date Reviewed: Jan 14 2020

Some properties of programs are not about a single run of the program; instead, they relate multiple runs. For example, a program is deterministic if, given the same input, two runs will always produce the same answer. Many other properties of interest, such as security properties, are also like this. These are known as k-hyperproperties, which relate the runs of k programs.

The authors claim that current approaches to the problem are not modular, which would clearly make them difficult to scale. They instead introduce a translation-based method for verifying such properties that blows up the data dependencies (linearly in k), but does not change the control flow. Quite a bit of care is needed to design a translation that deals with each control structure appropriately.

The problem and ideas involved are well motivated through well-chosen examples (sections 2 and 3). Because of this setup, the more technical details of the construction (section 4) make sense. Section 5 is a human proof of soundness and completeness (it’s a bit surprising to see a non-mechanized proof in TOPLAS). Section 6 gives applications to various information flow and security properties, showing the wide applicability of the method, while section 7 gives a rather thorough evaluation of the corresponding implementation in Viper.

The paper is very well written and quite readable. Anyone wanting a snapshot of an interesting method for proving hyperproperties, or even learning about hyperproperties, could benefit from reading this paper.

Reviewer:  Jacques Carette Review #: CR146838 (2005-0110)
Bookmark and Share
  Featured Reviewer  
 
Formal Methods (D.2.4 ... )
 
 
Validation (D.2.4 ... )
 
 
Verification (D.4.5 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Methods": Date
On a method of multiprogramming
Feijen W., van Gasteren A., Springer-Verlag New York, Inc., New York, NY, 1999. Type: Book (9780387988702)
May 1 2000
Computer-Aided reasoning: ACL2 case studies
Kaufmann M. (ed), Manolios P. (ed), Moore J. Kluwer Academic Publishers, Norwell, MA,2000. Type: Divisible Book
Jul 2 2002
Architecting families of software systems with process algebras
Bernardo M., Ciancarini P., Donatiello L. ACM Transactions on Software Engineering and Methodology 11(4): 386-426, 2002. Type: Article
Mar 10 2003
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy