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...)
All Media Types
1-10 of 49 Reviews about "
Mechanical Verification (F.3.1...)
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., Heu
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 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., 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 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
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2021 ThinkLoud, Inc.