| |
Browse All Reviews > Theory Of Computation (F) > Logics And Meanings Of Programs (F.3) > Specifying And Verifying And Reasoning About Programs (F.3.1) > Mechanical Verification (F.3.1...)
|
|
 |
|
|
| |
|
|
| |
1-10 of 15
Reviews about "Mechanical Verification (F.3.1...)":
|
Date Reviewed |
| |
A semantics comparison workbench for a concurrent, asynchronous, distributed programming language
Corrodi C., Heu&bgr;ner A., Poskitt C. Formal Aspects of Computing 30(1): 163-192, 2018. Type: Article
Changes in distributed-system runtime support in response to changes in technological and operational circumstances may also change the services offered to supported systems. The graph-based semantics comparison workbench described in ...
|
May 23 2018 |
| |
Fundamental proof methods in computer science: a computer-based approach
Arkoudas K., Musser D., MIT Press, Cambridge, MA, 2017. Type: Book (9780262035538)
An introduction to proof methods in computer science (CS), this book is set apart from other by its reliance on an interactive theorem prover (called Athena) to achieve the task....
|
Sep 21 2017 |
| |
Foundations for using linear temporal logic in Event-B refinement
Hoang T., Schneider S., Treharne H., Williams D. Formal Aspects of Computing 28(6): 909-935, 2016. Type: Article
Event-B is a formal method for system-level modeling and analysis. In the last decade, Event-B refinement has generated a lot of interest as a formalism for developing highly reliable software. The Event-B language, along with tools su...
|
Apr 12 2017 |
| |
Efficient analysis of probabilistic programs with an unbounded counter
Brázdil T., Kiefer S., Kŭcera A. Journal of the ACM 61(6): 1-35, 2014. Type: Article
The authors consider a probabilistic recursive program working on data of unbounded size, for example, with a geometric probability distribution for what the data looks like. This makes sense for common data structures like trees. Is t...
|
Mar 30 2015 |
| |
Automated termination proofs for Haskell by term rewriting
Giesl J., Raffelsieper M., Schneider-Kamp P., Swiderski S., Thiemann R. ACM Transactions on Programming Languages and Systems 33(2): 1-39, 2011. Type: Article
Automated analysis of software code is a fast-evolving field. Termination analysis is probably the most famous aspect, since it corresponds to the halting problem in computability. This undecidable problem is prototypical of an interes...
|
Apr 6 2011 |
| |
Automated termination proofs for logic programs by term rewriting
Schneider-Kamp P., Giesl J., Serebrenik A., Thiemann R. ACM Transactions on Computational Logic 11(1): 1-52, 2009. Type: Article
Analyzing the termination of programs is perhaps one of the most active research topics in most declarative programming languages. Within the logic programming paradigm, one can find two different types of approaches to analyze termina...
|
Jan 29 2010 |
| |
Termination of simply moded logic programs with dynamic scheduling
Bossi A., Etalle S., Rossi S., Smaus J. ACM Transactions on Computational Logic 5(3): 470-507, 2004. Type: Article
Many Prolog systems search for solutions by using a fixed rule to choose an atom to carry out a derivation step. This approach is not always adequate, since termination cannot be guaranteed, even if the program under consideration has ...
|
Dec 22 2004 |
| |
The complexity of probabilistic verification
Courcoubetis C., Yannakakis M. Journal of the ACM 42(4): 857-907, 1995. Type: Article
Program verification has always been a desirable task, but never an easy one. The advent of concurrent programming has made it significantly more necessary and difficult. Indeed, the conceptual complexity of concurrency increases the l...
|
Jan 1 1997 |
| |
Model checking and modular verification
Grumberg O., Long D. ACM Transactions on Programming Languages and Systems 16(3): 843-871, 1994. Type: Article
When reasoning about systems of parallel processes, verifying global properties requires construction of the global state space, whose size is typically exponential in the number of processes. Avoiding this state explosion is a central...
|
Jun 1 1995 |
| |
The concurrency workbench: a semantics-based tool for the verification of concurrent systems
Cleaveland R., Parrow J., Steffen B. ACM Transactions on Programming Languages and Systems 15(1): 36-72, 1993. Type: Article
Concurrent software systems often have dangerous weaknesses that are almost impossible to uncover by testing or manual quality assurance procedures. This paper describes a toolkit called the Concurrency Workshop that finds such er...
|
Nov 1 1993 |
| |
|
|
| |
|
|
