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 > Computing Methodologies (I) > Artificial Intelligence (I.2) > Automatic Programming (I.2.2) > Program Verification (I.2.2...)  
  1-10 of 36 Reviews about "Program Verification (I.2.2...)": Date Reviewed
  Quantum relational Hoare logic
Unruh D.  Proceedings of the ACM on Programming Languages 3(POPL): 1-31, 2019. Type: Article

All programs need to be verified--even post-quantum cryptography software. To prove properties of such protocols requires proofs that involve not only quantum programming, but also pairs of programs, an encryptor and an attacker. But proof al...

Jan 22 2021
  Performance-aware server architecture recommendation and automatic performance verification technology on IaaS cloud
Yamato Y.  Service Oriented Computing and Applications 11(2): 121-135, 2017. Type: Article

Yamato proposes “a server architecture recommendation and automatic performance verification technology, which recommends and verifies appropriate server architecture on an infrastructure as a service (IaaS) cloud with bare metal servers, co...

Dec 15 2017
  Proof checking and logic programming
Miller D.  Formal Aspects of Computing 29(3): 383-399, 2017. Type: Article

A proof checker is a program that takes a claimed proof of a logic formula and decides whether this claim is true; in applications such as program verification and automated reasoning, it is thus not necessary to trust the (potentially big) prover...

Jun 27 2017
  A devil’s advocate against termination of direct recursion
Frühwirth T.  PPDP 2015 (Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy,  Jul 14-16, 2015) 103-113, 2015. Type: Proceedings

A totally correct system terminates. Instead of establishing termination directly, this paper describes a technique based on non-termination. This technique is statically derivable from the program text and produces non-termination results that ar...

Aug 12 2015
  Matrix code
Van Emden M.  Science of Computer Programming 843-21, 2014. Type: Article

Imperative programming verification is a serious problem! Parallel development of proof and code for imperative programming is the proposed solution. A new language is presented to create a proof in parallel with the code called matrix code, which...

Aug 27 2014
  An integrated specification and verification technique for highly concurrent data structures
Abdulla P., Haziza F., Holík L., Jonsson B., Rezine A.  TACAS 2013 (Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy,  Mar 16-24, 2013) 324-338, 2013. Type: Proceedings

In this paper, the authors study the verification of concurrent programs, such as lock-free implementations of stacks and queues in a runtime environment where garbage collection is absent....

Jan 9 2014
  Mechanical reasoning about families of UTP theories
Zeyda F., Cavalcanti A.  Science of Computer Programming 77(4): 444-479, 2012. Type: Article

The final goal of formal methods in computer science is to prove that a program behaves as it should. The work of Zeyda and Cavalcanti, as reported in this paper, is another step toward this ultimate goal. The authors show that a current state-of-...

May 31 2012
  Flow logic for process calculi
Nielson H., Nielson F., Pilegaard H.  ACM Computing Surveys 44(1): 1-39, 2012. Type: Article

Nielson et al. present an approach using flow logic to represent programming notations in process calculi. Flow logic is usually used in static analysis for language paradigms, including imperative, functional, and concurrent features. The lambda ...

May 30 2012
  Optimize quality for business outcomes: a practical approach to software testing (3rd ed.)
Golze A., Sarbiewski M., Zahm A.,  Wiley Publishing, Indianapolis, IN, 2008. 304 pp. Type: Book (9780470404669)

Although this book is easy to read, it misleads the reader with incomplete, inaccurate, and confusing content. Even though its publication date is recent, the book does not reflect the breadth of current best practices for testing, in a full testi...

Jul 15 2009
  Model driven code checking
Holzmann G., Joshi R., Groce A.  Automated Software Engineering 15(3-4): 283-297, 2008. Type: Article

An erstwhile corollary of “thinking in C” was that we felt the specification and the program to be one and the same. Decades of collective suffering led us to realize the value of abstracting high-level models of the design and applyin...

Mar 5 2009
Display per page
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2021 ThinkLoud, Inc.
Terms of Use
| Privacy Policy