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 > Software (D) > Software Engineering (D.2) > Software/Program Verification (D.2.4) > Correctness Proofs (D.2.4...)  
  1-10 of 98 Reviews about "Correctness Proofs (D.2.4...)": Date Reviewed
  A language-independent proof system for full program equivalence
Ciobâcă S., Lucanu D., Rusu V., Roşu G.  Formal Aspects of Computing 28(3): 469-497, 2016. Type: Article

The authors consider proving two programs “fully equivalent” (that is, either both do not terminate or both terminate with the same value). Both compute the Collatz sequence starting with a natural number n, which re...

Jun 21 2016
  Introducing formal methods via program derivation
Chaudhari D., Damani O.  ITiCSE 2015 (Proceedings of the 2015 ACM Conference on Innovation and Technology in Computer Science Education, Vilnius, Lithuania,  Jul 4-8, 2015) 266-271, 2015. Type: Proceedings

The paper addresses teaching programming as a sequence of derivations from one partial solution to another, maintaining correctness of the partial programs at each step. This is contrasted with developing a program first, and then proving the comp...

Sep 17 2015
  A framework for testing first-order logic axioms in program verification
Ahn K., Denney E.  Software Quality Journal 21(1): 159-200, 2013. Type: Article

As model-driven code generators have increased in capability and in performance, so too has their use in mission-critical software development. One benefit of auto-generated code over handcrafted, individually created source code is that it is sim...

Jun 4 2014
  Proof-directed parallelization synthesis by separation logic
Botinan M., Dodds M., Jagannathan S.  ACM Transactions on Programming Languages and Systems 35(2): 1-60, 2013. Type: Article

The parallelization of sequential programs is a tedious and error-prone task; the incorrect use of synchronization primitives may yield a program that produces different results than the original code, or even different results in different runs. ...

Sep 27 2013
  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
  The essence of compiling with traces
Guo S., Palsberg J.  ACM SIGPLAN Notices 46(1): 563-574, 2011. Type: Article

A widely quoted rule of thumb says that a program spends 90 percent of its time in ten percent of its code. Can we record sequences of instructions (traces) that the program executes very frequently, optimize them in isolation, and make the progra...

Feb 24 2011
   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 prop...

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 investigated,...

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]. This...

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 progr...

Sep 29 2008
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