Search
for Topics
All Reviews
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...)
Options:
All Media Types
Journals
Proceedings
Div Books
Whole Books
Other
Date Reviewed
Title
Author
Publisher
Published Date
Descending
Ascending
110 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 89, 2018) 5365, 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 theorempro...
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): 163192, 2018. Type: Article
Changes in distributedsystem runtime support in response to changes in technological and operational circumstances may also change the services offered to supported systems. The graphbased 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): 345387, 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 computerbased 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 EventB refinement
Hoang T., Schneider S., Treharne H., Williams D. Formal Aspects of Computing 28(6): 909935, 2016. Type: Article
EventB is a formal method for systemlevel modeling and analysis. In the last decade, EventB refinement has generated a lot of interest as a formalism for developing highly reliable software. The EventB 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): 343365, 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): 135, 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 1314, 2015) 4960, 2015. Type: Proceedings
An attribute grammar (AG) is a contextfree grammar extended to describe the decoration of trees corresponding to sentences defined by that contextfree grammar. It provides a declarative specification from which tree computation code can be gener...
Mar 19 2015
A framework for testing firstorder logic axioms in program verification
Ahn K., Denney E. Software Quality Journal 21(1): 159200, 2013. Type: Article
As modeldriven code generators have increased in capability and in performance, so too has their use in missioncritical software development. One benefit of autogenerated 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): 156, 2012. Type: Article
Don’t go near this paper unless you are familiar with the NelsonOppen method, satisfiability modulo theories (SMT), firstorder logic, complete partial orders (CPOs), Tarski, monotone Galois connections, formal semantics, and a host of othe...
Mar 28 2013
Display
5
10
15
25
50
100
per page
Reproduction in whole or in part without permission is prohibited. Copyright © 20002021 ThinkLoud, Inc.
Terms of Use

Privacy Policy