Browse All Reviews
Theory Of Computation (F)
Logics And Meanings Of Programs (F.3)
Specifying And Verifying And Reasoning About Programs (F.3.1)
> Specification Techniques (F.3.1...)
All Media Types
1-10 of 151 Reviews about "
Specification Techniques (F.3.1...)
From hidden to visible
Zhang M., Ogata K. Theoretical Computer Science 722(C): 52-75, 2018. Type: Article
Algebraic specification is a technique in which a system is modeled by equations or conditional equations. This approach was originally used for defining data types and operations on them. An added benefit is that the equational systems can be rei...
Oct 12 2018
Behavioral subtyping, specification inheritance, and modular reasoning
Leavens G., Naumann D. ACM Transactions on Programming Languages and Systems 37(4): 1-88, 2015. Type: Article
This is a long paper: 67 pages plus a 21-page appendix. It describes the verification of a dynamically dispatched method call of an object-oriented program by using supertype abstraction. The authors maintain that such abstraction is only valid wh...
Dec 15 2015
Comorphisms of structured institutions
Ţuţu I. Information Processing Letters 113(22-24): 894-900, 2013. Type: Article
Once upon a time, programmers talked to their clients. Later, they were given a written specification instead. These specifications became standardized with special forms and formats. Academics explored special logics to use in them. Goguen and Bu...
Dec 11 2013
Formal analysis of event-driven cyber physical systems
Poroor J., Jayaraman B. SecurIT 2012 (Proceedings of the 1st International Conference on Security of Internet of Things, Kollam, India, Aug 17-19, 2012) 1-8, 2012. Type: Proceedings
The authors use the term “cyberphysical system” to describe an event-driven computer system where some events must be processed “as soon as possible.” Unlike real-time systems, these systems do not have explicit timing cons...
Aug 15 2013
Temporal-logic property preservation under
Derrick J., Smith G. Formal Aspects of Computing 24(3): 393-416, 2012. Type: Article
Monotonic properties are known to be preserved under software refinement, and there are counterexamples when an operator such as negation is introduced. The authors of this paper show that monotonic temporal logic properties are preserved under
Sep 27 2012
Flow logic for process calculi
Nielson H., Nielson F., Pilegaard H. ACM Computing Surveys 44(1): 1-39, 2012. Type: Article
Nielson et al. present an approach using flow logic to represent programming notations in process calculi. Flow logic is usually used in static analysis for language paradigms, including imperative, functional, and concurrent features. The lambda ...
May 30 2012
Programming assistance based on contracts and modular verification in the automation domain
Hurnaus D., Prähofer H. SAC 2010 (Proceedings of the 2010 ACM Symposium on Applied Computing, Sierre, Switzerland, Mar 22-26, 2010) 2544-2551, 2010. Type: Proceedings
While formal methods may not be a part of the mainstream , they have been shown, in many projects, to improve quality. Perhaps their mathematics and logic should be hidden inside special tools for specific domains....
Jul 30 2010
Proof search specifications of bisimulation and modal logics for the
Tiu A., Miller D. ACM Transactions on Computational Logic 11(2): 1-35, 2010. Type: Article
In a small but vibrant corner of the computer science world, theoreticians continue an elegant and subtle program to try to elucidate the meaning of computation. Milner, Parrow, and Walker’s
-calculus  has advocated a particular appr...
May 17 2010
Effects for cooperable and serializable threads
Yi J., Flanagan C. TLDI 2010 (Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, Madrid, Spain, Jan 23, 2010) 3-14, 2010. Type: Proceedings
Writing ubiquitously threaded code is still an uncommon practice, as not all problems are suited to threads--and this is unlikely to change any time soon. When problems are suited for threading, good threaded code is hard to craft. This paper...
Apr 30 2010
Functional pearl: streams and unique fixed points
Hinze R. ACM SIGPLAN Notices 43(9): 189-200, 2008. Type: Article
Streams, infinite sequences of elements, play an important role in various areas of mathematics and computer science. On the one hand, they represent a fundamental concept of discrete mathematics, where infinite integer sequences are investigated,...
Jun 11 2009
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2021 ThinkLoud, Inc.