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
  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 46 Reviews about "Mechanical Verification (F.3.1...)": Date Reviewed
  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 such as Rodin ...

Apr 12 2017
  Completeness and decidability results for CTL in constructive type theory
Doczkal C., Smolka G.  Journal of Automated Reasoning 56(3): 343-365, 2016. Type: Article

The following sentence from the rather demanding introduction to this quite demanding paper reveals common ground between us users of formal methods and the expert authors of this paper: “Given the practical importance of CTL [computation tr...

Jul 15 2016
  Efficient analysis of probabilistic programs with an unbounded counter
Brázdil T., Kiefer S., Kcera 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 the expected ...

Mar 30 2015
  Linearly ordered attribute grammars: with automatic augmenting dependency selection
van Binsbergen L., Bransen J., Dijkstra A.  PEPM 2015 (Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, Mumbai, India,  Jan 13-14, 2015) 49-60, 2015. Type: Proceedings

An attribute grammar (AG) is a context-free grammar extended to describe the decoration of trees corresponding to sentences defined by that context-free grammar. It provides a declarative specification from which tree computation code can be gener...

Mar 19 2015
  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 that it is sim...

Jun 4 2014
  Theories, solvers and static analysis by abstract interpretation
Cousot P., Cousot R., Mauborgne L.  Journal of the ACM 59(6): 1-56, 2012. Type: Article

Don’t go near this paper unless you are familiar with the Nelson-Oppen method, satisfiability modulo theories (SMT), first-order logic, complete partial orders (CPOs), Tarski, monotone Galois connections, formal semantics, and a host of othe...

Mar 28 2013
  Modeling and analysis of TinyOS sensor node firmware: a CSP approach
McInnes A.  ACM Transactions on Embedded Computing Systems 12(1): 1-23, 2013. Type: Article

This paper, as the name suggests, formalizes certain elements of TinyOS, an operating system that has become popular in the domain of sensor networks. The well-known formalism of communicating sequential processes (CSP) is used for modeling TinyOS...

Mar 8 2013
  Specifying and verifying sparse matrix codes
Arnold G., Hölzl J., Köksal A., Bodík R., Sagiv M.  ACM SIGPLAN Notices 45(9): 249-260, 2010. Type: Article

It is increasingly recognized that the heroics involved in coding efficient, low-level, imperative programs for various tasks are not sustainable. While the gain in efficiency might be quite real, the loss of certainty (with respect to correctness...

Nov 7 2011
  A parametric segmentation functor for fully automatic and scalable array content analysis
Cousot P., Cousot R., Logozzo F.  ACM SIGPLAN Notices 46(1): 105-118, 2011. Type: Article

Precise and scalable static analysis of realistic software is challenging due to several complex features used in software. One of these features, which has been the focus of attention in recent times, is an array. In spite of several proposals fo...

Jun 1 2011
Display per page
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2017 ThinkLoud, Inc.
Terms of Use
| Privacy Policy