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
ACM Transactions on Computational Logic
ACM Press
  1-10 of 66 reviews Date Reviewed 
  Incomplete SMT techniques for solving non-linear formulas over the integers
Borralleras C., Larraz D., Rodríguez-Carbonell E., Oliveras A., Rubio A.  ACM Transactions on Computational Logic 20(4): 1-36, 2019. Type: Article

It is well known that nonlinear integer arithmetic is undecidable due to a negative answer to Hilbert’s tenth problem. Still, constraint solving over nonlinear integer polynomials has attracted considerable attention because of the wide rang...

May 27 2021
  Parallel cost analysis
Albert E., Correas J., Johnsen E., Pun K., Román-Díez G.  ACM Transactions on Computational Logic 19(4): 1-37, 2018. Type: Article

In this paper, the authors present “static cost analysis for distributed systems that exploits the parallelism among distributed locations to infer a more precise estimation of the parallel cost.” Such a parallel cost analysis can be o...

Apr 2 2021
  Hierarchies in inclusion logic with lax semantics
Hannula M.  ACM Transactions on Computational Logic 19(3): 1-23, 2018. Type: Article

A natural interest of computational logic is to investigate decidable subsets of first-order logic. One such subset is the formalism of inclusion logic (FOI), introduced by Galliani as an evolution of dependence logic [1], which investigates funct...

Oct 1 2020
  Verification methods for the computationally complete symbolic attacker based on indistinguishability
Bana G., Chadha R., Eeralla A., Okada M.  ACM Transactions on Computational Logic 21(1): 1-44, 2019. Type: Article

First-order logic formalization for security protocols and attackers enables formal verification. Once a formalization is established, standard tools such as a theorem prover can be used in the analysis....

Dec 16 2019
  Modularisation of sequent calculi for normal and non-normal modalities
Lellmann B., Pimentel E.  ACM Transactions on Computational Logic 20(2): 1-46, 2019. Type: Article

Mathematician and logician Gerhard Gentzen introduced sequent calculus, a logical framework, in the first half of the 20th century. It can be used to establish systems for propositional, first-order, and modal logics. For the latter, it has some s...

Oct 10 2019
  An automatic proving approach to parameterized verification
Li Y., Duan K., Jansen D., Pang J., Zhang L., Lv Y., Cai S.  ACM Transactions on Computational Logic 19(4): 1-25, 2018. Type: Article

Network and security protocols occasionally require important but difficult to authenticate parameters such as the number in a communication party. The existing formal proofs of algorithms for verifying the required parameters in protocols by huma...

Feb 20 2019
  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 is suitable...

Aug 8 2018
  An effective characterization of the alternation hierarchy in two-variable logic
Krebs A., Straubing H.  ACM Transactions on Computational Logic 18(4): 1-22, 2017. Type: Article

Many interesting properties of words can be described in a first-order language with variables (x, y, ...) for positions and two basic properties: x < y (meaning that ...

Jul 6 2018
  Detecting decidable classes of finitely ground logic programs with function symbols
Calautti M., Greco S., Trubitsyna I.  ACM Transactions on Computational Logic 18(4): 1-42, 2017. Type: Article

The termination problem of programs is in general an undecidable problem. However, in the context of some programming paradigms, there has been a lot of research in finding useful decidable criteria characterizing certain subclasses of programs th...

May 22 2018
   Differential hybrid games
Platzer A.  ACM Transactions on Computational Logic 18(3): 1-44, 2017. Type: Article

As software becomes ever more pervasive in safety-critical devices--from pacemakers to cars, from robots to airplanes--it is important that we have means of insuring their safety. For some of the more advanced applications, namely those ...

Mar 22 2018
Display per column
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2021 ThinkLoud, Inc.
Terms of Use
| Privacy Policy