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) > Specification Techniques (F.3.1...)  
  1-10 of 151 Reviews about "Specification Techniques (F.3.1...)": Date Reviewed
  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 Z refinement
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 [1], 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 -calculus
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 [1] 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
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