Browse All Reviews
Software Engineering (D.2)
Software/Program Verification (D.2.4)
> Correctness Proofs (D.2.4...)
All Media Types
1-10 of 100 Reviews about "
Correctness Proofs (D.2.4...)
A generalized digraph model for expressing dependencies
Fradet P., Guo X., Monin J., Quinton S. RTNS 2018 (Proceedings of the 26th International Conference on Real-Time Networks and Systems, Chasseneuil-du-Poitou, France, Oct 10-12, 2018) 72-82, 2018. Type: Proceedings
The authors characterize this paper as a work in progress in computer assisted verification (CAV) of task-scheduling models. Directed graph (digraph) models are expressive; however, as the authors point out, they are limited with respect to “...
Feb 7 2019
Computer arithmetic and formal proofs: verifying floating-point algorithms with the Coq system
Boldo S., Melquiond G., ISTE Press - Elsevier, London, UK, 2017. 326 pp. Type: Book (978-1-785481-12-3)
The audience for this superlatively researched and crafted book includes postgraduate students and practitioners of floating-point (FP) computation or formal verification. The authors “sincerely hope that, after reading this book, you will f...
Aug 8 2018
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
, 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
an 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
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2022 ThinkLoud, Inc.