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
  Browse All Reviews > Theory Of Computation (F) > Logics And Meanings Of Programs (F.3) > Specifying And Verifying And Reasoning About Programs (F.3.1) > Invariants (F.3.1...)  
  1-10 of 13 Reviews about "Invariants (F.3.1...)": Date Reviewed
  Algorithms and programming: problems and solutions
Shen A.,  Springer Publishing Company, Incorporated, New York, NY, 2009. 272 pp. Type: Book (978-1-441917-47-8)

Anyone who has done any serious programming knows that programming is fun but not easy. The fun part comes from understanding a problem, developing a conceptual solution, writing a program, and seeing the program work. The hard part is making sure...

Dec 3 2010
  Improving abstract interpretations by combining domains
Codish M., Mulkers A., Bruynooghe M., de la Banda M., Hermenegildo M.  ACM Transactions on Programming Languages and Systems 17(1): 28-44, 1995. Type: Article

In the abstract setting of domain theory, the meaning of a program P is expressed as the least fixed point of a monotonic operator f P on a domain E. In the development of the pro...

Sep 1 1996
  On the mechanical derivation of loop invariants
Chadha R., Plaisted D.  Journal of Symbolic Computation 15(5-6): 705-744, 1993. Type: Article

A method for automatically deriving loop invariants for loops in a flowchart program for the purpose of proving the partial correctness of the program is described. In fact, the authors present a method for deriving logical consequences of first-o...

Mar 1 1995
  Invariant-based verification of a distributed deadlock detection algorithm
Kshemkalyani A., Singhal M. (ed)  IEEE Transactions on Software Engineering 17(9): 789-799, 1991. Type: Article

Proving the correctness of distributed deadlock detection algorithms (DDDAs) is difficult. Most previous works on DDDAs have either not provided a proof of correctness, provided only informal or intuitive arguments for correctness, or used simulat...

May 1 1993
  Reasoning about programs (videotape)
Dijkstra E. (ed),  University Video Communications, Stanford, CA, 1990.Type: Book

In this videotape, Dijkstra gives a tutorial on program verification. He uses two toy examples, in which he develops the program and its proof at the same time. The material covers basic concepts of assertions, invariants, pre-conditions, post-con...

Dec 1 1992
  On the design of some systolic algorithms
van de Snepscheut J., Swenker J.  Journal of the ACM 36(4): 826-840, 1989. Type: Article

A systolic algorithm is an algorithm that is executed on a synchronous array of computing cells that only communicate locally. This paper discusses a design technique for such algorithms that is based on established methods used in sequential prog...

Nov 1 1990
  Formal development programs and proofs
Dijkstra E. (ed),  Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990.Type: Book (9780201172379)

“Good programming is the art and science of keeping things simple” (p. viii). The Year of Programming (1987) at the University of Texas at Austin, which originated from this conviction, resulted in a series of somewhat unusual proceedi...

Sep 1 1990
  Detection of Ada Static Deadlocks Using Petri Net Invariants
Murata T., Shatz S., Shenker B.  IEEE Transactions on Software Engineering 15(3): 314-326, 1989. Type: Article

The authors present a technique which uses Petri nets to detect static deadlocks in concurrent Ada programs (Ada programs which use the tasking features of the language). This method addresses two kinds of static deadlock: what the authors refer t...

Apr 1 1990
  Reachability trees for high-level Petri nets
Huber P., Jensen A., Li ., Jepsen L., Jensen K. (ed)  Theoretical Computer Science 45(3): 261-292, 1986. Type: Article

High-level Petri nets (HL-nets) have been introduced to handle rather complex systems in a succinct and manageable way, although there is still much work to be done in order to establish the necessary analysis methods....

Feb 1 1989
  Sometime=always+recursionalways on the equivalence of the intermittent and invariant assertions methods for proving properties of programs
Cousot P., Cousot R.  Acta Informatica 24(1): 1-31, 1987. Type: Article

This paper compares two verification methods for inevitability properties of nondeterministic transition systems, the “always” method and the “sometime” method. These methods are abstractions of program-verification techniq...

Nov 1 1988
Display per page
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