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 49 Reviews about "Mechanical Verification (F.3.1...)": Date Reviewed
   Mechanising and verifying the WebAssembly specification
Watt C.  CPP 2018 (Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Los Angeles, CA,  Jan 8-9, 2018) 53-65, 2018. Type: Proceedings

Formal verification has had many successful applications to industry standards over the last few years, but an important question is whether formal verification can be included in standard design efforts. This paper presents the use of theorem-pro...

Jul 11 2018
  A semantics comparison workbench for a concurrent, asynchronous, distributed programming language
Corrodi C., Heuner 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 this paper d...

May 23 2018
   Markov chains and Markov decision processes in Isabelle/HOL
Hölzl J.  Journal of Automated Reasoning 59(3): 345-387, 2017. Type: Article

The intermingling of rather different domains can, at times, produce rather interesting results. Here the author explores the intersection of probability theory (in the guise of Markov chains and Markov decision processes) and formal proof (throug...

Jan 11 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 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
Display per page
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