Search for Topics All Reviews
	Browse All Reviews > Software (D) > Software Engineering (D.2) > Software/Program Verification (D.2.4) > Correctness Proofs (D.2.4...)     Options: All Media Types Journals Proceedings Div Books Whole Books Other Date Reviewed Title Author Publisher Published Date Descending Ascending     1-10 of 92 Reviews about "Correctness Proofs (D.2.4...)": Date Reviewed    Term transformers: a new approach to state Morris J., Bunkenburg A., Tyrrell M.  ACM Transactions on Programming Languages and Systems 31(4): 1-42, 2009. Type: Article I hope the ideas in this paper will lead to clearer languages and documentation. All language reference manuals use some kind of Backus-Naur form (BNF) grammar to define syntax. Hardly any provide formal semantics. People have... Aug 20 2009   Functional pearl: streams and unique fixed points Hinze R.  ACM SIGPLAN Notices 43(9): 189-200, 2008. Type: Article Streams, infinite sequences of elements, play an important role in various areas of mathematics and computer science. On the one hand, they represent a fundamental concept of discrete mathematics, where infinite integer sequences are... Jun 11 2009   A calculus of atomic actions Elmas T., Qadeer S., Tasiran S.  POPL 2009 (Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Savannah, GA,  Jan 21-23, 2009) 2-15, 2008. Type: Proceedings Verification of partial correctness of shared-variable parallel programs is a very old subject. Nearly 35 years ago, Owicki and Gries proposed the first axiomatization of partial verification of parallel programs, using Hoare-style logic [1].... Mar 16 2009   Proofs from tests Beckman N., Nori A., Rajamani S., Simmons R.  Software testing and analysis (Proceedings of the 2008 International Symposium on Software Testing and Analysis, Seattle, WA,  Jul 20-24, 2008) 3-14, 2008. Type: Proceedings Based in the area of software verification that uses model-checking methods, this paper builds on the recent verification methods that employ the technique of counterexample guided abstraction refinement (CEGAR) for proving a... Sep 29 2008   Model checking the Java metalocking algorithm Basu S., Smolka S.  ACM Transactions on Software Engineering and Methodology 16(3): 12-es, 2007. Type: Article Basu and Smolka present a case study of modeling and verifying the Java metalocking algorithm using the XMC model checker. They verify the correctness of the metalocking algorithm by manually constructing a model of the algorithm, and then... Jan 10 2008    Semantic errors in SQL queries: a quite complete list Brass S., Goldberg C.  Journal of Systems and Software 79(5): 630-644, 2006. Type: Article This paper is interesting and relevant. The understanding of semantic errors in structured query language (SQL) is inadequate among database practitioners and educators. This paper will help to rectify this. The authors propose a pre-query syntax ... Mar 15 2007   Correctness verification and performance analysis of real-time systems using stochastic preemptive time Petri nets Bucci G., Sassoli L., Vicario E.  IEEE Transactions on Software Engineering 31(11): 913-927, 2005. Type: Article This paper proposes a novel Petri net formalism, called stochastic preemptive time Petri nets (spTPN), for modeling and analyzing concurrent real-time systems. Stochastic preemptive time Petri nets capture resource contention, nondeterministic... Jun 23 2006   Echo: a practical approach to formal verification Strunk E., Yin X., Knight J.  Formal methods for industrial critical systems (Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, Lisbon, Portugal,  Sep 5-6, 2005) 44-53, 2005. Type: Proceedings “Practical” should be a word most welcome to formal methodists (out of whose way most software practitioners scurry so as not to get involved in “impractical, highfalutin math”). This paper’s authors show a way... Jan 6 2006   Constructing correct software (Formal Approaches to Computing and Information Technology) Cooke J.,  SpringerVerlag, 2004.Type: Book The issues surrounding the construction of correct software are discussed in this book. It provides the reader with introductory material, and concepts and techniques for formal methods in the area of software specification.... Apr 11 2005   On interactive proofs with a laconic prover Goldreich O., Vadhan S., Wigderson A.  Computational Complexity 11(1/2): 1-53, 2003. Type: Article As the authors state, “Interactive proof systems are two-party randomized protocols through which a computationally unbounded prover can convince a probabilistic polynomial-time verifier of the membership of a common input in a... Dec 21 2004       Display 510152550100 per page
	Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2010 Reviews.com Terms of Use | Privacy Policy