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 46 Reviews about "
Mechanical Verification (F.3.1...)
":
Date Reviewed
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
Modeling and analysis of TinyOS sensor node firmware: a CSP approach
McInnes A. ACM Transactions on Embedded Computing Systems 12(1): 123, 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 wellknown 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): 249260, 2010. Type: Article
It is increasingly recognized that the heroics involved in coding efficient, lowlevel, 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): 105118, 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
5
10
15
25
50
100
per page
Reproduction in whole or in part without permission is prohibited. Copyright © 20002017 ThinkLoud, Inc.
Terms of Use

Privacy Policy