
Browse All Reviews > Software (D) > Software Engineering (D.2) > Software/Program Verification (D.2.4) > Correctness Proofs (D.2.4...)









110 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 RealTime Networks and Systems, ChasseneuilduPoitou, France, Oct 1012, 2018) 7282, 2018. Type: Proceedings
The authors characterize this paper as a work in progress in computer assisted verification (CAV) of taskscheduling models. Directed graph (digraph) models are expressive; however, as the authors point out, they are limited with respe...

Feb 7 2019 

A languageindependent proof system for full program equivalence Ciobâcă S., Lucanu D., Rusu V., Roşu G. Formal Aspects of Computing 28(3): 469497, 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 firstorder logic axioms in program verification Ahn K., Denney E. Software Quality Journal 21(1): 159200, 2013. Type: Article
As modeldriven code generators have increased in capability and in performance, so too has their use in missioncritical software development. One benefit of autogenerated code over handcrafted, individually created source code is th...

Jun 4 2014 

Proofdirected parallelization synthesis by separation logic Botinčan M., Dodds M., Jagannathan S. ACM Transactions on Programming Languages and Systems 35(2): 160, 2013. Type: Article
The parallelization of sequential programs is a tedious and errorprone 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): 563574, 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): 189200, 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): 12es, 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 realtime systems using stochastic preemptive time Petri nets Bucci G., Sassoli L., Vicario E. IEEE Transactions on Software Engineering 31(11): 913927, 2005. Type: Article
This paper proposes a novel Petri net formalism, called stochastic preemptive time Petri nets (spTPN), for modeling and analyzing concurrent realtime 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 56, 2005) 4453, 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): 7986, 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 





