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 32 Reviews about "Correctness Proofs (D.2.4...)": Date Reviewed
  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 respe...

Feb 7 2019
  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...

Jun 21 2016
  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 th...

Jun 4 2014
  Proof-directed parallelization synthesis by separation logic
Botinč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 diff...

Sep 27 2013
  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 mak...

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

Jun 11 2009
  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 ...

Jan 10 2008
  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, nondeter...

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&#...

Jan 6 2006
  Software is discrete mathematics
Page R. ACM SIGPLAN Notices 38(9): 79-86, 2003.  Type: Article

How to best train software engineering students in discrete mathematics is a source of continual debate. This paper advocates teaching mathematics through examples based on reasoning about software, rather than via more traditional &am...

Mar 30 2004
Display per page
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2023 ThinkLoud®
Terms of Use
| Privacy Policy