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