| |
Browse All Reviews > Theory Of Computation (F) > Logics And Meanings Of Programs (F.3) > Specifying And Verifying And Reasoning About Programs (F.3.1) > Logics Of Programs (F.3.1...)
|
|
 |
|
|
| |
|
|
| |
1-10 of 39
Reviews about "Logics Of Programs (F.3.1...)":
|
Date Reviewed |
| |
A Hoare logic for GPU kernels
Kojima K., Igarashi A. ACM Transactions on Computational Logic 18(1): 1-43, 2017. Type: Article
Graphics processing units (GPUs) are hardware accelerators, originally designed to facilitate the fast rendering of images. Later, they became popular for computing in performance-sensitive areas because their highly parallel structure...
|
Aug 8 2018 |
| |
Proof search for propositional abstract separation logics via labelled sequents
Hóu Z., Clouston R., Goré R., Tiu A. ACM SIGPLAN Notices 49(1): 465-476, 2014. Type: Article
Pointers and sharing have always been difficult problems in program verification, and several extensions to Hoare logic have been proposed and investigated over the decades....
|
May 12 2014 |
| |
 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. Peopl...
|
Aug 20 2009 |
| |
Outlier detection by logic programming
Angiulli F., Greco G., Palopoli L. ACM Transactions on Computational Logic 9(1): 7-es, 2007. Type: Article
Detecting outliers in data mining, in the scenario of logic programming, is the topic covered in this paper. The specific problem, in this context, is that the background knowledge may (or may not) be in accordance with the hypotheses ...
|
Apr 28 2008 |
| |
On proving  -termination of rewriting by size-change termination
Fernández M. Information Processing Letters 93(4): 155-162, 2005. Type: Article
Term rewriting systems are an important tool, used in such areas as automated theorem proving, symbolic algebra, and rapid prototyping of equational specifications. A term rewriting system is a set of rewrite rules over terms for a giv...
|
Aug 17 2005 |
| |
Specificational functions
Morris J., Bunkenburg A. ACM Transactions on Programming Languages and Systems 21(3): 677-701, 1999. Type: Article
A function takes an input in its domain to an output in its codomain. How can this notion of function be generalized to include the possibility of a “function” producing no output (partiality) or a number of potenti...
|
Jan 1 2000 |
| |
Singular and plural nondeterministic parameters
Walicki M., Meldal S. SIAM Journal on Computing 26(4): 991-1005, 1997. Type: Article
The authors examine how nondeterminism interacts with the various ways by which parameters can be passed to procedures. For example, the binding of a nondeterministic variable to a particular value can be forced at the time of a proced...
|
Aug 1 1998 |
| |
An introduction to logic programming through Prolog
Spivey M., Prentice-Hall, Inc., Upper Saddle River, NJ, 1996. Type: Book (9780135360477)
Spivey covers three components of logic programming using Prolog: the theoretical background, programming techniques, and an implementation. However, he does not give a full account of all three. The most complete part of the book is o...
|
Jul 1 1997 |
| |
Complementation in abstract interpretation
Cortesi A., Filé G., Ranzato F., Giacobazzi R., Palamidessi C. ACM Transactions on Programming Languages and Systems 19(1): 7-47, 1997. Type: Article
Abstract interpretation is concerned with the semantics of programming languages at different levels of abstraction. The idea is to construct abstract domains that, in some sense, approximate the concrete domain in which the full progr...
|
Jul 1 1997 |
| |
Temporal verification of reactive systems
Manna Z., Pnueli A. (ed), Springer-Verlag New York, Inc., New York, NY, 1995. Type: Book (9780387944593)
A reactive system is a nonterminating system of concurrent processes. Their activities may sometimes require some coordination (such as in a producer-consumer relationship), and this task may be fulfilled by the processes involved or b...
|
Nov 1 1996 |
| |
|
|
| |
|
|
